awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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:
exact ⟨g x, this 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
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
⊢ Ideal.IsPrime (Ideal.comap f.toRingHom q)

Tactic:
subst hq
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 (Ideal.comap f.toRingHom q)

Tactic:
subst hq
-- 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
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

Tactic:
.of_surjective_algHom ⟨Localization.localRingHom _ q f.toRingHom rfl, ?_⟩ (hf q ‹_›)

Premises used: Algebra.QuasiFinite.of_surjective_algHom, Localization.localRingHom, AlgHom.toRingHom, AlgHom.mk, rfl
-- 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
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)
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 ⋯) :
              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)
⊢ QuasiFiniteAt R q

Tactic:
refine .of_surjective_algHom ⟨Localization.localRingHom _ q f.toRingHom rfl, ?_⟩ (hf q ‹_›)
-- 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
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)
⊢ ∀ (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 ⋯) :
              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:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime (q.comap _)),
    IsScalarTower.algebraMap_apply R T (Localization.AtPrime _)]

Premises used: Localization.AtPrime, Ideal.comap, IsScalarTower.algebraMap_apply
-- 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 : QuasiFiniteAt R p
hf : RingHom.SurjectiveOnStalks (algebraMap S T)
q : Ideal T
inst_9 : q.IsPrime
inst_10 : q.LiesOver p
⊢ QuasiFiniteAt R q

Tactic:
.of_surjectiveOnStalks p (IsScalarTower.toAlgHom R S T) hf _ (q.over_def p)

Premises used: IsScalarTower.toAlgHom, Algebra.QuasiFiniteAt.of_surjectiveOnStalks, Ideal.over_def
-- 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 : QuasiFiniteAt R p
f : T ≃ₐ[R] S
h :
  ∀ (x : S),
    x ∈ p ↔
      Membership.mem (γ := Ideal S)
        (Ideal.comap (↑f.symm : S →ₐ[R] T).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p)) x
⊢ p = Ideal.comap (↑f.symm : S →ₐ[R] T).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
ext
-- 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 : QuasiFiniteAt R p
f : T ≃ₐ[R] S
x : S
⊢ x ∈ p ↔
    Membership.mem (γ := Ideal S) (Ideal.comap (↑f.symm : S →ₐ[R] T).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p))
      x

Tactic:
simp
-- 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
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
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)
⊢ ∀ (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)

Tactic:
simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]

Premises used: IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff
-- 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
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
⊢ ∀ (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:
fun a ha ↦ IsLocalization.map_units (M := P.primeCompl) _ ⟨a, fun h ↦ ha (h₁ h)⟩

Premises used: Localization.AtPrime, Subtype.mk, IsLocalization.map_units
-- 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
P Q : Ideal S
inst_3 : P.IsPrime
inst_4 : Q.IsPrime
h₁ : P ≤ Q
inst_5 : QuasiFiniteAt R Q
⊢ ∀ (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:
exact fun a ha ↦ IsLocalization.map_units (M := P.primeCompl) _ ⟨a, fun h ↦ ha (h₁ h)⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- 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
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

Tactic:
.of_forall_exists_mul_mem_range f fun x ↦ ?_

Premises used: Algebra.QuasiFinite.of_forall_exists_mul_mem_range
-- 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
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)) ⋯
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
⊢ QuasiFiniteAt R P

Tactic:
refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
-- 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
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
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
⊢ ∃ (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:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- 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
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 s : S
hs : s ∈ P.primeCompl
⊢ IsUnit (M := Localization.AtPrime P)
    ((f : (a : Localization.AtPrime Q) → Localization.AtPrime P)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) s) :
      Localization.AtPrime P)

Tactic:
simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- 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
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 s : S
hs : s ∈ P.primeCompl
⊢ (f.toRingHom : (a : Localization.AtPrime Q) → Localization.AtPrime P)
      ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) =
    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)
          ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) s) :
        Localization.AtPrime P)

Tactic:
simp [f]
-- 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
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 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:
exact ⟨algebraMap _ _ s, by simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp [f]⟩
-- 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
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
⊢ Disjoint (↑Q.primeCompl : Set S) (↑P : Set S)

Tactic:
simpa [Set.disjoint_iff, Set.ext_iff, not_imp_comm]

Premises used: not_imp_comm, Set.ext_iff, Set.disjoint_iff
-- 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
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
⊢ 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]
-- 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
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)
⊢ 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
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 P) (Ideal.under R Q)

Tactic:
h₂
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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)
h₃ :
  Eq (α := Ideal R)
    (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
⊢ 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)))

Tactic:
convert! h₂
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
      (Ideal.under S (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 R P)

Tactic:
rw [← Ideal.under_under (B := S)]

Premises used: Ideal.under_under
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 (Ideal.under S (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q))))
    (Ideal.under R Q)
⊢ Eq (α := Ideal R)
    (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)

Tactic:
rw [← Ideal.under_under (B := S)]

Premises used: Ideal.under_under
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 h₃ : Eq (α := Ideal R) (Ideal.under R P) (Ideal.under R 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)

Tactic:
rw [IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]

Premises used: Ideal.primeCompl, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 h₃ : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q)
⊢ Eq (α := Ideal R)
    (Ideal.under R (Ideal.under S (B := Localization.AtPrime Q) (IsLocalRing.maximalIdeal (Localization.AtPrime Q))))
    (Ideal.under R Q)

Tactic:
rw [Localization.AtPrime.under_maximalIdeal]

Premises used: Localization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 (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])
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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)
rw₂ rw₃ : P = P
⊢ P = Q

Tactic:
rw [← Localization.AtPrime.under_maximalIdeal (I := Q), ← H,
    IsLocalization.under_map_of_isPrime_disjoint Q.primeCompl _ ‹P.IsPrime› this]

Premises used: Localization.AtPrime.under_maximalIdeal, Ideal.primeCompl, IsLocalization.under_map_of_isPrime_disjoint