awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
h_1 : n ∈ Finset.range (P.natDegree + 1)
⊢ IsIntegral R (A := K)
    ((HSMul.hSMul (β := Fin B.dim →₀ K) (P.coeff n)
            ((B.basis.repr : (a : S) → Fin B.dim →₀ K) (B.gen ^ n) : Fin B.dim →₀ K) :
          (a : Fin B.dim) → K)
        i :
      K)

Tactic:
exact (repr_gen_pow_isIntegral hB hmin _ _).smul _

Premises used: PowerBasis.repr_gen_pow_isIntegral, IsIntegral.smul
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
p : A[X]
⊢ Membership.mem (α := C) (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)]
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (ofId B C)) (Subalgebra.val A[b])) : ↥A[b] →+* C) : (a : ↥A[b]) → C)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) ⋯ :
          ↥A[b]) :
      C)

Tactic:
aesop (add norm [adjoin_singleton_eq_range_aeval, aeval_algebraMap_apply])

Premises used: Algebra.adjoin_singleton_eq_range_aeval, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
x : ↥A[b]
f :
  ∀ (p : A[X]),
    Membership.mem (α := C) (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)]
      (((↑(AlgHom.comp (AlgHom.restrictScalars A (ofId B C)) (Subalgebra.val A[b])) : ↥A[b] →+* C) : (a : ↥A[b]) → C)
          (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p)
              ⋯ :
            ↥A[b]) :
        C)
⊢ Membership.mem (α := C) (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)]
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (ofId B C)) (Subalgebra.val A[b])) : ↥A[b] →+* C) : (a : ↥A[b]) → C) x :
      C)

Tactic:
induction x using adjoin_singleton_induction with
      | f p => aesop (add norm [adjoin_singleton_eq_range_aeval, aeval_algebraMap_apply])

Premises used: Algebra.adjoin_singleton_eq_range_aeval, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
x : ↥A[b]
⊢ Eq.{u_3 + 1} (α := C) ((↑((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) x) : C) : C)
    ((algebraMap B C : (a : B) → C) (↑x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
c : ↥A[((algebraMap B C : (a : B) → C) b : C)]
obtain :
  ∀ (p : A[X]) (hp : ((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p = (↑c : C)),
    ∃ (a : ↥A[b]), (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = c
⊢ ∃ (a : ↥A[b]), (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = c

Tactic:
obtain ⟨p, hp⟩ := adjoin_eq_exists_aeval A (algebraMap B C b) c

Premises used: Algebra.algebraMap, Algebra.adjoin_eq_exists_aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
c : ↥A[((algebraMap B C : (a : B) → C) b : C)]
p : A[X]
hp : ((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p = (↑c : C)
⊢ ∃ (a : ↥A[b]), (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = c

Tactic:
aesop (add safe ((aeval_algebraMap_apply C b p).symm))

Premises used: Eq.symm, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
⊢ Eq (α := RingHom.{u_2, u_3} (↥A[b]) C) (algebraMap (↥A[b]) C)
    (@RingHom.comp _ ↥A[((algebraMap B C : (a : B) → C) b : C)] _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↥A[((algebraMap B C : (a : B) → C) b : C)]) C)
      (algebraMap ↥A[b] ↥A[((algebraMap B C : (a : B) → C) b : C)]))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
apply :
  ∀ (y : ↥A[((algebraMap B C : (a : B) → C) b : C)]),
    ∃! a : ↥A[b], (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = y
⊢ RingEquiv.{u_2, u_3} ↥A[b] ↥A[((algebraMap B C : (a : B) → C) b : C)]

Tactic:
apply RingEquiv.ofBijective (RingHom.adjoinAlgebraMap b)
     ((Function.bijective_iff_existsUnique (adjoinAlgebraMap b)).mpr (fun y ↦ ?_))

Premises used: Iff.mpr, RingEquiv.ofBijective, Algebra.RingHom.adjoinAlgebraMap, DFunLike.coe, Function.bijective_iff_existsUnique
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
p : A[X]
⊢ Membership.mem (α := B) (γ := Subalgebra A B) A[b] ((aeval b : (a : A[X]) → B) p : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
p : A[X]
h :
  (fun (a : ↥A[b]) ↦
        Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
          ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
            ↥A[((algebraMap B C : (a : B) → C) b : C)])
          (Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
              (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
            ↥A[((algebraMap B C : (a : B) → C) b : C)]))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) ⋯) ∧
    ∀ (y : ↥A[b]),
      (fun (a : ↥A[b]) ↦
            Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
              ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
                ↥A[((algebraMap B C : (a : B) → C) b : C)])
              (Subtype.mk (p := fun (x : C) ↦
                  Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
                  (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
                ↥A[((algebraMap B C : (a : B) → C) b : C)]))
          y →
        y = Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) ⋯
⊢ ∃! a : ↥A[b],
    Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
      ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])
      (Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
          (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])

Tactic:
use ⟨p.aeval b, by simp⟩
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
p : A[X]
⊢ (fun (a : ↥A[b]) ↦
        Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
          ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
            ↥A[((algebraMap B C : (a : B) → C) b : C)])
          (Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
              (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
            ↥A[((algebraMap B C : (a : B) → C) b : C)]))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) ⋯) ∧
    ∀ (y : ↥A[b]),
      (fun (a : ↥A[b]) ↦
            Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
              ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
                ↥A[((algebraMap B C : (a : B) → C) b : C)])
              (Subtype.mk (p := fun (x : C) ↦
                  Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
                  (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
                ↥A[((algebraMap B C : (a : B) → C) b : C)]))
          y →
        y = Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) ⋯

Tactic:
aesop (add norm [Polynomial.aeval_algebraMap_apply, Subtype.ext_iff])

Premises used: Subtype.ext_iff, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Singleton
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
y : ↥A[((algebraMap B C : (a : B) → C) b : C)]
f :
  ∀ (p : A[X]),
    ∃! a : ↥A[b],
      Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
        ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
          ↥A[((algebraMap B C : (a : B) → C) b : C)])
        (Subtype.mk (p := fun (x : C) ↦
            Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
            (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
          ↥A[((algebraMap B C : (a : B) → C) b : C)])
⊢ ∃! a : ↥A[b], (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = y

Tactic:
induction y using Algebra.adjoin_singleton_induction with | f p =>
  use ⟨p.aeval b, by simp⟩
  aesop (add norm [Polynomial.aeval_algebraMap_apply, Subtype.ext_iff])

Premises used: Subtype.ext_iff, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Tower
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))
h :
  ∀ (x : E),
    Membership.mem (γ := Subalgebra C E) (Subalgebra.restrictScalars C (adjoin D S)) x ↔
      Membership.mem (γ := Subalgebra C E)
        (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
          (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S))
        x
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Adjoin.Tower
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
h 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
⊢ 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

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Adjoin.Tower
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
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))
⊢ 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))

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]
-- Module: Mathlib.RingTheory.Adjoin.Tower
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 (α := 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:
simp
-- Module: Mathlib.RingTheory.Adjoin.Tower
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) ⊤
rcases :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤),
    Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤

