awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
p_1 : Ideal R
q : Ideal S
inst_5 : q.IsPrime
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : T ≃ₐ[R] S
x : S
⊢ x ∈ p ↔ Membership.mem (γ := Ideal S) (Ideal.comap (↑f.symm : S →ₐ[R] T) (Ideal.comap f.toRingEquiv.toRingHom p)) x

Tactic:
simp
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
inst_6 : WeaklyQuasiFiniteAt R q
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
⊢ q =
    q ⊔
      Ideal.comap (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) ⊥

Tactic:
simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

Premises used: RingHom.ker_eq_comap_bot, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
inst_6 : WeaklyQuasiFiniteAt R q
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
⊢ r.LiesOver q

Tactic:
have : r.LiesOver q :=
    ⟨.trans (by simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le])
    (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
inst_6 : WeaklyQuasiFiniteAt R q
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
this_1 : r.LiesOver q
this : Algebra (Localization.AtPrime q) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver q r
⊢ r.LiesOver p

Tactic:
have : r.LiesOver p := .trans _ q _
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
inst_6 : WeaklyQuasiFiniteAt R q
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
this_1 : r.LiesOver q
this_2 : Algebra (Localization.AtPrime q) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver q r
this_3 : r.LiesOver p
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver p r
⊢ Module.Finite.{u_1, u_2} p.ResidueField q.ResidueField

Tactic:
.of_injective (IsScalarTower.toAlgHom _ _ r.ResidueField).toLinearMap (RingHom.injective _)

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, Ideal.ResidueField, Module.Finite.of_injective, RingHom.injective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
inst_6 : WeaklyQuasiFiniteAt R q
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) :=
  Ideal.map (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R q))) q
this_1 : r.LiesOver q
this_2 : Algebra (Localization.AtPrime q) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver q r
this_3 : r.LiesOver p
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver p r
⊢ Module.Finite.{u_1, u_2} p.ResidueField q.ResidueField

Tactic:
exact .of_injective (IsScalarTower.toAlgHom _ _ r.ResidueField).toLinearMap (RingHom.injective _)
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
S : Type u_2
inst : CommRing S
q : Ideal S
inst_1 : q.IsPrime
K : Type u_4
inst_2 : Field K
inst_3 : Algebra K S
inst_4 : WeaklyQuasiFiniteAt K q
⊢ WeaklyQuasiFiniteAt K q

Tactic:
have H : Algebra.WeaklyQuasiFiniteAt K q := ‹_›
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
S : Type u_2
inst : CommRing S
q : Ideal S
inst_1 : q.IsPrime
K : Type u_4
inst_2 : Field K
inst_3 : Algebra K S
inst_4 H : WeaklyQuasiFiniteAt K q
⊢ QuasiFinite.{u_4, u_2} K (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q)) ⊥)

Tactic:
rw [Algebra.weaklyQuasiFiniteAt_iff, ← Ideal.over_def q ⊥, Ideal.map_bot] at H

Premises used: Bot.bot, Ideal.map_bot, Algebra.weaklyQuasiFiniteAt_iff, Ideal.over_def
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
S : Type u_2
inst : CommRing S
q : Ideal S
inst_1 : q.IsPrime
K : Type u_4
inst_2 : Field K
inst_3 : Algebra K S
inst_4 : WeaklyQuasiFiniteAt K q
H : QuasiFinite.{u_4, u_2} K (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q)) ⊥)
⊢ QuasiFinite.{u_4, u_2} K (Localization.AtPrime q)

Tactic:
have : QuasiFinite K (Localization.AtPrime q) := .of_surjective_algHom
    (AlgEquiv.quotientBot K _).toAlgHom (AlgEquiv.quotientBot K _).surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
S : Type u_2
inst : CommRing S
q : Ideal S
inst_1 : q.IsPrime
K : Type u_4
inst_2 : Field K
inst_3 : Algebra K S
inst_4 : WeaklyQuasiFiniteAt K q
H : QuasiFinite.{u_4, u_2} K (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q)) ⊥)
this : QuasiFinite.{u_4, u_2} K (Localization.AtPrime q)
⊢ Module.Finite.{u_4, u_2} K (Localization.AtPrime q)

Tactic:
.of_quasiFinite

Premises used: Module.Finite.of_quasiFinite
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
S : Type u_2
inst : CommRing S
q : Ideal S
inst_1 : q.IsPrime
K : Type u_4
inst_2 : Field K
inst_3 : Algebra K S
inst_4 : WeaklyQuasiFiniteAt K q
H : QuasiFinite.{u_4, u_2} K (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q)) ⊥)
this : QuasiFinite.{u_4, u_2} K (Localization.AtPrime q)
⊢ Module.Finite.{u_4, u_2} K (Localization.AtPrime q)

