awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
⊢ ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi

Tactic:
have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
rw :
  insert 1 (↑y : Set C) * insert 1 (↑y : Set C) ⊆
    (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
⊢ HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)

Tactic:
rw [span_mul_span, span_le, coe_insert]

Premises used: Submodule.span_mul_span, Finset.coe_insert, Submodule.span_le
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
inl : 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
⊢ HMul.hMul (α := C) 1 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
rw [mul_one]

Premises used: mul_one
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
subset_span (Set.mem_insert _ _)

Premises used: Set.Mem, Set.mem_insert, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
exact subset_span (Set.mem_insert _ _)

Premises used: Set.mem_insert, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yj : C
hyj : yj ∈ (↑y : Set C)
inl : yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
⊢ 1 * yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
subset_span (Set.mem_insert_of_mem _ hyj)

Premises used: Set.Mem, Set.mem_insert_of_mem, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
exact subset_span (Set.mem_insert_of_mem _ hyj)

Premises used: Set.mem_insert_of_mem, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
inr : yi ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
⊢ yi * 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
rw [mul_one]

Premises used: mul_one
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
⊢ yi ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
subset_span (Set.mem_insert_of_mem _ hyi)

Premises used: Set.Mem, Set.mem_insert_of_mem, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
⊢ yi ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
exact subset_span (Set.mem_insert_of_mem _ hyi)

Premises used: Set.mem_insert_of_mem, Submodule.subset_span
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
yj : C
hyj : yj ∈ (↑y : Set C)
inr : ∑ a ∈ y, f (yi * yj) a • a ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
⊢ yi * yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
rw [← hf (yi * yj)]

Premises used: HMul.hMul
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ ∑ a ∈ y, f (yi * yj) a • a ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))

Premises used: Iff.mpr, HMul.hMul, Algebra.subset_adjoin, Algebra.adjoin, Membership.mem, Set.mem_insert_of_mem, Subtype, Insert.insert, Finset.mem_image₂_of_mem, Subtype.mk, SetLike.coe, SetLike.mem_coe, Submodule.span, Submodule.subset_span, Finset.mem_union_right, OfNat.ofNat, sum_mem, Submodule.smul_mem, Finset.mul_mem_mul
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ ∑ a ∈ y, f (yi * yj) a • a ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)

Tactic:
exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))

Premises used: Iff.mpr, SetLike.mem_coe, sum_mem
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)

Tactic:
have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩

Premises used: Algebra.adjoin, Subalgebra.fg_adjoin_finset, Insert.insert, SetLike.coe, And.intro, Exists.intro, OfNat.ofNat
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
refine :
  Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤

Tactic:
refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤

Tactic:
restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _

Premises used: Algebra.adjoin, Membership.mem, Subtype, Submodule.restrictScalars_injective, SetLike.coe
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
convert_3 :
  Eq (α := Submodule A C)
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)))
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B))) ⊤)
⊢ Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤

Tactic:
convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _

Premises used: Algebra.adjoin, Membership.mem, Subtype, Submodule.restrictScalars_injective, SetLike.coe
-- 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)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
convert_3 :
  (↑(Submonoid.closure (↑x : Set C)) : Set C) ⊆
    (↑(restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))) :
      Set C)
⊢ Eq (α := Submodule A C)
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)))
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B))) ⊤)

Tactic:
rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]

Premises used: eq_top_iff, Submodule.restrictScalars_top, Algebra.top_toSubmodule, Algebra.adjoin_eq_span, Submodule.span_le