awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ (↑(adjoin R s) : Set A)
hb : (a, b).2 ∈ (↑(adjoin R t) : Set B)
P : Subalgebra R (A × B) :=
  adjoin R
    ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪ (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
Hb : (0, b) ∈ P
⊢ Membership.mem (γ := Subalgebra R (A × B))
    (adjoin R
      ((⇑(LinearMap.inl R A B) : (a : A) → A × B) '' (s ∪ {1}) ∪
        (⇑(LinearMap.inr R A B) : (a : B) → A × B) '' (t ∪ {1})))
    (a, b)

Tactic:
simpa [P] using Subalgebra.add_mem _ Ha Hb

Premises used: Subalgebra.add_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set S
⊢ Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' s))
    (Subalgebra.map (IsScalarTower.toAlgHom R S A) (adjoin R s))

Tactic:
adjoin_image R (IsScalarTower.toAlgHom R S A) s

Premises used: IsScalarTower.toAlgHom, Algebra.adjoin_image
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' s ∪ t))
    (Subalgebra.restrictScalars.{uR, uS, uA} R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t))

Tactic:
le_antisymm
    (closure_mono <|
      Set.union_subset (Set.range_subset_iff.2 fun r => Or.inl ⟨algebraMap R (adjoin R s) r,
        (IsScalarTower.algebraMap_apply _ _ _ _).symm⟩)
        (Set.union_subset_union_left _ fun _ ⟨_x, hx, hxs⟩ => hxs ▸ ⟨⟨_, subset_adjoin hx⟩, rfl⟩))
    (closure_le.2 <|
      Set.union_subset (Set.range_subset_iff.2 fun x => adjoin_mono Set.subset_union_left <|
        Algebra.adjoin_algebraMap R A s ▸ ⟨x, x.prop, rfl⟩)
        (Set.Subset.trans Set.subset_union_right subset_adjoin))

Premises used: Iff.mpr, Subsemiring.closure_le, Subsemiring.closure_mono, Algebra.algebraMap, Set.Subset.trans, Algebra.subset_adjoin, Set.subset_union_right, Algebra.adjoin, Membership.mem, Eq.rec, Subtype, Subtype.mk, Set.union_subset, Set.subset_union_left, le_antisymm, Algebra.adjoin_mono, Subtype.prop, And.intro, Exists.intro, Algebra.adjoin_algebraMap, Set.union_subset_union_left, Or.inl, Set.range, Set.range_subset_iff, _private.0.Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin.match_1, Eq.symm, Subtype.val, DFunLike.coe, IsScalarTower.algebraMap_apply, rfl
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
apply : LE.le (α := Subalgebra S A) (adjoin S s) (adjoin S (↑(adjoin R s) : Set A))
apply₁ : (↑(adjoin R s) : Set A) ⊆ (↑(adjoin S s) : Set A)
⊢ Eq (α := Subalgebra S A) (adjoin S (↑(adjoin R s) : Set A)) (adjoin S s)

Tactic:
apply le_antisymm (adjoin_le _)

Premises used: le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ LE.le (α := Subalgebra S A) (adjoin S s) (adjoin S (↑(adjoin R s) : Set A))

Tactic:
adjoin_mono subset_adjoin

Premises used: Algebra.subset_adjoin, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ LE.le (α := Subalgebra S A) (adjoin S s) (adjoin S (↑(adjoin R s) : Set A))

Tactic:
exact adjoin_mono subset_adjoin

Premises used: Algebra.subset_adjoin, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ LE.le (α := Subalgebra R A) (adjoin R s) (Subalgebra.restrictScalars R (adjoin S s))

Tactic:
adjoin_le subset_adjoin

Premises used: Algebra.subset_adjoin, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ LE.le (α := Subalgebra R A) (adjoin R s) (Subalgebra.restrictScalars R (adjoin S s))

Tactic:
exact adjoin_le subset_adjoin

Premises used: Algebra.subset_adjoin, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
⊢ Eq (α := Subalgebra R A) (Subalgebra.restrictScalars R (adjoin S s))
    (AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R s)

