awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : QuasiFiniteAt R p
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
      (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
          (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) s) :
        Localization.AtPrime (R := A ⊗[R] S) q) ∈
    f.range
have rw : Membership.mem (α := Localization.AtPrime (R := A ⊗[R] S) q) f.range
  ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
    Localization.AtPrime (R := A ⊗[R] S) q)
Tactic: rw [this, IsLocalization.mk'_spec_mk]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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
p : Ideal S
inst_5 : p.IsPrime
inst_6 : QuasiFiniteAt R p
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
q : Ideal T
inst_7 : q.IsPrime
hq : p = Ideal.comap f.toRingHom q
⊢ QuasiFiniteAt R q
have inst : Ideal.IsPrime (Ideal.comap f.toRingHom q)
Tactic: subst hq
Cleared hypotheses: p, inst_5, inst_6, hq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
p : Ideal S
inst_6 : p.IsPrime
inst_7 : QuasiFiniteAt R p
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
q : Ideal T
inst_8 : q.IsPrime
hq : p = Ideal.comap f.toRingHom q
inst : Ideal.IsPrime (Ideal.comap f.toRingHom q)
⊢ QuasiFiniteAt R q
have inst₁ : QuasiFiniteAt R (Ideal.comap f.toRingHom q)
Tactic: subst hq
Cleared hypotheses: p, inst_6, inst_7, hq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (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
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
q : Ideal T
inst_5 : q.IsPrime
inst_6 : Ideal.IsPrime (Ideal.comap f.toRingHom q)
inst_7 : QuasiFiniteAt R (Ideal.comap f.toRingHom q)
⊢ QuasiFiniteAt R q
have refine : ∀ (r : R),
  Eq (α := Localization.AtPrime q)
    (OneHom.toFun (M := Localization.AtPrime (Ideal.comap f.toRingHom q))
      (↑(↑(Localization.localRingHom (Ideal.comap f.toRingHom q) q f.toRingHom sorry) :
            Localization.AtPrime (Ideal.comap f.toRingHom q) →* Localization.AtPrime q) :
        OneHom (Localization.AtPrime (Ideal.comap f.toRingHom q)) (Localization.AtPrime q))
      ((algebraMap R (Localization.AtPrime (Ideal.comap f.toRingHom q)) :
          (a : R) → Localization.AtPrime (Ideal.comap f.toRingHom q))
        r))
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r)
Tactic: refine .of_surjective_algHom ⟨Localization.localRingHom _ q f.toRingHom rfl, ?_⟩ (hf q ‹_›)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (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
p : Ideal S
inst_7 : p.IsPrime
inst_8 : QuasiFiniteAt R p
f : T ≃ₐ[R] S
⊢ p = Ideal.comap (↑f.symm : S →ₐ[R] T).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p)
have h : ∀ (x : S),
  x ∈ p ↔
    Membership.mem (γ := Ideal S) (Ideal.comap (↑f.symm : S →ₐ[R] T).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
⊢ ∀ (y : ↥Q.primeCompl),
    IsUnit (M := Localization.AtPrime P)
      ((IsScalarTower.toAlgHom R S (Localization.AtPrime P) : (a : S) → Localization.AtPrime P) (↑y : S) :
        Localization.AtPrime P)
have simp : ∀ (a : S) (b : a ∉ Q),
  IsUnit (M := Localization.AtPrime P)
    ((algebraMap S (Localization.AtPrime P) : (a : S) → Localization.AtPrime P) a : Localization.AtPrime P)
Tactic: simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P :=
  IsLocalization.liftAlgHom (R := S) (M := Q.primeCompl) (f := IsScalarTower.toAlgHom R S (Localization.AtPrime P)) ⋯
⊢ QuasiFiniteAt R P
have refine : ∀ (x : Localization.AtPrime P),
  ∃ (s : Localization.AtPrime Q),
    IsUnit (M := Localization.AtPrime P)
        ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s : Localization.AtPrime P) ∧
      HMul.hMul (β := Localization.AtPrime P) x
          ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s : Localization.AtPrime P) ∈
        f.range
