awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : 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)
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)
⊢ 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))

Tactic:
rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]

Premises used: add_mul, mul_assoc, mul_comm
-- 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
σ : 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 * tx * ty + y * ty * tx)

Tactic:
add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)

Premises used: AddMemClass.add_mem, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : 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 * tx * ty + y * ty * tx)

Tactic:
exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)

Premises used: AddMemClass.add_mem, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h : EssFiniteType R T
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)
⊢ EssFiniteType S T

Tactic:
rw [essFiniteType_iff] at h ⊢

Premises used: Algebra.essFiniteType_iff
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h :
  ∃ (σ : Finset 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)

Tactic:
obtain ⟨σ, hσ⟩ := h
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : 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)
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)
⊢ ∃ (σ : 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:
use σ
-- 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
σ : 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
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)
⊢ ∃ (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
-- 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
σ : 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)
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)
⊢ ∃ (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:
simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]

Premises used: Algebra.adjoin_adjoin_of_tower, SetLike.coe
-- 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
σ : 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 (↑(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:
⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩

Premises used: Algebra.subset_adjoin, 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
σ : 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 (↑(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:
exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h :
  ∃ (σ : Finset T),
    ∀ (s : T),
      ∃ (t : T),
        Membership.mem (γ := Subalgebra 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)
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)
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 (↑(adjoin R (↑σ : Set T)) : Set T)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra S T) (adjoin S (↑(adjoin R (↑σ : Set T)) : 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)

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₃⟩
-- 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
inst_7 : EssFiniteType R S
⊢ EssFiniteType R T ↔ EssFiniteType S T

Tactic:
⟨fun _ ↦ of_comp R S T, fun _ ↦ comp R S T⟩

Premises used: Algebra.EssFiniteType.of_comp, Algebra.EssFiniteType.comp, Iff.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
inst_7 : EssFiniteType R S
I : Ideal S
⊢ EssFiniteType.{u_1, u_2} R (S ⧸ I)

Tactic:
.comp R S _

Premises used: Algebra.EssFiniteType.comp
-- 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
inst_7 : EssFiniteType R S
M : Submonoid S
⊢ EssFiniteType.{u_1, u_2} R (Localization (M := S) M)

Tactic:
have : EssFiniteType S (Localization M) := .of_isLocalization _ M
  .comp R S _

Premises used: Algebra.EssFiniteType.comp, Localization, Algebra.EssFiniteType.of_isLocalization
-- 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
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this : Algebra S T := f.toAlgebra
⊢ IsScalarTower R S T

Tactic:
have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
-- 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
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
⊢ Module.Finite S T

Tactic:
have : Module.Finite S T := .of_surjective (Algebra.linearMap S T) hf
-- 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
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this_1 : Algebra S T := f.toAlgebra
this_2 : IsScalarTower R S T
this : Module.Finite S T
⊢ EssFiniteType R T

Tactic:
.comp R S T

Premises used: Algebra.EssFiniteType.comp
-- 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
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
inst_5 : EssFiniteType R S
this_1 : Algebra S T := f.toAlgebra
this_2 : IsScalarTower R S T
this : Module.Finite S T
⊢ EssFiniteType R T

Tactic:
exact .comp R S T
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this : f.toRingHom = g.toRingHom
H₁ : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((g : (a : S) → T) x : T)
⊢ f = g

Tactic:
ext
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this : f.toRingHom = g.toRingHom
x : S
⊢ Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((g : (a : S) → T) x : T)

Tactic:
RingHom.congr_fun this _

Premises used: RingHom.congr_fun
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this : f.toRingHom = g.toRingHom
x : S
⊢ Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((g : (a : S) → T) x : T)

Tactic:
exact RingHom.congr_fun this _

Premises used: RingHom.congr_fun
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
suffices : f.toRingHom = g.toRingHom
⊢ f = g

Tactic:
suffices f.toRingHom = g.toRingHom by ext; exact RingHom.congr_fun this _
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
h :
  Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
    (g.comp (algebraMap (↥(subalgebra R S)) S))
⊢ f.toRingHom = g.toRingHom

Tactic:
apply IsLocalization.ringHom_ext (EssFiniteType.submonoid R S)

Premises used: Algebra.EssFiniteType.submonoid, IsLocalization.ringHom_ext
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this :
  Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
a :
  ∀ (x : ↥(subalgebra R S)),
    Eq.{u_3 + 1} (α := T) ((f.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
      ((g.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
⊢ Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
    (g.comp (algebraMap (↥(subalgebra R S)) S))

Tactic:
ext
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this :
  Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
x : ↥(subalgebra R S)
⊢ Eq.{u_3 + 1} (α := T) ((f.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
    ((g.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)

Tactic:
AlgHom.congr_fun this _

Premises used: AlgHom.congr_fun
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
this :
  Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
x : ↥(subalgebra R S)
⊢ Eq.{u_3 + 1} (α := T) ((f.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)
    ((g.comp (algebraMap (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T) x : T)

Tactic:
exact AlgHom.congr_fun this _

Premises used: AlgHom.congr_fun
-- 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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
h :
  Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
⊢ Eq (α := RingHom.{u_2, u_3} (↥(subalgebra R S)) T) (f.comp (algebraMap (↥(subalgebra R S)) S))
    (g.comp (algebraMap (↥(subalgebra R S)) S))

Tactic:
suffices f.comp (IsScalarTower.toAlgHom R _ S) = g.comp (IsScalarTower.toAlgHom R _ S) by
    ext; exact AlgHom.congr_fun this _