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
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)
⊢ ∀ (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)
have 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)
Tactic: simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
-- 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)
x : 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)) (x * t_1)
have 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)
Tactic: obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht 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
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_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)
have 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)
Tactic: obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
-- 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)
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_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)
have 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)
Tactic: obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
-- 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)
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)
have h : Membership.mem (γ := Subalgebra R T)
  (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • t₁ • y)
Tactic: refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
-- 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)
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))
h :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (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)
have h₇ : IsUnit (t₂ • t₁ • y)
Tactic: refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
-- 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)
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))
h :
  Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • t₁ • y)
h₇ : IsUnit (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)
have h₈ : Membership.mem (γ := Subalgebra R T)
  (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t₂ • t₁ • y)
Tactic: refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
-- 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)
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))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (t₂ • t₁ • y)
have h : Membership.mem (γ := Subalgebra R T)
  (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
  (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T) (t₁ • y))
Tactic: rw [Algebra.smul_def]
-- 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)
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))
⊢ IsUnit (t₂ • t₁ • y)
have h : IsUnit
  (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₂ : T)
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) y))
Tactic: rw [Algebra.smul_def, Algebra.smul_def]
-- 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)
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))
⊢ Membership.mem (γ := Subalgebra R T)
    (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T)) (x * t₂ • t₁ • y)
have h : Membership.mem (γ := Subalgebra R T)
  (Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R (↑s : Set S)) ⊔ adjoin R (↑t : Set T))
  (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) t₁ : T) (t₂ • (x * y)))
Tactic: rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
-- 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: classical
  obtain ⟨s, hs⟩ := h₁
  obtain ⟨t, ht⟩ := h₂
  use s.image (IsScalarTower.toAlgHom R S T) ∪ t
  simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
  obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
  obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
  refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
  · rw [Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
  · rw [Algebra.smul_def, Algebra.smul_def]
    exact (h₅.map _).mul ((h₂.map _).mul hy₂)
  · rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) 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 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)
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))
  (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: classical
  obtain ⟨s, hs⟩ := h₁
  obtain ⟨t, ht⟩ := h₂
  use s.image (IsScalarTower.toAlgHom R S T) ∪ t
  simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
  obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
  obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
  refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
  · rw [Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
  · rw [Algebra.smul_def, Algebra.smul_def]
    exact (h₅.map _).mul ((h₂.map _).mul hy₂)
  · rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆
Cleared hypotheses: h₁, h₂
-- 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
⊢ EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType.{u_1, u_2} R ↥S₀ ∧ IsLocalization M S
have refine : (∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType.{u_1, u_2} R ↥S₀ ∧ IsLocalization M S) → EssFiniteType R S
Tactic: refine ⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