Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ ℤ[hζ.toInteger] =
    Algebra.adjoin ℤ ({(algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger} ∪ ⇑(algebraMap (𝓞 ↥F₂) (𝓞 K)) '' {hζ₂✝.toInteger})

pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))

Tactic:
Set.image_singleton,

Goal state after:
K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ ℤ[hζ.toInteger] =
    Algebra.adjoin ℤ ({(algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger} ∪ {(algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger})

K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))