awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₄ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₅ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I)))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₅ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₆ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ I)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₅ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₆ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ I)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₇ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) J ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I)
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₅ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₆ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ I)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₇ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) J ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I)
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₈ : Eq (α := Ideal (R ⧸ J)) (⊥ ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₃ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₅ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₆ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ I)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₇ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) J ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I)
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₈ : Eq (α := Ideal (R ⧸ J)) (⊥ ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₉ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Injective.{u + 1, v + 1} (α := R ⧸ J) (β := S ⧸ I) (⇑(quotientMap I f H) : (a : R ⧸ J) → S ⧸ I)
have refine : ∀ (a : R ⧸ J)
  (ha :
    Eq.{v + 1} (α := S ⧸ I) (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      (0 : S ⧸ I)),
  a = 0
Tactic: refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha :
  Eq.{v + 1} (α := S ⧸ I) (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
    (0 : S ⧸ I)
⊢ a = 0
have obtain : ∀ (r : R)
  (ha :
    Eq.{v + 1} (α := S ⧸ I)
      (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
          ((Quotient.mk J : (a : R) → R ⧸ J) r) :
        S ⧸ I)
      (0 : S ⧸ I)),
  Eq (α := R ⧸ J) ((Quotient.mk J : (a : R) → R ⧸ J) r : R ⧸ J) (0 : R ⧸ J)
Tactic: obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha :
  Eq.{v + 1} (α := S ⧸ I)
    (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
        ((Quotient.mk J : (a : R) → R ⧸ J) r) :
      S ⧸ I)
    (0 : S ⧸ I)
⊢ Eq (α := R ⧸ J) ((Quotient.mk J : (a : R) → R ⧸ J) r : R ⧸ J) (0 : R ⧸ J)
have ha₁ : Membership.mem (α := S) I ((f : (a : R) → S) r : S)
Tactic: rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
⊢ let leq : LE.le (α := Ideal R) (comap f (comap g' I)) (comap g (comap f' I)) := ⋯;
  Eq (α := RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g leq))
have refine : ∀ (a : HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))),
  Eq.{u_6 + 1} (α := S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' sorry) (quotientMap (comap g' I) f sorry) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' sorry) (quotientMap (comap f' I) g sorry) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)
Tactic: refine RingHom.ext fun a => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
a : HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))
⊢ Eq.{u_6 + 1} (α := S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g ⋯) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)
have obtain : ∀ (r : R),
  Eq.{u_6 + 1} (α := S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' sorry) (quotientMap (comap g' I) f sorry) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        ((Quotient.mk (comap f (comap g' I)) : (a : R) → R ⧸ comap f (comap g' I)) r) :
      S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' sorry) (quotientMap (comap f' I) g sorry) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        ((Quotient.mk (comap f (comap g' I)) : (a : R) → R ⧸ comap f (comap g' I)) r) :
      S' ⧸ I)
Tactic: obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
⊢ r₁ • a₁ ≈ r₂ • a₂
have this : Membership.mem (γ := Submodule R R) (comap (F := R →+* A) (algebraMap R A) P) (r₁ - r₂)
Tactic: have := h (p.quotientRel_def.mp hr)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : Membership.mem (γ := Submodule R R) (comap (F := R →+* A) (algebraMap R A) P) (r₁ - r₂)
⊢ r₁ • a₁ ≈ r₂ • a₂
have this₁ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) r₁ : A) ((algebraMap R A : (a : R) → A) r₂ : A) ∈ P
Tactic: rw [mem_comap, map_sub] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab :
  Eq.{u_3 + 1} (α := A ⧸ I)
    ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)) (A ⧸ I) :
          (a : R ⧸ comap (algebraMap R A) I) → A ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a) :
      A ⧸ I)
    ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)) (A ⧸ I) :
          (a : R ⧸ comap (algebraMap R A) I) → A ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b) :
      A ⧸ I)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I))
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a)
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b)
have hab₁ : HSub.hSub (α := A) (β := A) (((algebraMap R A : R →+* A) : (a : R) → A) a : A)
    (((algebraMap R A : R →+* A) : (a : R) → A) b : A) ∈
  I
Tactic: replace hab := Quotient.eq.mp hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab :
  HSub.hSub (α := A) (β := A) (((algebraMap R A : R →+* A) : (a : R) → A) a : A)
      (((algebraMap R A : R →+* A) : (a : R) → A) b : A) ∈
    I
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I))
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a)
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b)
have hab₁ : Membership.mem (α := A) I (((algebraMap R A : R →+* A) : (a : R) → A) (a - b) : A)
Tactic: rw [← map_sub] at hab
Cleared hypotheses: hab