awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : Mul R
c_1 d : RingCon R
inst_2 : Subsingleton R
c c' : RingCon R
r r' : R
simp_rw : (c : (a : R) → R → Prop) r r ↔ (c' : (a : R) → R → Prop) r r
⊢ (c : (a : R) → R → Prop) r r' ↔ (c' : (a : R) → R → Prop) r r'
have simp_rw₁ : True ↔ (c' : (a : R) → R → Prop) r r
Tactic: simp_rw [Subsingleton.elim r' r, c.refl, c'.refl]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R
have inl : Subsingleton R → (Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
inl : Subsingleton R → (Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R)
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R
have inr : Nontrivial R → (Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R
have inl : Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R
Tactic: simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R
have inl : Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R
Tactic: on_goal 1 => simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R
have simp_rw : ¬Nontrivial.{u_3} (RingCon R) ↔ ¬Nontrivial R
Tactic: simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → (c : (a : R) → R → Prop) x y
⊢ ringConGen r ≤ c
have rw : sInf {s : RingCon R | ∀ (x y : R), r x y → (s : (a : R) → R → Prop) x y} ≤ c
Tactic: rw [ringConGen_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ ringConGen (⇑c : (a : R) → R → Prop) ≤ c
have rw : sInf {s : RingCon R | ∀ (x y : R), (c : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y} ≤ c
Tactic: rw [ringConGen_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ c ⊔ d = ringConGen fun (x y : R) ↦ (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y
have rw : c ⊔ d =
  sInf
    {s : RingCon R |
      ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}
Tactic: rw [ringConGen_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ c ⊔ d =
    sInf
      {s : RingCon R |
        ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}
have apply : Eq.{u_3 + 1} (α := Set (RingCon R)) {x : RingCon R | c ≤ x ∧ d ≤ x}
  {s : RingCon R |
    ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ c ⊔ d = ringConGen ((⇑c : (a : R) → R → Prop) ⊔ (⇑d : (a : R) → R → Prop))
have rw : Eq (α := RingCon R) (ringConGen fun (x y : R) ↦ (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y)
  (ringConGen ((⇑c : (a : R) → R → Prop) ⊔ (⇑d : (a : R) → R → Prop)))
Tactic: rw [sup_eq_ringConGen]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y
have rw : sSup S = sInf {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
Tactic: rw [ringConGen_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ sSup S = sInf {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
have apply : upperBounds S = {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ upperBounds S = {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
have h : ∀ (x : RingCon R),
  x ∈ upperBounds S ↔
    Membership.mem (γ := Set (RingCon R))
      {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y} x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen (sSup (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S))
have rw : Eq.{u_3 + 1} (α := RingCon R) (ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y)
  (ringConGen (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)))
Tactic: rw [sSup_eq_ringConGen, sSup_image]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ Eq.{u_3 + 1} (α := RingCon R) (ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y)
    (ringConGen (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)))
have e_r : ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)) x y
Tactic: congr with (x y)
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Defs (goal)
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ Eq.{u_1 + 1} (α := Con R) ((fun (c : RingCon R) ↦ c.toCon) c) ((fun (c : RingCon R) ↦ c.toCon) d) → c = d
have mk : ∀ (toCon : Con R)
  (add' :
    ∀ {w x y z : R},
      (toCon.toSetoid : R → R → Prop) w x →
        (toCon.toSetoid : R → R → Prop) y z → (toCon.toSetoid : R → R → Prop) (w + y) (x + z)),
  Eq.{u_1 + 1} (α := Con R) ((fun (c : RingCon R) ↦ c.toCon) { toCon := toCon, add' := @add' })
      ((fun (c : RingCon R) ↦ c.toCon) d) →
    { toCon := toCon, add' := @add' : RingCon R } = d
Tactic: cases c
Cleared hypotheses: c
-- 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
g : N →+* M
⊢ c.comap g = ker (c.mk'.comp g)
have rw : Eq (α := RingCon N) (c.comap g) ((ker c.mk').comap g)
Tactic: rw [ker_comp, ker_mk'_eq]
-- 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
g : N →+* M
rw : Eq (α := RingCon N) (c.comap g) ((ker c.mk').comap g)
⊢ c.comap g = ker (c.mk'.comp g)
have rw₁ : Eq (α := RingCon N) (c.comap g) (c.comap g)
Tactic: rw [ker_comp, ker_mk'_eq]
-- 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 d : RingCon M
h : c = d
x y : c.Quotient
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x * (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) sorry).toFun y
Tactic: rcases x with ⟨⟩
-- 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 d : RingCon M
h : c = d
x y : c.Quotient
a : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a_1 : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun
      (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
Tactic: rcases y with ⟨⟩
-- 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 d : RingCon M
h : c = d
x y : c.Quotient
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x + y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x + (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a + y) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
      (Quotient.congr (Equiv.refl M) sorry).toFun y
Tactic: rcases x with ⟨⟩
-- 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 d : RingCon M
h : c = d
x y : c.Quotient
a : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a + y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
      (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a_1 : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun
      (HAdd.hAdd (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
      (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
Tactic: rcases y with ⟨⟩
-- 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)
⊢ Eq.{u_2 + 1} (α := (a : N) → N → Prop)
    (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))
have refine : LE.le.{u_2} (α := (a : N) → N → Prop) (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
  (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))
Tactic: refine le_antisymm ?_ <| (RingCon.gi N).gc.le_u_l _
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Hom (hypothesis)
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)
⊢ LE.le.{u_2} (α := (a : N) → N → Prop) (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))
have 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))
Tactic: have := Relation.map_equivalence c.toSetoid.2 _ hf h
-- 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 : N
⊢ LE.le (α := (fun (a : N) ↦ N → Prop) i)
    ((mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i : N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i : N → Prop)
have _ : ∀ (i_1 : N),
  (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i i_1 ≤
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
Tactic: _
-- 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 w x y z : N
h_1 :
  RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) w x
h_2 :
  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)
have add : ∀ (a b : M) (h1 : (c : (a : M) → M → Prop) a b),
  RingConGen.Rel.{u_2} (R := N)
      (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
      ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) →
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
      (HAdd.hAdd (α := N) ((f : (a : M) → N) a : N) y) (HAdd.hAdd (α := N) ((f : (a : M) → N) b : N) z)
Tactic: rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
Cleared hypotheses: w, x, h_1, h₁
-- 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 y z : N
h_1 :
  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) y z
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_2 :
  RingConGen.Rel.{u_2} (R := N)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
    ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
    (HAdd.hAdd (α := N) ((f : (a : M) → N) a : N) y) (HAdd.hAdd (α := N) ((f : (a : M) → N) b : N) z)
have add : ∀ (p q : M) (h2 : (c : (a : M) → M → Prop) p q),
  RingConGen.Rel.{u_2} (R := N)
      (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
      ((f : (a : M) → N) p : N) ((f : (a : M) → N) q : N) →
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
      (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) p : N))
      (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) q : N))
Tactic: rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
Cleared hypotheses: y, z, h_1, h₂
-- 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 w x y z : N
h_1 :
  RingConGen.Rel (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)) w x
h_2 :
  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)
have mul : ∀ (a b : M) (h1 : (c : (a : M) → M → Prop) a b),
  RingConGen.Rel.{u_2} (R := N)
      (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
      ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) →
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
      (HMul.hMul (α := N) ((f : (a : M) → N) a : N) y) (HMul.hMul (α := N) ((f : (a : M) → N) b : N) z)
Tactic: rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
Cleared hypotheses: w, x, h_1, h₁
-- 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 y z : N
h_1 :
  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) y z
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_2 :
  RingConGen.Rel.{u_2} (R := N)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
    ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
    (HMul.hMul (α := N) ((f : (a : M) → N) a : N) y) (HMul.hMul (α := N) ((f : (a : M) → N) b : N) z)
have mul : ∀ (p q : M) (h2 : (c : (a : M) → M → Prop) p q),
  RingConGen.Rel.{u_2} (R := N)
      (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) : N → N → Prop)
      ((f : (a : M) → N) p : N) ((f : (a : M) → N) q : N) →
    Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) p : N))
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) q : N))
Tactic: rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
Cleared hypotheses: y, z, h_1, h₂
-- 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
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
have 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
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
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
have refl : ∀ (x : N), Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x x
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
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
have 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
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