Theorem: FltRegular.is_principal_aux (FltRegular/CaseI/Statement.lean)

State before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
letI : NumberField K' := IsCyclotomicExtension.numberField { P } ℚ K'
State after:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨α, hα⟩ : I.IsPrincipal := by
  apply IsPrincipal_of_IsPrincipal_pow_of_Coprime (𝓞 K') _ hreg I
  constructor
  use ↑a + ζ * ↑b
  rw [submodule_span_eq, hI]
State after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : I = Submodule.span (𝓞 K') {α}
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : I = Submodule.span (𝓞 K') {α}
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
replace hα := congr_arg (fun (J : Submodule _ _) => J ^ p) hα
State after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : (fun J => J ^ p) I = (fun J => J ^ p) (Submodule.span (𝓞 K') {α})
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : (fun J => J ^ p) I = (fun J => J ^ p) (Submodule.span (𝓞 K') {α})
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
simp only [← hI, submodule_span_eq, span_singleton_pow, span_singleton_eq_span_singleton] at hα
State after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : Associated (↑a + ζ * ↑b) (α ^ p)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : Associated (↑a + ζ * ↑b) (α ^ p)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨u, hu⟩ := hα
State after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
refine' ⟨u⁻¹, α, _⟩
State after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * α ^ p = ↑a + ζ * ↑b

State before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * α ^ p = ↑a + ζ * ↑b
Tactic:
rw [← hu, mul_comm ((_ + ζ * _)), ← mul_assoc]
State after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * ↑u * (↑a + ζ * ↑b) = ↑a + ζ * ↑b

State before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * ↑u * (↑a + ζ * ↑b) = ↑a + ζ * ↑b
Tactic:
simp only [Units.inv_mul, one_mul]
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal I
Tactic:
apply IsPrincipal_of_IsPrincipal_pow_of_Coprime (𝓞 K') _ hreg I
State after:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal (I ^ p)

State before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal (I ^ p)
Tactic:
constructor
State after:
case principal'
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ a, I ^ p = Submodule.span (𝓞 K') {a}

State before:
case principal'
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ a, I ^ p = Submodule.span (𝓞 K') {a}
Tactic:
use ↑a + ζ * ↑b
State after:
case h
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ I ^ p = Submodule.span (𝓞 K') {↑a + ζ * ↑b}

State before:
case h
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ I ^ p = Submodule.span (𝓞 K') {↑a + ζ * ↑b}
Tactic:
rw [submodule_span_eq, hI]
State after:
no goals