Tactic: refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P :=
  IsLocalization.liftAlgHom (R := S) (M := Q.primeCompl) (f := IsScalarTower.toAlgHom R S (Localization.AtPrime P)) ⋯
x : Localization.AtPrime P
⊢ ∃ (s : Localization.AtPrime Q),
    IsUnit (M := Localization.AtPrime P)
        ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s : Localization.AtPrime P) ∧
      HMul.hMul (β := Localization.AtPrime P) x
          ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s : Localization.AtPrime P) ∈
        f.range
have obtain : ∀ (x s : S) (hs : s ∈ P.primeCompl),
  ∃ (s_1 : Localization.AtPrime Q),
    IsUnit (M := Localization.AtPrime P)
        ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s_1 : Localization.AtPrime P) ∧
      HMul.hMul (α := Localization.AtPrime P) (β := Localization.AtPrime P)
          (IsLocalization.mk' (Localization.AtPrime P) x (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) s hs) :
            Localization.AtPrime P)
          ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P) s_1 : Localization.AtPrime P) ∈
        f.range
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
h₂ : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R Q)
inst_5 : QuasiFiniteAt R Q
⊢ P = Q
have this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
Tactic: have : Disjoint (Q.primeCompl : Set S) P := by simpa [Set.disjoint_iff, Set.ext_iff, not_imp_comm]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
h₂ : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R Q)
inst_5 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
⊢ P = Q
have inst : Ideal.IsPrime (α := Localization.AtPrime Q)
  (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
Tactic: have inst := IsLocalization.isPrime_of_isPrime_disjoint _ (Localization.AtPrime Q) P ‹_› this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ Eq (α := Ideal R)
    (Ideal.under R (B := Localization.AtPrime Q)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P))
    (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
have h : Eq (α := Ideal R)
  (Ideal.under R (B := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P))
  (Ideal.under R P)
Tactic: convert! h₂
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
h :
  Eq (α := Ideal R)
    (Ideal.under R (B := Localization.AtPrime Q)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P))
    (Ideal.under R P)
⊢ Eq (α := Ideal R)
    (Ideal.under R (B := Localization.AtPrime Q)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P))
    (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
have h₃ : Eq (α := Ideal R)
  (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
  (Ideal.under R Q)
Tactic: convert! h₂
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ Eq (α := Ideal R)
    (Ideal.under R (B := Localization.AtPrime Q)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P))
    (Ideal.under R P)
have h : Eq (α := Ideal R)
  (Ideal.under R
    (Ideal.under S (B := Localization.AtPrime Q)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)))
  (Ideal.under R P)
Tactic: rw [← Ideal.under_under (B := S)]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ Eq (α := Ideal R)
    (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
have h : Eq (α := Ideal R)
  (Ideal.under R (Ideal.under S (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q))))
  (Ideal.under R Q)
Tactic: rw [← Ideal.under_under (B := S)]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ Eq (α := Ideal R)
    (Ideal.under R
      (Ideal.under S (B := Localization.AtPrime Q)
        (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)))
    (Ideal.under R P)
have h : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R P)
Tactic: rw [IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ Eq (α := Ideal R)
    (Ideal.under R (Ideal.under S (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q))))
    (Ideal.under R Q)
