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
σ : 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 tx : T ⊗[R] S
hx₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) tx
hx₂ : IsUnit tx
hx₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (x * tx)
ty : T ⊗[R] S
hy₁ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) ty
hy₂ : IsUnit ty
hy₃ :
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (y * ty)
⊢ Membership.mem (γ := Subalgebra T (T ⊗[R] S))
    (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
    ((x + y) * (tx * ty))
have h : Membership.mem (γ := Subalgebra T (T ⊗[R] S))
  (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
  (x * tx * ty + y * ty * tx)
Tactic: rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
-- 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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
s : T ⊗[R] S
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (s * t)
have h : ∃ (t : T ⊗[R] S),
  Membership.mem (γ := Subalgebra T (T ⊗[R] S))
      (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
    IsUnit t ∧
      Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (0 * t)
Tactic: induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)
Cleared hypotheses: 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
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
s : T ⊗[R] S
h :
  ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (0 * t)
⊢ ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) (s * t)
have h₁ : ∀ (x : T) (y : S),
  ∃ (t : T ⊗[R] S),
    Membership.mem (γ := Subalgebra T (T ⊗[R] S))
        (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S))) t ∧
      IsUnit t ∧
        Membership.mem (γ := Subalgebra T (T ⊗[R] S))
          (adjoin T (↑(Finset.image (⇑TensorProduct.includeRight : (a : S) → T ⊗[R] S) σ) : Set (T ⊗[R] S)))
          (x ⊗ₜ[R] y * t)
Tactic: induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)
Cleared hypotheses: 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
h : EssFiniteType R S
⊢ EssFiniteType T (T ⊗[R] S)
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)),
  ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
Tactic: classical
  rw [essFiniteType_iff] at h ⊢
  obtain ⟨σ, hσ⟩ := h
  use σ.image Algebra.TensorProduct.includeRight
  intro s
  induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)
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 : EssFiniteType R S
rw rw₁ rw₂ :
  ∀
    (h :
      ∃ (σ : Finset S),
        ∀ (s : S),
          ∃ (t : S),
            Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
              IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)),
    ∃ (σ : Finset (T ⊗[R] S)),
      ∀ (s : T ⊗[R] S),
        ∃ (t : T ⊗[R] S),
          Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
⊢ EssFiniteType T (T ⊗[R] S)
have rw₃ : ∀ (σ : Finset S)
  (hσ :
    ∀ (s : S),
      ∃ (t : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)),
  ∃ (σ : Finset (T ⊗[R] S)),
    ∀ (s : T ⊗[R] S),
      ∃ (t : T ⊗[R] S),
        Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra T (T ⊗[R] S)) (adjoin T (↑σ : Set (T ⊗[R] S))) (s * t)
Tactic: classical
  rw [essFiniteType_iff] at h ⊢
  obtain ⟨σ, hσ⟩ := h
  use σ.image Algebra.TensorProduct.includeRight
  intro s
  induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)
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 : EssFiniteType R T
⊢ EssFiniteType S T
have rw : ∀
  (h :
    ∃ (σ : 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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
Tactic: rw [essFiniteType_iff] at 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 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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
have obtain : ∀ (σ : Finset T)
  (hσ :
    ∀ (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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
Tactic: obtain ⟨σ, hσ⟩ := 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
σ : Finset T
hσ :
  ∀ (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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
have h : ∀ (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)
Tactic: use σ
-- 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
σ : Finset T
hσ :
  ∀ (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)
x : T
⊢ ∃ (t : T),
    Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
have h : ∀ (y : T) (hy₁ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) y) (hy₂ : IsUnit y)
  (hy₃ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (x * y)),
  ∃ (t : T),
    Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
Tactic: obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ 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
σ : Finset T
hσ :
  ∀ (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)
x y : T
hy₁ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) y
hy₂ : IsUnit y
hy₃ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (x * y)
⊢ ∃ (t : T),
    Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
have h : ∃ (t : T),
  Membership.mem (γ := Subalgebra S T) (adjoin S (↑(adjoin R (↑σ : Set T)) : Set T)) t ∧
    IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑(adjoin R (↑σ : Set T)) : Set T)) (x * t)
Tactic: simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
-- 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 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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
have obtain : ∀ (σ : Finset T)
  (hσ :
    ∀ (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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
Tactic: classical
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩
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 R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
obtain :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (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 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 S T) (adjoin S (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
have h₁ : ∀ (σ : Finset T)
  (hσ :
    ∀ (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))
  (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)
Tactic: classical
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩
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 R T) (adjoin R (↑σ : Set T)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (s * t)
obtain :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (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 S T) (adjoin S (↑σ : Set T)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (s * t)
h₁ h₂ :
  ∀ (σ : Finset T)
    (hσ :
      ∀ (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))
    (x : T),
    ∃ (t : T),
      Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
⊢ ∃ (σ : 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)
have h₃ : ∀ (σ : Finset T)
  (hσ :
    ∀ (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))
  (x y : T) (hy₁ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) y) (hy₂ : IsUnit y)
  (hy₃ : Membership.mem (γ := Subalgebra R T) (adjoin R (↑σ : Set T)) (x * y)),
  ∃ (t : T),
    Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑σ : Set T)) (x * t)
Tactic: classical
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩
Cleared hypotheses: h