awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i i_1 : N
hg : (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i i_1
of :
  ∀ (x y : N) (a : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y),
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y
refl : ∀ (x : N), Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x x
symm :
  ∀ {x y : N},
    RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) x
        y →
      ∀ (h : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y),
        Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) y x
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
have trans : ∀ {x y z : N},
  RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) x y →
    RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) y
        z →
      ∀ (h₁ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y)
        (h₂ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) y z),
        Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x z
Tactic: induction hg with
  | of _ _ a => exact a
  | refl x => exact this.refl x
  | symm _ h => exact this.symm h
  | trans _ _ h₁ h₂ => exact this.trans h₁ h₂
  | add _ _ h₁ h₂ =>
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a + p, b + q, c.add h1 h2, map_add f _ _, map_add f _ _⟩
  | mul _ _ h₁ h₂ =>
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i i_1 : N
hg : (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i i_1
of :
  ∀ (x y : N) (a : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y),
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y
refl : ∀ (x : N), Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x x
symm :
  ∀ {x y : N},
    RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) x
        y →
      ∀ (h : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y),
        Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) y x
trans :
  ∀ {x y z : N},
    RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) x
        y →
      RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) y
          z →
        ∀ (h₁ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y)
          (h₂ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) y z),
          Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x z
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
have add : ∀ {w x y z : N},
  RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) w x →
    RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) y
        z →
      ∀ (h₁ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) w x)
        (h₂ : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) y z),
        Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) (w + y) (x + z)
Tactic: induction hg with
  | of _ _ a => exact a
  | refl x => exact this.refl x
  | symm _ h => exact this.symm h
  | trans _ _ h₁ h₂ => exact this.trans h₁ h₂
  | add _ _ h₁ h₂ =>
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a + p, b + q, c.add h1 h2, map_add f _ _, map_add f _ _⟩
  | mul _ _ h₁ h₂ =>
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x y : M
⊢ (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) ((f : (a : M) → N) x : N)
      ((f : (a : M) → N) y) ↔
    (c : (a : M) → M → Prop) x y
have rw : (∃ (a : M) (b : M),
    (c : (a : M) → M → Prop) a b ∧
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ∧
        Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) y : N)) ↔
  (c : (a : M) → M → Prop) x y
Tactic: rw [mapGen_eq_map_of_surjective f h hf, Relation.map_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x y : M
⊢ (∃ (a : M) (b : M),
      (c : (a : M) → M → Prop) a b ∧
        Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ∧
          Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) y : N)) ↔
    (c : (a : M) → M → Prop) x y
have refine : (∃ (a : M) (b : M),
    (c : (a : M) → M → Prop) a b ∧
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ∧
        Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) y : N)) →
  ∀ (a b : M) (h₁ : (c : (a : M) → M → Prop) a b)
    (h₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N))
    (h₃ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) y : N)), (c : (a : M) → M → Prop) x y
