-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
    [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C]
    (h : Function.Injective (algebraMap B C)) : IsCyclotomicExtension (S ∪ T) A C

Proof state:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : f b ∈ Subalgebra.map f (adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb

Result:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Proof state:
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
⊢ IsCyclotomicExtension (S ∪ T) A C

Tactic:
refine ⟨fun hn => ?_, fun x => ?_⟩

Result:
case refine_1
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S ∪ T
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
⊢ x ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Proof state:
case refine_1.inr
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Tactic:
exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn

Result:
no goals

Proof state:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1})
y : C
hy : y ∈ ⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1}
⊢ y ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy

Result:
case refine_2.intro.intro.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1})
y : C
b₁ : B
h₁ : f b₁ = y
n : ℕ+
hn : n ∈ S ∧ b₁ ^ ↑n = 1
⊢ y ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Proof state:
case refine_1.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Tactic:
refine ⟨algebraMap B C b, ?_⟩

Result:
case refine_1.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ IsPrimitiveRoot ((algebraMap B C) b) ↑n✝

Proof state:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
refine adjoin_mono (fun y hy => ?_) hb

Result:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1})
y : C
hy : y ∈ ⇑f '' {b | ∃ a ∈ S, b ^ ↑a = 1}
⊢ y ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Proof state:
case refine_1.inl
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Tactic:
obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn

Result:
case refine_1.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Proof state:
case refine_1.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ IsPrimitiveRoot ((algebraMap B C) b) ↑n✝

Tactic:
exact hb.map_of_injective h

Result:
no goals