-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
lemma id : χ₀ n (RingEquiv.refl L) = 1

Proof state:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
this : Subsingleton ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
obtain rfl : t = 1 := Subsingleton.elim t 1

Result:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
this : Subsingleton ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑1 = ↑(↑1 ^ ZMod.val 1)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
⊢ χ₀ n (RingEquiv.refl L) = 1

Tactic:
refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
obtain (h | h) := this.lt_or_eq

Result:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 < Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Proof state:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 < Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
have := Fact.mk h

Result:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 < Fintype.card ↥(rootsOfUnity n L)
this : Fact (1 < Fintype.card ↥(rootsOfUnity n L))
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Proof state:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 < Fintype.card ↥(rootsOfUnity n L)
this : Fact (1 < Fintype.card ↥(rootsOfUnity n L))
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
simp [ZMod.val_one]

Result:
no goals

Proof state:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
have := Fintype.card_le_one_iff_subsingleton.mp h.ge

Result:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
this : Subsingleton ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Proof state:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
this✝ : 1 ≤ Fintype.card ↥(rootsOfUnity n L)
h : 1 = Fintype.card ↥(rootsOfUnity n L)
this : Subsingleton ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑1 = ↑(↑1 ^ ZMod.val 1)

Tactic:
simp

Result:
no goals