Theorem: cantor_diagonal' (GroupComp/Turing.lean)

State before:
α : Type
f : α → α → Bool
⊢ ∃ t, ∀ (a : α), t ≠ f a
Tactic:
apply Exists.intro (fun a ↦ !(f a a) )
State after:
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a

State before:
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a
Tactic:
intro a h
State after:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False

State before:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False
Tactic:
let h' := congrFun h a
State after:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False

State before:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False
Tactic:
by_cases c:f a a <;> simp [c] at h'
State after:
no goals