Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux (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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
obtain ⟨β, hβ_zero, hβ⟩ := Hilbert90_integral (A := A) (B := B) σ hσ η hη
State after:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)

State before:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
haveI : IsDomain B :=
  (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
State after:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)

State before:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
have hβ' := comap_map_eq_of_isUnramified K L _
  (comap_span_galRestrict_eq_of_cyclic σ hσ (A := A) (B := B) β η hβ)
State after:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)

State before:
case intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
refine ⟨(Ideal.span {β}).comap (algebraMap A B), ?_, ?_⟩
State after:
case intro.intro.refine_1
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ¬Submodule.IsPrincipal (Ideal.comap (algebraMap A B) (Ideal.span {β}))

case intro.intro.refine_2
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})))

State before:
case intro.intro.refine_1
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ¬Submodule.IsPrincipal (Ideal.comap (algebraMap A B) (Ideal.span {β}))
Tactic:
rintro ⟨⟨γ, hγ : _ = Ideal.span _⟩⟩
State after:
case intro.intro.refine_1.mk.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
γ : A
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False

State before:
case intro.intro.refine_1.mk.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
γ : A
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Tactic:
rw [hγ, Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hβ'
State after:
case intro.intro.refine_1.mk.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
γ : A
hβ' : Associated ((algebraMap A B) γ) β
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False

State before:
case intro.intro.refine_1.mk.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
γ : A
hβ' : Associated ((algebraMap A B) γ) β
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Tactic:
obtain ⟨a, rfl⟩ := hβ'
State after:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ((algebraMap A B) γ * ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ False

State before:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ((algebraMap A B) γ * ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ False
Tactic:
rw [map_mul, AlgEquiv.commutes, mul_left_comm, (mul_right_injective₀ _).eq_iff] at hβ
State after:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ False

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ False

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
apply hη'
State after:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case intro.intro.refine_1.mk.intro.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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
use a
State after:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η = (algebraMap B L) ↑a / σ ((algebraMap B L) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η = (algebraMap B L) ↑a / σ ((algebraMap B L) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
conv_rhs => enter [1]; rw [← hβ]
State after:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η = (algebraMap B L) (↑η * ((galRestrict A K L B) σ) ↑a) / σ ((algebraMap B L) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η = (algebraMap B L) (↑η * ((galRestrict A K L B) σ) ↑a) / σ ((algebraMap B L) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K L B σ a]
State after:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η =
    (algebraMap B L) ↑η * (algebraMap B L) (((galRestrict A K L B) σ) ↑a) /
      (algebraMap B L) (((galRestrictHom A K L B) ↑σ) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η =
    (algebraMap B L) ↑η * (algebraMap B L) (((galRestrict A K L B) σ) ↑a) /
      (algebraMap B L) (((galRestrictHom A K L B) ↑σ) ↑a)

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
refine (mul_div_cancel_right₀ _ ?_).symm
State after:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) (((galRestrict A K L B) σ) ↑a) ≠ 0

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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0

State before:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) (((galRestrict A K L B) σ) ↑a) ≠ 0
Tactic:
rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsIntegralClosure.algebraMap_injective B A L),
  (injective_iff_map_eq_zero' _).mp (galRestrict A K L B σ).injective]
State after:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ¬↑a = 0

State before:
case h
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ¬↑a = 0
Tactic:
exact a.isUnit.ne_zero
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
exact (mul_ne_zero_iff.mp hβ_zero).1
State after:
no goals

State before:
case intro.intro.refine_2
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})))
Tactic:
rw [hβ']
State after:
case intro.intro.refine_2
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.span {β})

State before:
case intro.intro.refine_2
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 : finrank K L = ↑p
A : Type u_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.span {β})
Tactic:
exact ⟨⟨_, rfl⟩⟩
State after:
no goals