Tactic: refine ⟨fun ⟨a, b, h₁, h₂, h₃⟩ ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : (↑(Set.Ici c) : Type u_1)
⊢ (fun (d : RingCon c.Quotient) ↦
        (Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯ : { x : RingCon M // x ∈ Set.Ici c }))
      ((fun (d : (↑(Set.Ici c) : Type u_1)) ↦
          (mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : RingCon c.Quotient))
        d) =
    d
have a : ∀ (x y : M),
  ((↑((fun (d : RingCon c.Quotient) ↦
                (Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') sorry :
                  { x : RingCon M // x ∈ Set.Ici c }))
              ((fun (d : (↑(Set.Ici c) : Type u_1)) ↦
                  (mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : RingCon c.Quotient))
                d)) :
          RingCon M) :
        (a : M) → M → Prop)
      x y ↔
    ((↑d : RingCon M) : (a : M) → M → Prop) x y
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : (↑(Set.Ici c) : Type u_1)
x y : M
⊢ (mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
    ((↑d : RingCon M) : (a : M) → M → Prop) x y
have a : ((↑d : RingCon M) : (a : M) → M → Prop) x y ↔ ((↑d : RingCon M) : (a : M) → M → Prop) x y
Tactic: rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le d.2) c.mk'_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : RingCon c.Quotient
⊢ (fun (d : (↑(Set.Ici c) : Type u_1)) ↦
        (mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : RingCon c.Quotient))
      ((fun (d : RingCon c.Quotient) ↦
          (Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯ :
            { x : RingCon M // x ∈ Set.Ici c }))
        d) =
    d
have H : ∀ (x y : c.Quotient),
  ((fun (d : (↑(Set.Ici c) : Type u_1)) ↦
            (mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : RingCon c.Quotient))
          ((fun (d : RingCon c.Quotient) ↦
              (Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') sorry :
                { x : RingCon M // x ∈ Set.Ici c }))
            d) :
        (a : c.Quotient) → c.Quotient → Prop)
      x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : RingCon c.Quotient
x y : c.Quotient
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop) x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) x y
have H : ∀ (x : M),
  (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y
Tactic: obtain ⟨x, rfl⟩ := c.mk'_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : RingCon c.Quotient
y : c.Quotient
x : M
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y
have H : ∀ (y : M),
  (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
Tactic: obtain ⟨y, rfl⟩ := c.mk'_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : RingCon c.Quotient
x y : M
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
have H : (d.comap c.mk' : (a : M) → M → Prop) x y ↔
  (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) y)
Tactic: rw [mapGen_apply_apply_of_surjective _ (comap_bot c.mk' ▸ comap_mono bot_le) c.mk'_surjective,
      comap_rel]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d_1 c : RingCon M
d : RingCon c.Quotient
x y : M
H :
  (d.comap c.mk' : (a : M) → M → Prop) x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
have H₁ : (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) y) ↔
  (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) y)
Tactic: rw [mapGen_apply_apply_of_surjective _ (comap_bot c.mk' ▸ comap_mono bot_le) c.mk'_surjective,
      comap_rel]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d c : RingCon M
s t : (↑(Set.Ici c) : Type u_1)
⊢ LE.le (α := RingCon c.Quotient)
      (({
              toFun := fun (d : (↑(Set.Ici c) : Type u_1)) ↦
                mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient),
              invFun := fun (d : RingCon c.Quotient) ↦
                Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Ici c) : Type u_1)) → RingCon c.Quotient)
          s :
        RingCon c.Quotient)
      (({
              toFun := fun (d : (↑(Set.Ici c) : Type u_1)) ↦
                mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient),
              invFun := fun (d : RingCon c.Quotient) ↦
                Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Ici c) : Type u_1)) → RingCon c.Quotient)
          t :
        RingCon c.Quotient) ↔
    s ≤ t
have simp : (∀ (x x_1 : M),
    (mapGen (M := M) (c := (↑s : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
        ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1) →
      (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
        ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
  ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y
Tactic: simp only [Equiv.coe_fn_mk, le_def, c.mk'_surjective.forall, ← Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d c : RingCon M
s t : (↑(Set.Ici c) : Type u_1)
⊢ (∀ (x x_1 : M),
      (mapGen (M := M) (c := (↑s : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1) →
        (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
    ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y
have simp_rw : (∀ (x x_1 : M),
    ((↑s : RingCon M) : (a : M) → M → Prop) x x_1 →
      (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
        ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
  ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y
Tactic: simp_rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le s.2) c.mk'_surjective,
      mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le t.2) c.mk'_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 d c : RingCon M
x_1 y_1 : M
f_1 : M →+* P
f : RingHom.{u_1, u_3} c.Quotient P
x y : M
h : (c : (a : M) → M → Prop) x y
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑x : c.Quotient) : P)
    ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
have rw : Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
  ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
Tactic: rw [c.eq.2 h]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : RingHom.{u_1, u_3} c.Quotient P
⊢ c.lift (f.comp c.mk') ⋯ = f
have a : ∀ (x : c.Quotient),
  Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') sorry : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : RingHom.{u_1, u_3} c.Quotient P
x : c.Quotient
⊢ Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)
have a : ∀ (a : M),
  Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') sorry : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
    ((f : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
Tactic: rcases x with ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔ c = ker f
have refine : c = ker f → Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P)
Tactic: refine ⟨fun H ↦ ext'' (Setoid.ker_eq_lift_of_injective f h H).symm, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : N →+* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
        (↑((f : (a : N) → M) x) : c.Quotient) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)
have rw : Eq.{u_2 + 1} (α := d.Quotient)
  (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
      ((c.comapQuotientEquivOfSurj f hf hcd : (a : d.Quotient) → c.Quotient) (↑x : d.Quotient)) :
    d.Quotient)
  ((↑x : d.Quotient) : d.Quotient)
Tactic: rw [← c.comapQuotientEquivOfSurj_mk hf hcd x, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : N →+* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
d : RingCon N
hcd : d = c.comap f
x : N
rw :
  Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
        ((c.comapQuotientEquivOfSurj f hf hcd : (a : d.Quotient) → c.Quotient) (↑x : d.Quotient)) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
        (↑((f : (a : N) → M) x) : c.Quotient) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)
have rw₁ : Eq (α := d.Quotient) (↑x : d.Quotient) (↑x : d.Quotient)
Tactic: rw [← c.comapQuotientEquivOfSurj_mk hf hcd x, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((RingEquiv.symm (c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd) : RingEquiv.{u_1, u_2} c.Quotient d.Quotient) :
          (a : c.Quotient) → d.Quotient)
        ⟦(f : (a : N) → M) x⟧ :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)
have h : ⟦(f : (a : N) → M) x⟧ =
  ((c.comapQuotientEquivOfSurj (↑f : N →+* M) sorry hcd : RingEquiv.{u_2, u_1} d.Quotient c.Quotient) :
      (a : d.Quotient) → c.Quotient)
    (↑x : d.Quotient)
Tactic: convert! RingEquiv.symm_apply_apply _ _
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦(f : (a : N) → M) x⟧ =
    ((c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd : RingEquiv.{u_2, u_1} d.Quotient c.Quotient) :
        (a : d.Quotient) → c.Quotient)
      (↑x : d.Quotient)
have h : ⟦(f : (a : N) → M) x⟧ = (↑((f : (a : N) → M) x) : c.Quotient)
Tactic: rw [comapQuotientEquivOfSurj_mk, RingEquiv.coe_toRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c_1 : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HAdd.hAdd (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    HAdd.hAdd (α := d.Quotient) (β := d.Quotient) ((d.mk' : (a : M) → d.Quotient) a : d.Quotient)
      ((d.mk' : (a : M) → d.Quotient) b : d.Quotient)
have rw : (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
    (HAdd.hAdd (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
      (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
  (d.mk' : (a : M) → d.Quotient) (a + b)
Tactic: rw [← d.mk'.map_add]