-- 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)
s : T ⊗[R] S
h :
  ∃ (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))) (0 * t)
h₁ :
  ∀ (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)
h₂ :
  ∀ (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)
⊢ ∃ (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:
induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    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
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)

Premises used: add_mul, Algebra.TensorProduct.includeRight_apply, mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, Subalgebra.smul_mem, TensorProduct.smul_tmul', smul_eq_mul, mul_one