awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
h :
  Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))
⊢ Eq (α := P.Fiber T)
    (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)) :
      P.Fiber T)
    (p ⊗ₜ[S] IsLocalization.mk' T s t : P.ResidueField ⊗[S] T)

Tactic:
apply ((IsLocalization.map_units T t).map
      Algebra.TensorProduct.includeRight).mul_left_injective

Premises used: IsUnit.mul_left_injective, IsLocalization.map_units, IsUnit.map, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
    (0 : P.ResidueField)
⊢ Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))

Tactic:
simp [ht]
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
⊢ Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((s • p) ⊗ₜ[S] 1)

Tactic:
simp [div_mul_cancel₀ _ ht]

Premises used: div_mul_cancel₀
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
dsimp :
  Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
    ((p * 1) ⊗ₜ[S] HMul.hMul (β := T) (IsLocalization.mk' T s t) ((algebraMap S T : (a : S) → T) (↑t : S) : T))
⊢ Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
⊢ Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
    ((p * 1) ⊗ₜ[S] HMul.hMul (β := T) (IsLocalization.mk' T s t) ((algebraMap S T : (a : S) → T) (↑t : S) : T))

Tactic:
simp [Algebra.algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
M : Submonoid S
inst_7 : QuasiFinite R S
⊢ QuasiFinite.{u_1, u_2} R (Localization (M := S) M)

Tactic:
of_isLocalization M

Premises used: Algebra.QuasiFinite.of_isLocalization
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : IsFractionRing R S
⊢ QuasiFinite R S

Tactic:
of_isLocalization (nonZeroDivisors R)

Premises used: nonZeroDivisors, Algebra.QuasiFinite.of_isLocalization
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
p : Ideal R
inst_8 : p.IsPrime
q : Ideal (p.Fiber S)
inst_9 : q.IsPrime
⊢ Module.Finite p.ResidueField (Localization.AtPrime (R := p.Fiber S) q)

Tactic:
.of_quasiFinite

Premises used: Module.Finite.of_quasiFinite
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
P : Ideal S
inst_7 : P.IsPrime
inst_8 : QuasiFinite R S
⊢ QuasiFinite.{u_1, u_2} R P.ResidueField

Tactic:
.trans _ (S ⧸ P) _

Premises used: Algebra.QuasiFinite.trans, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
⊢ QuasiFinite S T

Tactic:
⟨fun P hP ↦ ?_⟩

Premises used: Algebra.QuasiFinite.mk
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
refine : ∀ (P : Ideal S) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber T)
⊢ QuasiFinite S T

Tactic:
refine ⟨fun P hP ↦ ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
rw :
  {t : P.ResidueField ⊗[S] T | ∃ (m : P.ResidueField) (n : T), m ⊗ₜ[S] n = t} ⊆
    (↑(LinearMap.range (AlgHom.toLinearMap (AlgHom.restrictScalars S f))) : Set (P.ResidueField ⊗[S] T))
⊢ Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)

Tactic:
rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]

Premises used: AlgHom.coe_toLinearMap, TensorProduct.span_tmul_eq_top, LinearMap.range_eq_top, AlgHom.coe_restrictScalars', top_le_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
a : P.ResidueField
b : T
⊢ Eq (α := P.Fiber T)
    ((AlgHom.toLinearMap (AlgHom.restrictScalars S f) : (a : P.ResidueField ⊗[R] T) → P.Fiber T) (a ⊗ₜ[R] b) :
      P.Fiber T)
    (a ⊗ₜ[S] b : P.ResidueField ⊗[S] T)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
a : P.ResidueField
b : T
⊢ a ⊗ₜ[S] b ∈ (↑(LinearMap.range (AlgHom.toLinearMap (AlgHom.restrictScalars S f))) : Set (P.ResidueField ⊗[S] T))

Tactic:
exact ⟨a ⊗ₜ b, by simp [f]⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)

Tactic:
have hf : Function.Surjective f := by
    rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]
    rintro _ ⟨a, b, rfl⟩
    exact ⟨a ⊗ₜ b, by simp [f]⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
hf :
  Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
⊢ Module.Finite P.ResidueField (TensorProduct.{u_1, u_2, u_3} R P.ResidueField T)

