contradiction tactic with excluded middle

Stream: general

[procero]

Hey would anyone be able to help me with this proof? I'm trying to show that f B.T ≠ B.F -> f B.T = B.T

This is what I have tried so far.

inductive B : Type
| T : B
| F : B

example : ∀ (f : B → B), f B.T ≠ B.F -> f B.T = B.T := by
  intro f he
  cases Classical.em (f B.T = B.T)
  assumption
  contradiction

The context it arrives at:

f: B → B
he: f B.T ≠ B.F
h✝: ¬f B.T = B.T
⊢ f B.T = B.T

I think he and h✝ should be a contradiction but the tactic doesn't work.

[Kevin Buzzard]

They're not literally a contradiction: a contradiction would be P and \not P. You seem to want to do cases on f B.T, then you should be fine

[Jireh Loreaux]

Although the function f here is just a red herring.

inductive B : Type
| T : B
| F : B

theorem eq_T_of_ne_F {x : B} (hx : x ≠ B.F) : x = B.T :=
  match x with
  | B.T => rfl
  | B.F => (hx rfl).elim

example : ∀ (f : B → B), f B.T ≠ B.F -> f B.T = B.T := by
  intro f he
  exact eq_T_of_ne_F he

[Eric Wieser]

Or with even less work:

inductive B : Type
| T : B
| F : B

theorem eq_T_of_ne_F {x : B} (hx : x ≠ B.F) : x = B.T :=
  match x, hx with
  | B.T, _ => rfl

example : ∀ (f : B → B), f B.T ≠ B.F -> f B.T = B.T := by
  intro f he
  exact eq_T_of_ne_F he

match can eliminate the false case for you

[procero]

I don't quite understand this line

  | B.F => (hx rfl).elim

Is rfl a tactic in (hx rfl).elim? What does it mean? My understanding here is that some how Lean treated rfl like x = B x but I want to understand how one can get the equality implied by the match branch as an assumption.

i.e.

match x with
| B.T => /-! where is x = B.T ? -/
...

[Kyle Miller]

No, rfl is a term, and it's the constructor for the equality type.

[Kyle Miller]

Here's a tactic equivalent for that proof:

theorem eq_T_of_ne_F {x : B} (hx : x ≠ B.F) : x = B.T := by
  cases x with
  | T => rfl
  | F =>
    exfalso -- corresponds to `(...).elim`, short for `False.elim (...)`
    apply hx
    rfl

[Ruben Van de Velde]

You may be confused because rfl is used for three distinct things in lean; it's a term of type a = a, it's a tactic that proves a goal R a a for any reflexive relation R, and it's a pattern used to substitute out variables in rcases/obtain