awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : 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 : ↥(adjoin R (↑σ : Set S))
e :
  Eq (α := S) ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x : S)
    ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) y : S)
⊢ (↑1 : ↥(adjoin R (↑σ : Set S))) * x = (↑1 : ↥(adjoin R (↑σ : Set S))) * y

Tactic:
simpa using Subtype.ext e

Premises used: Subtype.ext
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : 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 : ↥(adjoin R (↑σ : Set S))
e :
  Eq (α := S) ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x : S)
    ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) y : S)
⊢ ∃ (c :
    ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))),
    (↑c : ↥(adjoin R (↑σ : Set S))) * x = (↑c : ↥(adjoin R (↑σ : Set S))) * y

Tactic:
exact ⟨1, by simpa using Subtype.ext e⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
simp_rw :
  EssFiniteType R S ↔
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S
⊢ EssFiniteType R S ↔
    ∃ (σ : 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)

Tactic:
simp_rw [← essFiniteType_cond_iff]

Premises used: Algebra.essFiniteType_cond_iff
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
mp :
  EssFiniteType R S →
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S
mpr :
  (∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S) →
    EssFiniteType R S
⊢ EssFiniteType R S ↔
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S

Tactic:
constructor
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType R S →
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S

Tactic:
fun ⟨a, b⟩ ↦ ⟨a, b⟩

Premises used: IsLocalization, Algebra.algebraMap, Algebra.adjoin, Membership.mem, IsUnit.submonoid, Exists, Subtype, Submonoid.comap, SetLike.coe, _private.0.Algebra.essFiniteType_iff.match_1, Exists.intro
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType R S →
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S

Tactic:
exact fun ⟨a, b⟩ ↦ ⟨a, b⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ (∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S) →
    EssFiniteType R S

Tactic:
fun ⟨a, b⟩ ↦ ⟨a, b⟩

Premises used: Algebra.EssFiniteType, Exists.intro, Algebra.EssFiniteType.mk, _private.0.Algebra.essFiniteType_iff.match_2
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ (∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S) →
    EssFiniteType R S

Tactic:
exact fun ⟨a, b⟩ ↦ ⟨a, b⟩
-- 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 : FiniteType R S
obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), EssFiniteType R S
⊢ EssFiniteType R S

Tactic:
obtain ⟨s, hs⟩ := ‹FiniteType R S›

Premises used: Algebra.FiniteType
-- 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 : FiniteType R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
rw :
  ∃ (σ : 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)
⊢ EssFiniteType R S

Tactic:
rw [essFiniteType_iff]

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 : FiniteType R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
x : 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)) (x * t)

Tactic:
simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩

Premises used: Algebra.mem_top, and_true, true_and
-- 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 : FiniteType R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ ∃ (σ : 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)

Tactic:
exact ⟨s, fun _ ↦ by simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
rw :
  ∃ (σ : 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)
⊢ EssFiniteType R S

Tactic:
rw [essFiniteType_iff]

Premises used: Algebra.essFiniteType_iff
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M 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 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)

Tactic:
use ∅
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
h :
  ∀ (s : S),
    ∃ (a : R),
      IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) a : S) ∧
        ∃ (y : R), (algebraMap R S : (a : R) → S) y = HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) a : 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)

Tactic:
simp only [Finset.coe_empty, Algebra.adjoin_empty, Algebra.mem_bot,
    Set.mem_range, exists_exists_eq_and]

Premises used: Set.mem_range, Finset.coe_empty, Algebra.mem_bot, exists_exists_eq_and, Algebra.adjoin_empty
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : S
h :
  ∀ (x : R) (t : ↥M)
    (e :
      HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(x, t).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (x, t).1),
    ∃ (a : R),
      IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) a : S) ∧
        ∃ (y : R), (algebraMap R S : (a : R) → S) y = HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) a : S)
⊢ ∃ (a : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) a : S) ∧
      ∃ (y : R), (algebraMap R S : (a : R) → S) y = HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) a : S)

Tactic:
obtain ⟨⟨x, t⟩, e⟩ := IsLocalization.surj M s

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : S
x : R
t : ↥M
e : HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(x, t).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, t).1
⊢ ∃ (a : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) a : S) ∧
      ∃ (y : R), (algebraMap R S : (a : R) → S) y = HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) a : S)

Tactic:
⟨_, IsLocalization.map_units S t, x, e.symm⟩

Premises used: And.intro, Exists.intro, IsLocalization.map_units, Eq.symm
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : S
x : R
t : ↥M
e : HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(x, t).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, t).1
⊢ ∃ (a : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) a : S) ∧
      ∃ (y : R), (algebraMap R S : (a : R) → S) y = HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) a : S)

Tactic:
exact ⟨_, IsLocalization.map_units S t, x, e.symm⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
inst : CommRing R
⊢ EssFiniteType R R

Tactic:
inferInstance

Premises used: inferInstance
-- 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
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)

Tactic:
Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht

