-- 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
h : EssFiniteType R S
rw rw₁ 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)
rw₃ :
  ∀ (σ : 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)
h₁ h₂ :
  ∀ (σ : 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),
    ∃ (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)
⊢ EssFiniteType T (T ⊗[R] S)

Tactic:
classical
  rw [essFiniteType_iff] at h ⊢
  obtain ⟨σ, hσ⟩ := h
  use σ.image Algebra.TensorProduct.includeRight
  intro s
  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, Algebra.essFiniteType_iff