awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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
h : EssFiniteType R S
⊢ EssFiniteType T (T ⊗[R] S)
have rw : ∀
  (h :
    ∃ (σ : Finset S),
      ∀ (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)),
  ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
Tactic: rw [essFiniteType_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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
h :
  ∃ (σ : Finset S),
    ∀ (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)
⊢ ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
have obtain : ∀ (σ : 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)),
  ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
Tactic: obtain ⟨σ, hσ⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
⊢ ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
have h : ∀ (s : 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))) (s * t)
Tactic: use σ.image Algebra.TensorProduct.includeRight
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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 : 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)
have h : ∀ (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)),
  ∃ (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: obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
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 (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (1 ⊗ₜ[R] x)
have 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)
Tactic: have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Algebra.adjoin_adjoin_of_tower R]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
⊢ 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)
have a : 1 ⊗ₜ[R] x ∈
  (↑(adjoin R (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) : Set (T ⊗[R] S))
Tactic: apply Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (hypothesis)
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)
⊢ ∃ (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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
have 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))
Tactic: refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)))
    (HMul.hMul (α := T ⊗[R] S) (β := T ⊗[R] S) (x ⊗ₜ[R] y)
      ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) t : T ⊗[R] S))
have 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))
Tactic: simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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))) (x ⊗ₜ[R] (y * t))
have 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)))
Tactic: rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)))
    (HSMul.hSMul (β := T ⊗[R] S) x (1 ⊗ₜ[R] (y * t)))
have 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))
Tactic: apply Subalgebra.smul_mem
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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)
have 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))
Tactic: refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