import Mathlib import Mathlib.Tactic import Mathlib.Algebra.Group.Defs import Canonical variable {G : Type*} [Group G] theorem t1 (h : ∃ (a : G), a ≠ 1 ∧ a⁻¹ = a) : ∃ (a : G), a ≠ 1 ∧ a = a⁻¹ := -- by canonical by exact Exists.intro h.choose ⟨fun a ↦ Eq.rec (motive := fun a t ↦ a) (Sort _) (False.rec (fun t ↦ Sort _ = False) ((Exists.choose_spec h).1 a)), Eq.rec (motive := fun a t ↦ a = h.choose⁻¹) (Eq.refl h.choose⁻¹) (Exists.choose_spec h).2⟩ 

error: Main.lean:14:82: type mismatch False has type Prop : Type but is expected to have type Type ?u.675 : Type (?u.675 + 1) 

import Mathlib import Mathlib.Tactic import Mathlib.Algebra.Group.Defs import Canonical variable {G : Type*} [Group G] theorem t1 (h : ∃ (a : G), a ≠ 1 ∧ a⁻¹ = a) : ∃ (a : G), a ≠ 1 ∧ a = a⁻¹ := -- by canonical [congrFun] by exact Exists.intro h.choose ⟨fun a ↦ False.rec (fun t ↦ False) ((Exists.choose_spec h).1 a), Eq.rec (motive := fun a t ↦ a = h.choose⁻¹) (Eq.refl h.choose⁻¹) (Exists.choose_spec h).2⟩