have h : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q)
Tactic: rw [Localization.AtPrime.under_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ P = Q
have H : Eq (α := Ideal (Localization.AtPrime Q))
  (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
  (IsLocalRing.maximalIdeal (Localization.AtPrime Q))
Tactic: have H := QuasiFinite.eq_of_le_of_under_eq (R := R)
    (Ideal.map (algebraMap S (Localization.AtPrime Q)) P) _
    (IsLocalRing.le_maximalIdeal_of_isPrime _) (by
      convert! h₂ <;> rw [← Ideal.under_under (B := S)]
      · rw [IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]
      · rw [Localization.AtPrime.under_maximalIdeal])
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
H :
  Eq (α := Ideal (Localization.AtPrime Q))
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
    (IsLocalRing.maximalIdeal (Localization.AtPrime Q))
⊢ P = Q
have rw : P =
  Ideal.under S (B := Localization (M := S) Q.primeCompl)
    (IsLocalRing.maximalIdeal (Localization (M := S) Q.primeCompl))
Tactic: rw [← Localization.AtPrime.under_maximalIdeal (I := Q), ← H,
    IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
H :
  Eq (α := Ideal (Localization.AtPrime Q))
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
    (IsLocalRing.maximalIdeal (Localization.AtPrime Q))
rw :
  P =
    Ideal.under S (B := Localization (M := S) Q.primeCompl)
      (IsLocalRing.maximalIdeal (Localization (M := S) Q.primeCompl))
⊢ P = Q
have rw₁ : P =
  Ideal.under S (B := Localization (M := S) Q.primeCompl)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
Tactic: rw [← Localization.AtPrime.under_maximalIdeal (I := Q), ← H,
    IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra 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)
inst_6 : QuasiFiniteAt R Q
this : Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)
inst :
  Ideal.IsPrime (α := Localization.AtPrime Q)
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
H :
  Eq (α := Ideal (Localization.AtPrime Q))
    (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
    (IsLocalRing.maximalIdeal (Localization.AtPrime Q))
rw :
  P =
    Ideal.under S (B := Localization (M := S) Q.primeCompl)
      (IsLocalRing.maximalIdeal (Localization (M := S) Q.primeCompl))
rw₁ :
  P =
    Ideal.under S (B := Localization (M := S) Q.primeCompl)
      (Ideal.map (F := S →+* Localization.AtPrime Q) (algebraMap S (Localization.AtPrime Q)) P)
⊢ P = Q
have rw₂ : P = P
Tactic: rw [← Localization.AtPrime.under_maximalIdeal (I := Q), ← H,
    IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
Tactic: have : IsLocalizedModule p.primeCompl (.id (R := S) (M := Localization.AtPrime p)) :=
    ⟨IsLocalizedModule.map_units (Algebra.linearMap S (Localization.AtPrime p)),
      fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, p.primeCompl.one_mem⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
Tactic: have : Module.Finite R (Localization.AtPrime p) := .of_quasiFinite
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : Module.Finite S (Localization.AtPrime p)
Tactic: have : Module.Finite S (Localization.AtPrime p) := .of_restrictScalars_finite R _ _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this : Module.Finite S (Localization.AtPrime p)
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : IsArtinianRing.{u_2} (Localization.AtPrime p)
Tactic: have : IsArtinianRing (Localization.AtPrime p) := .of_finite R _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this : IsArtinianRing.{u_2} (Localization.AtPrime p)
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : IsNoetherianRing S
Tactic: have : IsNoetherianRing S := Algebra.EssFiniteType.isNoetherianRing R S
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
inst_5 : EssFiniteType R S
inst_6 : QuasiFiniteAt R p
this_1 : IsLocalizedModule (M := Localization.AtPrime p) p.primeCompl LinearMap.id
this_2 : Module.Finite.{u_1, u_2} R (Localization.AtPrime p)
this_3 : Module.Finite S (Localization.AtPrime p)
this_4 : IsArtinianRing.{u_2} (Localization.AtPrime p)
this : IsNoetherianRing S
⊢ ∃ f ∉ p,
    (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) = {{ asIdeal := p, isPrime := inst_3 : PrimeSpectrum S }}
have this₁ : Module.FinitePresentation S (Localization.AtPrime p)
Tactic: have : Module.FinitePresentation S (Localization.AtPrime p) :=
    Module.finitePresentation_of_finite _ _