internlm/Lean-Github huggingface dataset:
Theorem: flt_regular
Proof state before:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False
Tactic:
by_cases case : ↑p ∣ (a / d) * (b / d) * (c / d)
Proof state after:
case pos
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False

case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Theorem: flt_regular
Proof state before:
case pos
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False

case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
exact caseII hreg hodd hprod' hgcd case e'
Proof state after:
case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Theorem: flt_regular
Proof state before:
case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
exact caseI hreg case e'
Proof state after:
no goals
Theorem: isRegularNumber_two
Proof state before:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsRegularNumber 2
Tactic:
rw [IsRegularNumber]
Proof state after:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Coprime 2 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))))
Theorem: isRegularNumber_two
Proof state before:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Coprime 2 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))))
Tactic:
convert coprime_one_right _
Proof state after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))) = 1
Theorem: isRegularNumber_two
Proof state before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))) = 1
Tactic:
dsimp
Proof state after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField 2 ℚ))) = 1
Theorem: isRegularNumber_two
Proof state before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField 2 ℚ))) = 1
Tactic:
apply (card_classGroup_eq_one_iff (R := 𝓞 (CyclotomicField (⟨2, two_pos⟩ : ℕ+) ℚ))).2
Proof state after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))
Theorem: isRegularNumber_two
Proof state before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))
Tactic:
infer_instance
Proof state after:
no goals
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
⊢ Submodule.IsPrincipal I
Tactic:
by_cases Izero : I = 0
Proof state after:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal I

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ Submodule.IsPrincipal I
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ Submodule.IsPrincipal I
Tactic:
rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero _)] at hI ⊢
Proof state after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
swap
Proof state after:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
swap
Proof state after:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1
Tactic:
rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
Proof state after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup A)
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup A)
Tactic:
refine ⟨?_, orderOf_dvd_card⟩
Proof state after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p
Tactic:
rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow]
Proof state after:
no goals
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal I
Tactic:
rw [Izero]
Proof state after:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal 0
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal 0
Tactic:
exact bot_isPrincipal
Proof state after:
no goals
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0
Tactic:
exact Izero
Proof state after:
no goals
Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime
Proof state before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
exact pow_ne_zero p Izero
Proof state after:
no goals
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ ∃ n, x ≡ ↑n [SMOD span {pb.gen}]
Tactic:
refine' ⟨(pb.basis.repr x) ⟨0, pb.dim_pos⟩, _⟩
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
have H := Basis.sum_repr pb.basis x
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [PowerBasis.coe_basis, ← insert_erase (mem_univ (⟨0, pb.dim_pos⟩ : Fin pb.dim)), sum_insert] at H
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr x) i • (fun i => pb.gen ^ ↑i) i = x
⊢ ⟨0, ⋯⟩ ∉ univ.erase ⟨0, ⋯⟩
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
have :
  ∀ i : (univ : Finset (Fin pb.dim)).erase ⟨0, pb.dim_pos⟩,
    ↑((pb.basis.repr x) i) * pb.gen ^ ((i : Fin pb.dim) : ℕ) =
      ↑((pb.basis.repr x) i) * pb.gen ^ (i : ℕ).pred.succ := by
  rintro ⟨i, hi⟩
  congr 1
  rw [succ_pred_eq_of_pos]
  rw [Subtype.coe_mk]
  refine' Nat.pos_of_ne_zero fun h => _
  cases' i with i₁ hi₁
  simp only [Subtype.coe_mk] at h
  simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
  exact hi h
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
simp only [Fin.val_mk, _root_.pow_zero, zsmul_eq_mul] at H
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, ↑((pb.basis.repr x) x_1) * pb.gen ^ ↑x_1 = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, ↑((pb.basis.repr x) x_1) * pb.gen ^ ↑x_1 = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [← Finset.sum_finset_coe] at H
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
conv_lhs at H =>
  congr
  rfl
  congr
  rfl
  ext i
  rw [this i, _root_.pow_succ, ← mul_assoc, mul_comm _ pb.gen]
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), pb.gen * (↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), pb.gen * (↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [← mul_sum] at H
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
nth_rw 1 [← H]
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred ≡
    ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]