-- 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_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✝

Tactic:
rcases hn with hn | hn

Result:
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✝

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✝

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
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
let f := IsScalarTower.toAlgHom A B C

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
⊢ (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)
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 ^ ↑n = 1

Tactic:
rw [← h₁, ← map_pow, hn.2, map_one]

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
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}).map f :=
  ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩

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 : 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}

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
⊢ x ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
refine adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
  (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
  (fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy)
  fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy

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
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Proof state:
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}

Tactic:
exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← map_pow, hn.2, map_one]⟩⟩

Result:
no goals