awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : Algebra C D
inst_4 : Algebra C E
inst_5 : Algebra D E
inst_6 : IsScalarTower C D E
S : Set E
this :
  Eq (α := Set E) (Set.range.{u_3, u_2 + 1} (ι := D) (⇑(algebraMap D E) : (a : D) → E))
    (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
      (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
        (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E))
x : E
⊢ Membership.mem (γ := Subsemiring E)
      (Subsemiring.closure (Set.range.{u_3, u_2 + 1} (ι := D) (⇑(algebraMap D E) : (a : D) → E) ∪ S)) x ↔
    Membership.mem (γ := Subsemiring E)
      (Subsemiring.closure
        (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
            (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
              (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E) ∪
          S))
      x
have h : Membership.mem (γ := Subsemiring E)
    (Subsemiring.closure
      (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
          (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
            (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E) ∪
        S))
    x ↔
  Membership.mem (γ := Subsemiring E)
    (Subsemiring.closure
      (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
          (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
            (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E) ∪
        S))
    x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : Algebra C D
inst_4 : Algebra C E
inst_5 : Algebra D E
inst_6 : IsScalarTower C D E
S : Set E
⊢ Eq (α := Subalgebra C E) (Subalgebra.restrictScalars C (adjoin D S))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S))
have D₁ : Eq (α := Set E) (Set.range.{u_3, u_2 + 1} (ι := D) (⇑(algebraMap D E) : (a : D) → E))
  (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
    (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
      (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E))
Tactic: suffices
    Set.range (algebraMap D E) =
      Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E) by
    ext x
    change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
    rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : CommSemiring F
inst_4 : Algebra C D
inst_5 : Algebra C E
inst_6 : Algebra C F
inst_7 : Algebra D F
inst_8 : Algebra E F
inst_9 : IsScalarTower C D F
inst_10 : IsScalarTower C E F
S : Set D
T : Set E
hS : Eq (α := Subalgebra C D) (adjoin C S) ⊤
hT : Eq (α := Subalgebra C E) (adjoin C T) ⊤
⊢ Eq.{u_4 + 1} (α := Subalgebra C F) (Subalgebra.restrictScalars C (adjoin E ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
have rw : Eq.{u_4 + 1} (α := Subalgebra C F)
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
  (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
Tactic: rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
    ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
    IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
    adjoin_union_eq_adjoin_adjoin, Set.union_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : CommSemiring F
inst_4 : Algebra C D
inst_5 : Algebra C E
inst_6 : Algebra C F
inst_7 : Algebra D F
inst_8 : Algebra E F
inst_9 : IsScalarTower C D F
inst_10 : IsScalarTower C E F
S : Set D
T : Set E
hS : Eq (α := Subalgebra C D) (adjoin C S) ⊤
hT : Eq (α := Subalgebra C E) (adjoin C T) ⊤
rw :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
⊢ Eq.{u_4 + 1} (α := Subalgebra C F) (Subalgebra.restrictScalars C (adjoin E ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
have rw₁ : Eq.{u_4 + 1} (α := Subalgebra C F)
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤)) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
Tactic: rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
    ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
    IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
    adjoin_union_eq_adjoin_adjoin, Set.union_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : CommSemiring F
inst_4 : Algebra C D
inst_5 : Algebra C E
inst_6 : Algebra C F
inst_7 : Algebra D F
inst_8 : Algebra E F
inst_9 : IsScalarTower C D F
inst_10 : IsScalarTower C E F
S : Set D
T : Set E
hS : Eq (α := Subalgebra C D) (adjoin C S) ⊤
hT : Eq (α := Subalgebra C E) (adjoin C T) ⊤
rw :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₁ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤)) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
⊢ Eq.{u_4 + 1} (α := Subalgebra C F) (Subalgebra.restrictScalars C (adjoin E ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
have rw₂ : Eq.{u_4 + 1} (α := Subalgebra C F)
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
Tactic: rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
    ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
    IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
    adjoin_union_eq_adjoin_adjoin, Set.union_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : CommSemiring F
inst_4 : Algebra C D
inst_5 : Algebra C E
inst_6 : Algebra C F
inst_7 : Algebra D F
inst_8 : Algebra E F
inst_9 : IsScalarTower C D F
inst_10 : IsScalarTower C E F
S : Set D
T : Set E
hS : Eq (α := Subalgebra C D) (adjoin C S) ⊤
hT : Eq (α := Subalgebra C E) (adjoin C T) ⊤
rw :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₁ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤)) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₂ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
⊢ Eq.{u_4 + 1} (α := Subalgebra C F) (Subalgebra.restrictScalars C (adjoin E ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
have rw₃ : Eq.{u_4 + 1} (α := Subalgebra C F)
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) (adjoin C T)))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) (adjoin C T))) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
  (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
Tactic: rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
    ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
    IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
    adjoin_union_eq_adjoin_adjoin, Set.union_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hRS : Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
hSA : Subalgebra.FG.{u_2, u_3} (R := S) (A := A) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
have rcases : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
Tactic: rcases hRS with ⟨s, hs⟩
Cleared hypotheses: hRS
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hSA : Subalgebra.FG.{u_2, u_3} (R := S) (A := A) ⊤
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
have rcases : ∀ (t : Finset A) (ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤), Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
Tactic: rcases hSA with ⟨t, ht⟩
Cleared hypotheses: hSA
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw : Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₂ : Eq (α := Subalgebra R A)
  (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
    (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
  ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
rw₂ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
      (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
    ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₃ : Eq (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (adjoin ↥⊤ (↑t : Set A))) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
rw₂ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
      (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
    ⊤
rw₃ : Eq (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (adjoin ↥⊤ (↑t : Set A))) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₄ : Eq (α := Subalgebra R A)
  (Subalgebra.restrictScalars R (S := ↥⊤) (Subalgebra.restrictScalars (↥⊤) (adjoin S (↑t : Set A)))) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
rw₂ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
      (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
    ⊤
rw₃ : Eq (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (adjoin ↥⊤ (↑t : Set A))) ⊤
rw₄ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars R (S := ↥⊤) (Subalgebra.restrictScalars (↥⊤) (adjoin S (↑t : Set A)))) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₅ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (Subalgebra.restrictScalars ↥⊤ (S := S) ⊤)) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
rw₂ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
      (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
    ⊤
rw₃ : Eq (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (adjoin ↥⊤ (↑t : Set A))) ⊤
rw₄ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars R (S := ↥⊤) (Subalgebra.restrictScalars (↥⊤) (adjoin S (↑t : Set A)))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (Subalgebra.restrictScalars ↥⊤ (S := S) ⊤)) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₆ : Eq.{u_3 + 1} (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) ⊤) ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
t : Finset A
ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤
rw :
  Eq (α := Subalgebra R A) (adjoin R ((↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s) : Set A) ∪ (↑t : Set A))) ⊤
rw₁ : Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' (↑s : Set S) ∪ (↑t : Set A))) ⊤
rw₂ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥(adjoin R (↑s : Set S)))
      (adjoin ↥(adjoin R (↑s : Set S)) (↑t : Set A)))
    ⊤
rw₃ : Eq (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (adjoin ↥⊤ (↑t : Set A))) ⊤
rw₄ :
  Eq (α := Subalgebra R A)
    (Subalgebra.restrictScalars R (S := ↥⊤) (Subalgebra.restrictScalars (↥⊤) (adjoin S (↑t : Set A)))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) (Subalgebra.restrictScalars ↥⊤ (S := S) ⊤)) ⊤
rw₆ : Eq.{u_3 + 1} (α := Subalgebra R A) (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥⊤) ⊤) ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) s ∪ t) : Set A)) ⊤
have rw₇ : Eq.{u_3 + 1} (α := Subalgebra R A) ⊤ ⊤
Tactic: rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hRS : Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
hSA : Subalgebra.FG.{u_2, u_3} (R := S) (A := A) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
have rcases : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
Tactic: classical
  rcases hRS with ⟨s, hs⟩
  rcases hSA with ⟨t, ht⟩
  exact ⟨s.image (algebraMap S A) ∪ t, by
    rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
    ⟩
Cleared hypotheses: hRS