Theorem: comap_span_galRestrict_eq_of_cyclic (FltRegular/NumberTheory/Hilbert94.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}
Tactic:
suffices : (Ideal.span {β}).map
    (galRestrict A K L B σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β}
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
this : Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}

case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.span {↑η * ((galRestrict A K L B) σ) β} = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_eq_top.mpr η.isUnit,
  ← Ideal.one_eq_top, one_mul, ← Set.image_singleton, ← Ideal.map_span] at hβ
State after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map ((galRestrict A K L B) σ) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map ((galRestrict A K L B) σ) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
change Ideal.map (galRestrict A K L B σ : B →+* B) _ = _ at hβ
State after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
generalize σ'⁻¹ = σ'
State after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ'✝ : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ').toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ'✝ : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ').toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
State after:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) (σ ^ n)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) (σ ^ n)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
rw [map_pow]
State after:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}

State before:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
induction n with
| zero =>
  simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe]
  exact Ideal.map_id _
| succ n IH =>
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ] at IH ⊢
  conv_lhs at IH => rw [← hβ, Ideal.map_map]
  exact IH
State after:
no goals

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
this : Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}
Tactic:
rwa [RingEquiv.toRingHom_eq_coe, Ideal.map_comap_of_equiv, map_inv] at this
State after:
no goals

State before:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ ^ 0).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe]
State after:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑1) (Ideal.span {β}) = Ideal.span {β}

State before:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑1) (Ideal.span {β}) = Ideal.span {β}
Tactic:
exact Ideal.map_id _
State after:
no goals

State before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ ^ (n + 1)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ] at IH ⊢
State after:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map (↑↑((galRestrict A K L B) σ ^ n)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}

State before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map (↑↑((galRestrict A K L B) σ ^ n)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Tactic:
conv_lhs at IH => rw [← hβ, Ideal.map_map]
State after:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((↑↑((galRestrict A K L B) σ ^ n)).comp ↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}

State before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((↑↑((galRestrict A K L B) σ ^ n)).comp ↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Tactic:
exact IH
State after:
no goals