Theorem: ModularCyclotomicCharacter.id (AntLorentz/CyclotomicCharacter.lean)

State before:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ χ n (RingEquiv.refl L) = 1
Tactic:
refine ext (G := rootsOfUnity n L) rfl ?_
State after:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (RingEquiv.refl L)) = t ^ ZMod.val 1

State before:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (RingEquiv.refl L)) = t ^ ZMod.val 1
Tactic:
intro ζ
State after:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (RingEquiv.refl L)) = ζ ^ ZMod.val 1

State before:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (RingEquiv.refl L)) = ζ ^ ZMod.val 1
Tactic:
ext
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (RingEquiv.refl L))) = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (RingEquiv.refl L))) = ↑↑(ζ ^ ZMod.val 1)
Tactic:
rw [← spec]
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
State after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
obtain (h | h) := this.lt_or_eq
State after:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have := Fact.mk h
State after:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
this : Fact (1 < Fintype.card { x // x ∈ rootsOfUnity n L })
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
this : Fact (1 < Fintype.card { x // x ∈ rootsOfUnity n L })
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
simp [ZMod.val_one]
State after:
no goals

State before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have := Fintype.card_le_one_iff_subsingleton.mp h.ge
State after:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

State before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
obtain rfl : ζ = 1 := by apply Subsingleton.elim
State after:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑1 = ↑↑(1 ^ ZMod.val 1)

State before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑1 = ↑↑(1 ^ ZMod.val 1)
Tactic:
simp
State after:
no goals

State before:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ζ = 1
Tactic:
apply Subsingleton.elim
State after:
no goals