Tactic:
le_antisymm (fun _ hx ↦ adjoin_induction
    (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
    (fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩)
    (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
    (Subalgebra.mem_restrictScalars _).mp hx) (sup_le ?_ <| adjoin_le subset_adjoin)

Premises used: Algebra.subset_adjoin, le_antisymm, Algebra.adjoin_le, sup_le
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
refine :
  LE.le (α := Subalgebra R A) (AlgHom.range (IsScalarTower.toAlgHom R S A)) (Subalgebra.restrictScalars R (adjoin S s))
⊢ Eq (α := Subalgebra R A) (Subalgebra.restrictScalars R (adjoin S s))
    (AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R s)

Tactic:
refine le_antisymm (fun _ hx ↦ adjoin_induction
    (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
    (fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩)
    (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
    (Subalgebra.mem_restrictScalars _).mp hx) (sup_le ?_ <| adjoin_le subset_adjoin)

Premises used: Algebra.subset_adjoin, le_antisymm, Algebra.adjoin_le, sup_le
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
x : S
⊢ Membership.mem (α := A) (γ := Subalgebra R A) (Subalgebra.restrictScalars R (adjoin S s))
    ((AlgHom.toRingHom (IsScalarTower.toAlgHom R S A) : (a : S) → A) x : A)

Tactic:
algebraMap_mem (adjoin S s) x

Premises used: Set.Mem, Algebra.adjoin, algebraMap_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
s : Set A
x : S
⊢ Membership.mem (α := A) (γ := Subalgebra R A) (Subalgebra.restrictScalars R (adjoin S s))
    ((AlgHom.toRingHom (IsScalarTower.toAlgHom R S A) : (a : S) → A) x : A)

Tactic:
exact algebraMap_mem (adjoin S s) x

Premises used: Algebra.adjoin, algebraMap_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra S A
t : Set A
⊢ Eq (α := Subalgebra.{uS, u_1} (↥⊤) A) (adjoin (↥⊤) t) (Subalgebra.restrictScalars (↥⊤) (adjoin S t))

Tactic:
let equivTop : Subalgebra (⊤ : Subalgebra R S) A ≃o Subalgebra S A :=
    { toFun := fun s => { s with algebraMap_mem' := fun r => s.algebraMap_mem ⟨r, trivial⟩ }
      invFun := fun s => s.restrictScalars _
      left_inv := fun _ => SetLike.coe_injective rfl
      right_inv := fun _ => SetLike.coe_injective rfl
      map_rel_iff' := @fun _ _ => Iff.rfl }
  le_antisymm
    (adjoin_le <| show t ⊆ adjoin S t from subset_adjoin)
    (equivTop.symm_apply_le.mpr <|
      adjoin_le <| show t ⊆ adjoin (⊤ : Subalgebra R S) t from subset_adjoin)

Premises used: Iff.mpr, trivial, RelIso.mk, Iff.rfl, Algebra.subset_adjoin, Membership.mem, Equiv.mk, Subtype, Subalgebra.toSubsemiring, SetLike.coe_injective, Subtype.mk, le_antisymm, OrderIso.symm_apply_le, Algebra.adjoin_le, Subalgebra.algebraMap_mem, Top.top, Subalgebra.restrictScalars, rfl, Subalgebra.mk
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (s ∪ t))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t))

Tactic:
simpa using adjoin_algebraMap_image_union_eq_adjoin_adjoin R s t

Premises used: Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
⊢ Eq (α := Subalgebra R B) (Subalgebra.map (IsScalarTower.toAlgHom R A B) (adjoin R s))
    (Subalgebra.map (IsScalarTower.toAlgHom R A B) ⊤)

Tactic:
have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom R A B)) hS
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (Subalgebra.map (IsScalarTower.toAlgHom R A B) (adjoin R s))
    (Subalgebra.map (IsScalarTower.toAlgHom R A B) ⊤)
⊢ Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
    (AlgHom.range (IsScalarTower.toAlgHom R A B))

Tactic:
rw [Algebra.map_top, AlgHom.map_adjoin, IsScalarTower.coe_toAlgHom'] at this

Premises used: IsScalarTower.coe_toAlgHom', AlgHom.map_adjoin, Algebra.map_top
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
s : Set A
t : Set B
hS : Eq (α := Subalgebra R A) (adjoin R s) ⊤
this :
  Eq (α := Subalgebra R B) (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))
    (AlgHom.range (IsScalarTower.toAlgHom R A B))
rw :
  Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s)))
      (adjoin (↥(adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s))) t))
