awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ WeaklyQuasiFiniteAt R q
have rw : QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p))) →
  ∀ (q : Ideal T) [inst_9 : q.IsPrime] (f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q))
    (hf :
      Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
        (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)),
    QuasiFinite.{u_1, u_3} R
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
Tactic: rw [weaklyQuasiFiniteAt_iff] at *
Cleared hypotheses: inst_6, q, inst_7, f, hf
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
      (Ideal.under R p))
    (Ideal.comap f.toRingHom
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
have rw : LE.le (α := Ideal R) (Ideal.under R p)
  (Ideal.comap (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.under R q)))
Tactic: rw [Ideal.map_le_iff_le_comap, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
      AlgHom.comp_algebraMap_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ LE.le (α := Ideal R) (Ideal.under R p)
    (Ideal.comap (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
have grw : LE.le (α := Ideal R) (Ideal.under R p) (Ideal.under R q)
Tactic: grw [← Ideal.le_comap_map]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
⊢ Membership.mem (γ := Submodule R R) (Ideal.under R q) x
have by_contra : ∀ (hx' : x ∉ Ideal.under R q), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
⊢ False
have this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
Tactic: have : IsLocalHom f.toRingHom := .of_surjective _ hf
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
⊢ IsUnit.{u_3} (M := Localization.AtPrime q)
    ((f.toRingHom : (a : Localization.AtPrime p) → Localization.AtPrime q)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x) :
      Localization.AtPrime q)
have suffices : IsUnit.{u_3} (M := Localization.AtPrime q)
  (IsLocalization.mk' (R := T) (M := q.primeCompl) (Localization.AtPrime q) ((algebraMap R T : (a : R) → T) x : T)
    (1 : ↥q.primeCompl))
Tactic: suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.under R p) x
hx' : x ∉ Ideal.under R q
this : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) f.toRingHom
⊢ False
have this₁ : IsUnit.{u_2} (M := Localization.AtPrime p)
  ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p)
Tactic: have := this.1 (algebraMap _ _ x) (by
      suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff])
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 :
  QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime p) (B := Ideal (Localization.AtPrime p))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
        (Ideal.under R p)))
q : Ideal T
inst_7 : q.IsPrime
f : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime p) (Localization.AtPrime q)
hf :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑f : (a : Localization.AtPrime p) → Localization.AtPrime q)
⊢ QuasiFinite.{u_1, u_3} R
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
have H : LE.le (α := Ideal (Localization.AtPrime p))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime p)) (algebraMap R (Localization.AtPrime p))
    (Ideal.under R p))
  (Ideal.comap f.toRingHom
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
      (Ideal.under R q)))
Tactic: have H : (p.under R).map (algebraMap R _) ≤
      ((q.under R).map (algebraMap R _)).comap f.toRingHom := by
    rw [Ideal.map_le_iff_le_comap, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
      AlgHom.comp_algebraMap_of_tower]
    grw [← Ideal.le_comap_map]
    intro x hx
    by_contra hx'
    have : IsLocalHom f.toRingHom := .of_surjective _ hf
    have := this.1 (algebraMap _ _ x) (by
      suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff])
    exact (IsLocalization.AtPrime.isUnit_mk'_iff (Localization.AtPrime p) p
      (algebraMap _ _ x) 1).mp (by simpa [IsLocalization.mk'_one]) hx
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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 : Ideal S
inst_5 : p.IsPrime
inst_6 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_7 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
⊢ WeaklyQuasiFiniteAt R q
have inst : Ideal.IsPrime (Ideal.comap f q)
Tactic: subst hq
Cleared hypotheses: p, inst_5, inst_6, hq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing T
inst_5 : Algebra R T
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
q : Ideal T
inst_8 : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
inst : Ideal.IsPrime (Ideal.comap f q)
⊢ WeaklyQuasiFiniteAt R q
have inst₁ : WeaklyQuasiFiniteAt R (Ideal.comap f q)
Tactic: subst hq
Cleared hypotheses: p, inst_6, inst_7, hq
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
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
⊢ p = Ideal.comap (↑f.symm : S →ₐ[R] T) (Ideal.comap f.toRingEquiv.toRingHom p)
have h : ∀ (x : S),
  x ∈ p ↔ Membership.mem (γ := Ideal S) (Ideal.comap (↑f.symm : S →ₐ[R] T) (Ideal.comap f.toRingEquiv.toRingHom p)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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
⊢ Module.Finite.{u_1, u_2} p.ResidueField q.ResidueField
have this : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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
⊢ Module.Finite.{u_1, u_2} p.ResidueField q.ResidueField
have this₁ : r.LiesOver p
Tactic: have : r.LiesOver p := .trans _ q _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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
⊢ Module.Finite.{u_4, u_2} K (Localization.AtPrime q)
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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)) ⊥)
⊢ Module.Finite.{u_4, u_2} K (Localization.AtPrime q)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (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 : WeaklyQuasiFiniteAt R Q
⊢ P = Q
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (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
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 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))
have 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)))
Tactic: rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (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
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 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)))
have 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)))
Tactic: dsimp [Ideal.under] at h₂ ⊢