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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
apply :
  Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sy : T)
apply₁ :
  Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sx : T)
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) sy : T) (sx • x) +
      HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) sx : T) (sy • y))

Tactic:
apply add_mem (mul_mem _ hsx'') (mul_mem _ hsy'')

Premises used: AddMemClass.add_mem, 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sy : T)

Tactic:
Algebra.mem_sup_left ⟨_, ‹_›, rfl⟩

Premises used: Algebra.mem_sup_left, And.intro, Exists.intro, 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sy : T)

Tactic:
exact Algebra.mem_sup_left ⟨_, ‹_›, 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sx : T)

Tactic:
Algebra.mem_sup_left ⟨_, ‹_›, rfl⟩

Premises used: Algebra.mem_sup_left, And.intro, Exists.intro, 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((algebraMap S T : (a : S) → T) sx : T)

Tactic:
exact Algebra.mem_sup_left ⟨_, ‹_›, 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • (x * y))

Tactic:
⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩

Premises used: Subalgebra.mul_mem, IsUnit.mul, And.intro, Exists.intro
-- 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
refine_4 :
  Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((sx * sy) • (x * y))
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • (x * y))

Tactic:
refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
-- 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
refine_4 :
  Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x * sy • y)
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((sx * sy) • (x * y))

Tactic:
rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]

Premises used: smul_assoc, smul_eq_mul, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x * sy • y)

Tactic:
mul_mem hsx'' hsy''

Premises used: 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x)
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sy • y)
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x * sy • y)

Tactic:
exact mul_mem hsx'' hsy''

Premises used: 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
h₁ : EssFiniteType R S
h₂ : EssFiniteType S T
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))
    (h₂ :
      ∃ (σ : Finset T),
        ∀ (s : T),
          ∃ (t : T),
            Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
              IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)),
    ∃ (σ : Finset T),
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
⊢ EssFiniteType R T

Tactic:
rw [essFiniteType_iff] at h₁ h₂ ⊢

Premises used: Algebra.essFiniteType_iff
-- 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₁ :
  ∃ (σ : 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)
h₂ :
  ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
obtain :
  ∀ (s : Finset S)
    (hs :
      ∀ (s_1 : S),
        ∃ (t : S),
          Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)),
    ∃ (σ : Finset T),
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
⊢ ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)

Tactic:
obtain ⟨s, hs⟩ := 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
h₂ :
  ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
obtain :
  ∀ (t : Finset T)
    (ht :
      ∀ (s : T),
        ∃ (t_1 : T),
          Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
            IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)),
    ∃ (σ : Finset T),
      ∀ (s : T),
        ∃ (t : T),
          Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
⊢ ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)

Tactic:
obtain ⟨t, ht⟩ := 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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
h :
  ∀ (s_1 : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (adjoin R (↑(Finset.image (⇑(IsScalarTower.toAlgHom R S T) : (a : S) → T) s ∪ t) : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (adjoin R (↑(Finset.image (⇑(IsScalarTower.toAlgHom R S T) : (a : S) → T) s ∪ t) : Set T)) (s_1 * t_1)
⊢ ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)

Tactic:
use s.image (IsScalarTower.toAlgHom R S T) ∪ t

Premises used: IsScalarTower.toAlgHom, DFunLike.coe, Finset.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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
h :
  ∀ (s_1 : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (s_1 * t_1)
⊢ ∀ (s_1 : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (adjoin R (↑(Finset.image (⇑(IsScalarTower.toAlgHom R S T) : (a : S) → T) s ∪ t) : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (adjoin R (↑(Finset.image (⇑(IsScalarTower.toAlgHom R S T) : (a : S) → T) s ∪ t) : Set T)) (s_1 * t_1)

Tactic:
simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]

Premises used: Algebra.adjoin_union, Finset.coe_image, Algebra.adjoin_image, Finset.coe_union
-- 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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x : T
h :
  ∀ (y : T) (hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y) (hy₂ : IsUnit y)
    (hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)
⊢ ∃ (t_1 : T),
    Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
      IsUnit t_1 ∧
        Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)

Tactic:
obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
-- 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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
h :
  ∀ (t₁ : S) (h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁) (h₂ : IsUnit t₁)
    (h₃ :
      Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)
⊢ ∃ (t_1 : T),
    Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
      IsUnit t_1 ∧
        Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)

Tactic:
obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁

Premises used: Algebra.EssFiniteType.aux
-- 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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
h :
  ∀ (t₂ : S) (h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂) (h₅ : IsUnit t₂)
    (h₆ :
      Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧
          Membership.mem (γ := Subalgebra R T)
            (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)
⊢ ∃ (t_1 : T),
    Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
      IsUnit t_1 ∧
        Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)

Tactic:
obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃

Premises used: Algebra.EssFiniteType.aux
-- 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
s : Finset S
hs :
  ∀ (s_1 : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) (s_1 * t)
t : Finset T
ht :
  ∀ (s : T),
    ∃ (t_1 : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) t_1 ∧
        IsUnit t_1 ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (s * t_1)
x y : T
hy₁ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra S T) (adjoin S (↑t : Set T)) (x * y)
t₁ : S
h₁ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₁
h₂ : IsUnit t₁
h₃ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₁ • y)
t₂ : S
h₄ : Membership.mem (γ := Subalgebra R S) (adjoin R (↑s : Set S)) t₂
h₅ : IsUnit t₂
h₆ :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • (x * y))
⊢ ∃ (t_1 : T),
    Membership.mem (γ := Subalgebra R T)
        (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) t_1 ∧
      IsUnit t_1 ∧
        Membership.mem (γ := Subalgebra R T)
          (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t_1)

Tactic:
⟨t₂ • t₁ • y, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, HSMul.hSMul