-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :
    Module.Finite A B

Proof state:
case empty
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Module.Finite A B

Tactic:
refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩

Result:
case empty
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Submodule.span A ↑{1} = ⊤

Proof state:
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B

Tactic:
rw [← union_singleton] at h₂

Result:
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (S ∪ {n}) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B

Proof state:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
⊢ Module.Finite A B

Tactic:
haveI : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) :=
  union_left _ (insert n S) _ _ (subset_insert n S)

Result:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite A B

Proof state:
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (S ∪ {n}) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B

Tactic:
let _ := union_right S {n} A B

Result:
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (S ∪ {n}) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
x✝ : IsCyclotomicExtension {n} (↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})) B := union_right S {n} A B
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B

Proof state:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite A B

Tactic:
haveI := H A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1})

Result:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite A B

Proof state:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
⊢ Module.Finite A B

Tactic:
have : Module.Finite (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) B := by
  rw [← union_singleton] at h₂
  let _ := union_right S {n} A B
  exact finite_of_singleton n _ _

Result:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this✝¹ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this✝ : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B
⊢ Module.Finite A B

Proof state:
case insert
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
this✝¹ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this✝ : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B
⊢ Module.Finite A B

Tactic:
exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) _

Result:
no goals

Proof state:
case empty
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Submodule.span A ↑{1} = ⊤

Tactic:
simp [← top_toSubmodule, ← empty, toSubmodule_bot, Submodule.one_eq_span]

Result:
no goals