rw₁ :
  Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
      (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
rw₂ rw₃ :
  Eq (α := Subalgebra R B)
    (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
      (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
    (Subalgebra.restrictScalars R (S := ↥(AlgHom.range (IsScalarTower.toAlgHom R A B)))
      (adjoin (↥(AlgHom.range (IsScalarTower.toAlgHom R A B))) t))
⊢ Eq (α := Subalgebra R B) (Subalgebra.restrictScalars R (adjoin A t))
    (adjoin R ((⇑(algebraMap A B) : (a : A) → B) '' s ∪ t))

Tactic:
rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]

Premises used: IsScalarTower.adjoin_range_toAlgHom, Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (adjoin R s) x
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) (adjoin R s) : Submodule R B) x

Tactic:
change x ∈ Subalgebra.toSubmodule (adjoin R s) at hx

Premises used: Algebra.adjoin, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
hx :
  Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) (adjoin R s) : Submodule R B) x
⊢ ∃ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
    (Finsupp.linearCombination R (Subtype.val (p := fun (x : B) ↦ x ∈ (↑(Submonoid.closure s) : Set B))) :
          (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB) →₀ R) → B)
        l =
      x

Tactic:
rw [adjoin_eq_span, Finsupp.mem_span_iff_linearCombination] at hx

Premises used: Finsupp.mem_span_iff_linearCombination, Algebra.adjoin_eq_span
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
x : B
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
hx :
  ∃ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
    (Finsupp.linearCombination R (Subtype.val (p := fun (x : B) ↦ x ∈ (↑(Submonoid.closure s) : Set B))) :
          (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB) →₀ R) → B)
        l =
      x
rcases :
  ∀ (l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R),
    ∃ (n₀ : ℕ),
      ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ B'

Tactic:
rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
choose :
  ∀ (n₁ : (x : ↥(Submonoid.closure s)) → ℕ)
    (n₂ :
      ∀ (x : ↥(Submonoid.closure s)),
        Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))),
    ∃ (n₀ : ℕ),
      ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
⊢ ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'

Tactic:
choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop

Premises used: Subtype.prop, Submonoid.pow_smul_mem_closure_smul
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
h :
  ∀ n ≥ l.support.sup n₁,
    HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'
⊢ ∃ (n₀ : ℕ),
    ∀ n ≥ n₀, HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'

Tactic:
use l.support.sup n₁

Premises used: Finsupp.support, Finset.sup
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
h : (l.sum fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) ∈ B'
⊢ HSMul.hSMul (β := B) (r ^ n) (l.sum fun (i : ↥(Submonoid.closure s)) (c : R) ↦ c • (↑i : B)) ∈ B'

Tactic:
rw [Finsupp.smul_sum]

Premises used: Finsupp.smul_sum
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ (l.sum fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) ∈ B'

Tactic:
B'.toSubmodule.sum_mem ?_

Premises used: Set.Mem, Submodule.sum_mem, Finsupp.sum, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
h :
  ∀ c ∈ l.support,
    Membership.mem (γ := Submodule R B)
      ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
      ((fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) c
        ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) c))
⊢ (l.sum fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) ∈ B'

Tactic:
refine B'.toSubmodule.sum_mem ?_

Premises used: Submodule.sum_mem, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
⊢ n ≥ n₁ a

Tactic:
have : n ≥ n₁ a := le_trans (Finset.le_sup ha) hn
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
h :
  Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    (r ^ n •
      HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R) (↑a : B))
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    ((fun (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) (b : R) ↦ r ^ n • b • (↑a : B)) a
      ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a))

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
h :
  Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    (HPow.hPow (α := B) ((algebraMap A B : (a : A) → B) r : B) (n - n₁ a) *
      HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
        (r ^ n₁ a • (↑a : B)))
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    (r ^ n •
      HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R) (↑a : B))

Tactic:
rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, ←
    IsScalarTower.algebraMap_smul A (l a) (a : B), smul_smul (r ^ n₁ a), mul_comm, ← smul_smul,
    smul_def, map_pow, IsScalarTower.algebraMap_smul]

Premises used: pow_add, smul_smul, tsub_add_cancel_of_le, map_pow, IsScalarTower.algebraMap_smul, HPow.hPow, mul_comm, Algebra.smul_def, Subtype.val, DFunLike.coe