-- Mathlib/Algebra/Module/CharacterModule.lean
lemma eq_zero_of_ofSpanSingleton_apply_self (a : A)
    (h : ofSpanSingleton a ⟨a, Submodule.mem_span_singleton_self a⟩ = 0) : a = 0

Proof state:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a

Tactic:
split_ifs with h

Result:
case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
h : addOrderOf a = 0
⊢ 0 < 2

case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
h : ¬addOrderOf a = 0
⊢ 0 < addOrderOf a

Proof state:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0

Tactic:
apply_fun Rat.den at hn

Result:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : (n • 1).den = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ a = 0

Proof state:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0
⊢ a = 0

Tactic:
erw [ofSpanSingleton, LinearMap.toAddMonoidHom_coe, LinearMap.comp_apply,
   intSpanEquivQuotAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
  AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_one,
  AddCircle.coe_eq_zero_iff] at h

Result:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0

Proof state:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0

Tactic:
rcases h with ⟨n, hn⟩

Result:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹
⊢ a = 0

Proof state:
case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
⊢ a = 0

Tactic:
rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn

Result:
no goals

Proof state:
case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
h : addOrderOf a = 0
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : (n • 1).den = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ a = 0

Tactic:
rw [zsmul_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos] at hn

Result:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a

Proof state:
case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
h : ¬addOrderOf a = 0
⊢ 0 < addOrderOf a

Tactic:
exact Nat.pos_of_ne_zero h

Result:
no goals

Proof state:
case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : addOrderOf a = 0
hn : 1 = 2
⊢ a = 0

Tactic:
cases hn

Result:
no goals

Proof state:
case intro
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

Tactic:
split_ifs at hn

Result:
case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : addOrderOf a = 0
hn : 1 = 2
⊢ a = 0

case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
⊢ a = 0