Tactic:
exact .of_quasiFinite
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
⊢ RingHom.ker (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) ≤
    P

Tactic:
simpa [← h₂] using Ideal.map_comap_le

Premises used: Ideal.map_comap_le
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
⊢ Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)

Tactic:
have : (P.map (Ideal.Quotient.mk ((Q.under R).map (algebraMap R S)))).IsPrime :=
    Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective
    (by simpa [← h₂] using Ideal.map_comap_le)
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
this :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
rw :
  Eq (α := Ideal R)
    (Ideal.under R
      (Ideal.under S (B :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.map (F :=
          S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)))
    (Ideal.under R
      (Ideal.under S (B :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.map (F :=
          S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)))
⊢ Eq (α := Ideal R)
    (Ideal.under R (B :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.map (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P))
    (Ideal.under R (B :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.map (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q))

Tactic:
rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]

Premises used: Ideal.under_under
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
this :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
dsimp :
  Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.comap (F :=
        S →+*
          HasQuotient.Quotient S (B := Ideal S)
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.map (F :=
          S →+*
            HasQuotient.Quotient S (B := Ideal S)
              (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          (Ideal.Quotient.mk
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          P)))
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.comap (F :=
        S →+*
          HasQuotient.Quotient S (B := Ideal S)
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.map (F :=
          S →+*
            HasQuotient.Quotient S (B := Ideal S)
              (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          (Ideal.Quotient.mk
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          Q)))
⊢ Eq (α := Ideal R)
    (Ideal.under R
      (Ideal.under S (B :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.map (F :=
          S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)))
    (Ideal.under R
      (Ideal.under S (B :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.map (F :=
          S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)))

Tactic:
dsimp [Ideal.under] at h₂ ⊢

Premises used: Ideal.under
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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.comap (F := R →+* S) (algebraMap R S) P) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)
inst_5 : WeaklyQuasiFiniteAt R Q
this :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
simp :
  Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q) ⊔ P))
    (Ideal.comap (F := R →+* S) (algebraMap R S) Q)
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.comap (F :=
        S →+*
          HasQuotient.Quotient S (B := Ideal S)
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.map (F :=
          S →+*
            HasQuotient.Quotient S (B := Ideal S)
              (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          (Ideal.Quotient.mk
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          P)))
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.comap (F :=
        S →+*
          HasQuotient.Quotient S (B := Ideal S)
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
        (Ideal.map (F :=
          S →+*
            HasQuotient.Quotient S (B := Ideal S)
              (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          (Ideal.Quotient.mk
            (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)))
          Q)))

Tactic:
simp [Ideal.map_comap_le]

Premises used: Ideal.map_comap_le
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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.comap (F := R →+* S) (algebraMap R S) P) (Ideal.comap (F := R →+* S) (algebraMap R S) Q)
inst_5 : WeaklyQuasiFiniteAt R Q
this :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S) (algebraMap R S)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) Q) ⊔ P))
    (Ideal.comap (F := R →+* S) (algebraMap R S) Q)

Tactic:
simp [Ideal.map_comap_le, ← h₂]

Premises used: Ideal.map_comap_le
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
this :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
⊢ Eq (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
have := QuasiFiniteAt.eq_of_le_of_under_eq (R := R)
    (P := P.map (Ideal.Quotient.mk ((Q.under R).map (algebraMap R S))))
    (Q := Q.map (Ideal.Quotient.mk ((Q.under R).map (algebraMap R S))))
    (Ideal.map_mono h₁) (by
      rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]
      dsimp [Ideal.under] at h₂ ⊢
      simp [Ideal.map_comap_le]
      simp [Ideal.map_comap_le, ← h₂])
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
this_1 :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
this :
  Eq (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)
⊢ P ⊔
      Ideal.comap (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) ⊥ =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.map (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
replace this := (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm.trans
    congr($(this).comap _)
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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 : WeaklyQuasiFiniteAt R Q
this_1 :
  Ideal.IsPrime (α :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
this_2 :
  Eq (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) P)
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)
this :
  P ⊔
      Ideal.comap (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) ⊥ =
    Ideal.comap (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
      (Ideal.map (F :=
        S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q))) Q)
⊢ P ⊔ Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R Q) = Q

Tactic:
simp [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.map_comap_le] at this

Premises used: Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.map_comap_le