Theorem: const_func_ext (WTA.lean)

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
⊢ ((fun x => a) = fun x => b) → a = b
Tactic:
intro h
State after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
⊢ a = b

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
⊢ a = b
Tactic:
have ha : (fun _ : α => a) (choice inferInstance) = a := rfl
State after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
⊢ a = b

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
⊢ a = b
Tactic:
have hb : (fun _ : α => b) (choice inferInstance) = b := rfl
State after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
hb : (fun x => b) (choice (_ : Nonempty α)) = b
⊢ a = b

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
hb : (fun x => b) (choice (_ : Nonempty α)) = b
⊢ a = b
Tactic:
rw [←ha, ←hb, h]
State after:
no goals