awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x_1 : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x
⊢ Membership.mem (α := T ⊗[R] S) (γ := Subalgebra R (T ⊗[R] S))
    (Subalgebra.map TensorProduct.includeRight (adjoin R (↑σ : Set S)))
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) x : T ⊗[R] S)

Tactic:
have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x_1 : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x
this :
  Membership.mem (α := T ⊗[R] S) (γ := Subalgebra R (T ⊗[R] S))
    (Subalgebra.map TensorProduct.includeRight (adjoin R (↑σ : Set S)))
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) x : T ⊗[R] S)
rw :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T
      (↑(adjoin R (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) :
        Set (T ⊗[R] S)))
    (1 ⊗ₜ[R] x)
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)

Tactic:
rw [← Algebra.adjoin_adjoin_of_tower R]

Premises used: Algebra.adjoin_adjoin_of_tower
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x_1 : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x
this :
  Membership.mem (α := T ⊗[R] S) (γ := Subalgebra R (T ⊗[R] S))
    (Subalgebra.map TensorProduct.includeRight (adjoin R (↑σ : Set S)))
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) x : T ⊗[R] S)
a :
  1 ⊗ₜ[R] x ∈
    (↑(adjoin R (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) :
      Set (T ⊗[R] S))
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T
      (↑(adjoin R (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) :
        Set (T ⊗[R] S)))
    (1 ⊗ₜ[R] x)

Tactic:
apply Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x_1 : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x
this :
  Membership.mem (α := T ⊗[R] S) (γ := Subalgebra R (T ⊗[R] S))
    (Subalgebra.map TensorProduct.includeRight (adjoin R (↑σ : Set S)))
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) x : T ⊗[R] S)
⊢ 1 ⊗ₜ[R] x ∈
    (↑(adjoin R (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) :
      Set (T ⊗[R] S))

Tactic:
simpa [← Algebra.adjoin_image] using this

Premises used: Algebra.adjoin_image
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
⊢ ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)

Tactic:
have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          (x ⊗ₜ[R] y * t)

Tactic:
⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩

Premises used: And.intro, Exists.intro, IsUnit.map, DFunLike.coe, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
h :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    (HMul.hMul (α := T ⊗[R] S) (β := T ⊗[R] S) (x ⊗ₜ[R] y)
      ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) t : T ⊗[R] S))
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          (x ⊗ₜ[R] y * t)

Tactic:
refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
h :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x ⊗ₜ[R] (y * t))
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    (HMul.hMul (α := T ⊗[R] S) (β := T ⊗[R] S) (x ⊗ₜ[R] y)
      ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) t : T ⊗[R] S))

Tactic:
simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]

Premises used: Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
h :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    (HSMul.hSMul (β := T ⊗[R] S) x (1 ⊗ₜ[R] (y * t)))
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x ⊗ₜ[R] (y * t))

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
h :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] (y * t))
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    (HSMul.hSMul (β := T ⊗[R] S) x (1 ⊗ₜ[R] (y * t)))

Tactic:
apply Subalgebra.smul_mem

Premises used: Subalgebra.smul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] (y * t))

Tactic:
H _ h₃

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x : T
y t : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t
h₂ : IsUnit t
h₃ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (y * t)
H :
  ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] (y * t))

Tactic:
exact H _ h₃
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x y : T ⊗[R] S
hx :
  ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * t)
hy :
  ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * t)
h :
  ∀ (tx : T ⊗[R] S)
    (hx₁ :
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) tx)
    (hx₂ : IsUnit tx)
    (hx₃ :
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * tx)),
    ∃ (t : T ⊗[R] S),
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
        IsUnit t ∧
          Membership.mem (γ := Subalgebra T (T ⊗[R] S))
            (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
            ((x + y) * t)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          ((x + y) * t)

Tactic:
obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x y : T ⊗[R] S
hy :
  ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * t)
tx : T ⊗[R] S
hx₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) tx
hx₂ : IsUnit tx
hx₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * tx)
h :
  ∀ (ty : T ⊗[R] S)
    (hy₁ :
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) ty)
    (hy₂ : IsUnit ty)
    (hy₃ :
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * ty)),
    ∃ (t : T ⊗[R] S),
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
        IsUnit t ∧
          Membership.mem (γ := Subalgebra T (T ⊗[R] S))
            (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
            ((x + y) * t)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          ((x + y) * t)

Tactic:
obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x y tx : T ⊗[R] S
hx₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) tx
hx₂ : IsUnit tx
hx₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * tx)
ty : T ⊗[R] S
hy₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) ty
hy₂ : IsUnit ty
hy₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * ty)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          ((x + y) * t)

Tactic:
⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩

Premises used: IsUnit.mul, And.intro, Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
x y tx : T ⊗[R] S
hx₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) tx
hx₂ : IsUnit tx
hx₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * tx)
ty : T ⊗[R] S
hy₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) ty
hy₂ : IsUnit ty
hy₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * ty)
h :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    ((x + y) * (tx * ty))
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          ((x + y) * t)

Tactic:
refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