Premises used: Algebra.adjoin_induction
-- 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
refine_1 :
  ∀ (x : T) (hx : x ∈ τ),
    ∃ s ∈ σ,
      IsUnit s ∧
        Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • x)
refine_2 :
  ∀ (r : S),
    ∃ s ∈ σ,
      IsUnit s ∧
        Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
          (HSMul.hSMul (β := T) s ((algebraMap S T : (a : S) → T) r : T))
refine_3 :
  ∀ (x y : T) (hx : Membership.mem (γ := Subalgebra S T) (adjoin S τ) x)
    (hy : Membership.mem (γ := Subalgebra S T) (adjoin S τ) y),
    (∃ s ∈ σ,
        IsUnit s ∧
          Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • x)) →
      (∃ s ∈ σ,
          IsUnit s ∧
            Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
              (s • y)) →
        ∃ s ∈ σ,
          IsUnit s ∧
            Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
              (s • (x + y))
refine_4 :
  ∀ (x y : T) (hx : Membership.mem (γ := Subalgebra S T) (adjoin S τ) x)
    (hy : Membership.mem (γ := Subalgebra S T) (adjoin S τ) y),
    (∃ s ∈ σ,
        IsUnit s ∧
          Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • x)) →
      (∃ s ∈ σ,
          IsUnit s ∧
            Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
              (s • y)) →
        ∃ s ∈ σ,
          IsUnit s ∧
            Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
              (s • (x * y))
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)

Tactic:
refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
-- 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_1 : T
ht_1 : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t_1
t : T
ht : t ∈ τ
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)

Tactic:
⟨1, Subalgebra.one_mem _, isUnit_one,
      (one_smul S t).symm ▸ Algebra.mem_sup_right (Algebra.subset_adjoin ht)⟩

Premises used: Algebra.subset_adjoin, Eq.rec, one_smul, isUnit_one, And.intro, Exists.intro, Algebra.mem_sup_right, OfNat.ofNat, Eq.symm, Subalgebra.one_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_1 : T
ht_1 : Membership.mem (γ := Subalgebra S T) (adjoin S τ) t_1
t : T
ht : t ∈ τ
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)

Tactic:
exact ⟨1, Subalgebra.one_mem _, isUnit_one,
      (one_smul S t).symm ▸ Algebra.mem_sup_right (Algebra.subset_adjoin ht)⟩
-- 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
s : S
refine_2 :
  ∀ (s' : S) (hs₁ : s' ∈ σ) (hs₂ : IsUnit s') (hs₃ : s * s' ∈ σ),
    ∃ s_1 ∈ σ,
      IsUnit s_1 ∧
        Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
          (HSMul.hSMul (β := T) s_1 ((algebraMap S T : (a : S) → T) s : T))
⊢ ∃ s_1 ∈ σ,
    IsUnit s_1 ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
        (HSMul.hSMul (β := T) s_1 ((algebraMap S T : (a : S) → T) s : T))

Tactic:
obtain ⟨s', hs₁, hs₂, hs₃⟩ := hσ s
-- 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
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
⊢ ∃ s_1 ∈ σ,
    IsUnit s_1 ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
        (HSMul.hSMul (β := T) s_1 ((algebraMap S T : (a : S) → T) s : T))

Tactic:
⟨_, hs₁, hs₂, Algebra.mem_sup_left ?_⟩

Premises used: Algebra.mem_sup_left, 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
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
refine_2 :
  Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    (HSMul.hSMul (β := T) s' ((algebraMap S T : (a : S) → T) s : T))
⊢ ∃ s_1 ∈ σ,
    IsUnit s_1 ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
        (HSMul.hSMul (β := T) s_1 ((algebraMap S T : (a : S) → T) s : T))

Tactic:
refine ⟨_, hs₁, hs₂, Algebra.mem_sup_left ?_⟩
-- 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
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
refine_2 :
  Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    ((algebraMap S T : (a : S) → T) (s * s') : T)
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    (HSMul.hSMul (β := T) s' ((algebraMap S T : (a : S) → T) s : T))

Tactic:
rw [Algebra.smul_def, ← map_mul, mul_comm]

Premises used: map_mul, mul_comm, Algebra.smul_def
-- 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
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    ((algebraMap S T : (a : S) → T) (s * s') : T)

Tactic:
⟨_, hs₃, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
s s' : S
hs₁ : s' ∈ σ
hs₂ : IsUnit s'
hs₃ : s * s' ∈ σ
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    ((algebraMap S T : (a : S) → T) (s * s') : T)

Tactic:
exact ⟨_, hs₃, 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_3 :
  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_3 :
  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))
⊢ Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
    ((sx * sy) • (x + y))

Tactic:
rw [smul_add, mul_smul, mul_smul, Algebra.smul_def sx (sy • y), smul_comm,
      Algebra.smul_def sy (sx • x)]

Premises used: HSMul.hSMul, Algebra.smul_def, SMulCommClass.smul_comm, SemigroupAction.mul_smul, smul_add