Tactic:
have : Module.Finite P.ResidueField (P.ResidueField ⊗[R] T) := .of_quasiFinite
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
hf :
  Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
this : Module.Finite P.ResidueField (TensorProduct.{u_1, u_2, u_3} R P.ResidueField T)
⊢ Module.Finite P.ResidueField (P.Fiber T)

Tactic:
.of_surjective f.toLinearMap hf

Premises used: AlgHom.toLinearMap, Module.Finite.of_surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
hf :
  Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
this : Module.Finite P.ResidueField (TensorProduct.{u_1, u_2, u_3} R P.ResidueField T)
⊢ Module.Finite P.ResidueField (P.Fiber T)

Tactic:
exact .of_surjective f.toLinearMap hf
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : DiscreteTopology.{u_1} (PrimeSpectrum R)
inst_4 : QuasiFinite R S
⊢ DiscreteTopology.{u_2} (PrimeSpectrum S)

Tactic:
isDiscrete_univ_iff.mp
    (isDiscrete_comap_preimage (R := R) (S := S) (isDiscrete_univ_iff.mpr ‹_›))

Premises used: Iff.mpr, isDiscrete_univ_iff, Iff.mp, Algebra.QuasiFinite.isDiscrete_comap_preimage
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite.{u_1 + 1} (PrimeSpectrum R)
inst_4 : QuasiFinite R S
⊢ Finite.{u_2 + 1} (PrimeSpectrum S)

Tactic:
Set.finite_univ_iff.mp
    (finite_comap_preimage (Set.finite_univ (α := PrimeSpectrum R)))

Premises used: Algebra.QuasiFinite.finite_comap_preimage, Set.finite_univ, Iff.mp, Set.finite_univ_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
⊢ ∀ (y : ↥(Submonoid.comap f (IsUnit.submonoid T))), IsUnit.{u_3} (M := T) ((f : (a : S) → T) (↑y : S) : T)

Tactic:
simp [IsUnit.mem_submonoid_iff]

Premises used: IsUnit.mem_submonoid_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
suffices :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization (Submonoid.comap f (IsUnit.submonoid T))) (β := T)
    (⇑φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T)
⊢ QuasiFinite R T

Tactic:
suffices Function.Surjective φ from .of_surjective_algHom φ this
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
obtain :
  ∀ (s : S) (hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)) (t : S)
    (ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)),
    ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
      (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x
⊢ ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x

Tactic:
obtain ⟨s, hs, t, ht⟩ := H x
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
s : S
hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)
t : S
ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)
⊢ ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x

Tactic:
⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap f) _ t ⟨s, hs⟩, ?_⟩

Premises used: Subtype.mk, IsLocalization.mk', Exists.intro
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
s : S
hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)
t : S
ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)
refine :
  (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T)
      (IsLocalization.mk' (M := Submonoid.comap f (IsUnit.submonoid T))
        (Localization (Submonoid.comap f (IsUnit.submonoid T))) t
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.comap f (IsUnit.submonoid T)) x) s
          hs)) =
    x
⊢ ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x

Tactic:
refine ⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap f) _ t ⟨s, hs⟩, ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
s : S
hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)
t : S
ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)
⊢ (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T)
      (IsLocalization.mk' (M := Submonoid.comap f (IsUnit.submonoid T))
        (Localization (Submonoid.comap f (IsUnit.submonoid T))) t
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.comap f (IsUnit.submonoid T)) x) s
          hs)) =
    x

Tactic:
simpa [φ, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.coe_liftRight]

Premises used: Units.mul_inv_eq_iff_eq_mul, IsLocalization.lift_mk', IsUnit.coe_liftRight
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : QuasiFinite R S
P Q : Ideal S
inst_4 : P.IsPrime
inst_5 : Q.IsPrime
h₁ : P ≤ Q
h₂ : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R Q)
⊢ { asIdeal := P, isPrime := inst_4 : PrimeSpectrum S } ⤳ { asIdeal := Q, isPrime := inst_5 }

Tactic:
simpa [← PrimeSpectrum.le_iff_specializes]

Premises used: PrimeSpectrum.le_iff_specializes