Tactic:
rcases hRS with ⟨s, hs⟩
-- Module: Mathlib.RingTheory.Adjoin.Tower
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)) ⊤
rcases :
  ∀ (t : Finset A) (ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤),
    Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤

Tactic:
rcases hSA with ⟨t, ht⟩
-- Module: Mathlib.RingTheory.Adjoin.Tower
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 := ↥⊤) ⊤) ⊤
rw₇ rw₈ : Eq.{u_3 + 1} (α := Subalgebra R A) ⊤ ⊤
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(Finset.image (⇑(algebraMap S A) : (a : S) → A) 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
       ]

Premises used: Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, Finset.coe_image, Algebra.adjoin_top, Subalgebra.restrictScalars_top, Finset.coe_union
-- Module: Mathlib.RingTheory.Adjoin.Tower
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)) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤

Tactic:
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
       ]
    ⟩
-- Module: Mathlib.RingTheory.Adjoin.Tower
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) ⊤
rcases :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤),
    Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
rcases₁ :
  ∀ (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)) ⊤), Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
⊢ 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
       ]
    ⟩
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
hAC : Subalgebra.FG.{w, u_1} (R := A) (A := C) ⊤
hBC : FG.{u₁, u_1} (R := B) (M := C) ⊤
obtain :
  ∀ (x : Finset C) (hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤),
    ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
obtain ⟨x, hx⟩ := hAC
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
hBC : FG.{u₁, u_1} (R := B) (M := C) ⊤
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
obtain :
  ∀ (y : Finset C) (hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤),
    ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
obtain ⟨y, hy⟩ := hBC
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
⊢ Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤

Tactic:
have := hy
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy this : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
⊢ ∀ (x : C), ∃ (f : C → B), Function.support f ⊆ (↑y : Set C) ∧ ∑ a ∈ y, f a • a = x

Tactic:
simp_rw [eq_top_iff', mem_span_finset] at this

Premises used: Submodule.eq_top_iff', Submodule.mem_span_finset
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
this : ∀ (x : C), ∃ (f : C → B), Function.support f ⊆ (↑y : Set C) ∧ ∑ a ∈ y, f a • a = x
choose :
  ∀ (f : (x : C) → C → B),
    (∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)) →
      ∀ (hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x), ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
choose f _ hf using this