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
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ EssFiniteType R S
have 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)
Tactic: rw [essFiniteType_iff]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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
⊢ ∃ (σ : 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)
have 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)
Tactic: use ∅
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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),
    ∃ (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)
have 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)
Tactic: simp only [Finset.coe_empty, Algebra.adjoin_empty, Algebra.mem_bot,
    Set.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨⟨x, t⟩, e⟩ := IsLocalization.surj M s
-- 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
σ : 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)
have 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)
Tactic: refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
-- 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
σ : 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)
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)
have 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))
Tactic: refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
-- 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
σ : 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))
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)
have 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))
Tactic: refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
-- 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
σ : 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))
⊢ ∃ s ∈ σ,
    IsUnit s ∧
      Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (s • t)
have 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))
Tactic: refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht
-- 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
σ : 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_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))
have 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))
Tactic: obtain ⟨s', hs₁, hs₂, hs₃⟩ := hσ s
-- 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
σ : 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))
have 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))
Tactic: refine ⟨_, hs₁, hs₂, Algebra.mem_sup_left ?_⟩
-- 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
σ : 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 (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
    (HSMul.hSMul (β := T) s' ((algebraMap S T : (a : S) → T) s : T))
have refine_2 : Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ)
  ((algebraMap S T : (a : S) → T) (s * s') : T)
Tactic: rw [Algebra.smul_def, ← map_mul, mul_comm]
-- 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
σ : 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))
have refine_3 : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
  ((sx * sy) • (x + y))
Tactic: refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
-- 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
σ : 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 * sy) • (x + y))
have 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))
Tactic: rw [smul_add, mul_smul, mul_smul, Algebra.smul_def sx (sy • y), smul_comm,
      Algebra.smul_def sy (sx • x)]
-- 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
σ : 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 τ)
    (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))
have apply : Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
  ((algebraMap S T : (a : S) → T) sy : T)
Tactic: apply add_mem (mul_mem _ hsx'') (mul_mem _ hsy'')
-- 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
σ : 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)
⊢ 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))
have apply₁ : Membership.mem (α := T) (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
  ((algebraMap S T : (a : S) → T) sx : T)
Tactic: apply add_mem (mul_mem _ hsx'') (mul_mem _ hsy'')
-- 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
σ : 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))
have refine_4 : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ)
  ((sx * sy) • (x * y))
Tactic: refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
-- 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
σ : 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 * sy) • (x * y))
have refine_4 : Membership.mem (γ := Subalgebra R T) (Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) (sx • x * sy • y)
Tactic: rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]
-- 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
h₂ : EssFiniteType S T
⊢ EssFiniteType R T
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))
  (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)
Tactic: rw [essFiniteType_iff] at h₁ h₂ ⊢
Cleared hypotheses: h₁, 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)
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)
have 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)
Tactic: obtain ⟨s, hs⟩ := 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 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)
⊢ ∃ (σ : 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)
have 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)
Tactic: obtain ⟨t, ht⟩ := 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
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)
⊢ ∃ (σ : 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)
have 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)
Tactic: use s.image (IsScalarTower.toAlgHom R S T) ∪ t