awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Congruence.Hom
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 x : N
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x x

Tactic:
exact this.refl x

Premises used: Equivalence.refl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h_1 : 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 x y : N
h_2 :
  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:
this.symm h

Premises used: Equivalence.symm
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h_1 : 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 x y : N
h_2 :
  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:
exact this.symm h

Premises used: Equivalence.symm
-- Module: Mathlib.RingTheory.Congruence.Hom
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 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)) x y
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) 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:
this.trans h₁ h₂

Premises used: Equivalence.trans
-- Module: Mathlib.RingTheory.Congruence.Hom
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 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)) x y
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) 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:
exact this.trans h₁ h₂

Premises used: Equivalence.trans
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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)
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) (w + y) (x + z)

Tactic:
rcases h₁ with ⟨a, b, h1, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
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)
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))
⊢ 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 ⟨p, q, h2, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
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
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_1 :
  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)
p q : M
h2 : (c : (a : M) → M → Prop) p q
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) 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:
⟨a + p, b + q, c.add h1 h2, map_add f _ _, map_add f _ _⟩

Premises used: map_add, HAdd.hAdd, And.intro, Exists.intro, RingCon.add, Relation.Map
-- Module: Mathlib.RingTheory.Congruence.Hom
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
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_1 :
  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)
p q : M
h2 : (c : (a : M) → M → Prop) p q
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) 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:
exact ⟨a + p, b + q, c.add h1 h2, map_add f _ _, map_add f _ _⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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)
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) (w * y) (x * z)

Tactic:
rcases h₁ with ⟨a, b, h1, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
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)
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))
⊢ 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 ⟨p, q, h2, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
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
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_1 :
  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)
p q : M
h2 : (c : (a : M) → M → Prop) p q
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) 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:
⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

Premises used: HMul.hMul, RingCon.mul, map_mul, And.intro, Exists.intro, Relation.Map
-- Module: Mathlib.RingTheory.Congruence.Hom
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
a b : M
h1 : (c : (a : M) → M → Prop) a b
h_1 :
  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)
p q : M
h2 : (c : (a : M) → M → Prop) p q
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) 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:
exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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
⊢ (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

Tactic:
rw [mapGen_eq_map_of_surjective f h hf, Relation.map_apply]

Premises used: Relation.map_apply, RingCon.mapGen_eq_map_of_surjective
-- Module: Mathlib.RingTheory.Congruence.Hom
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
⊢ (c : (a : M) → M → Prop) x y →
    ∃ (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)

Tactic:
grind
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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
⊢ (∃ (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:
refine ⟨fun ⟨a, b, h₁, h₂, h₃⟩ ↦ ?_, by grind⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
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
h_1 :
  ∃ (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:
c.trans (h h₂.symm) <| c.trans h₁ <| h h₃

Premises used: RingCon.trans, Eq.symm
-- Module: Mathlib.RingTheory.Congruence.Hom
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
h_1 :
  ∃ (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:
exact c.trans (h h₂.symm) <| c.trans h₁ <| h h₃

Premises used: RingCon.trans, Eq.symm
-- Module: Mathlib.RingTheory.Congruence.Hom
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)
a :
  ∀ (x y : M),
    ((↑((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)) :
            RingCon M) :
          (a : M) → M → Prop)
        x y ↔
      ((↑d : RingCon M) : (a : M) → M → Prop) x y
⊢ (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

Tactic:
ext
-- Module: Mathlib.RingTheory.Congruence.Hom
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
a a₁ : ((↑d : RingCon M) : (a : M) → M → Prop) x y ↔ ((↑d : RingCon M) : (a : M) → M → Prop) x y
⊢ (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

Tactic:
rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le d.2) c.mk'_surjective]

Premises used: RingCon.mapGen_apply_apply_of_surjective, RingCon.mk'_surjective, RingCon.mk', Eq.trans_le, RingCon.ker_mk'_eq, Subtype.property
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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') ⋯ :
                  { 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
⊢ (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

Tactic:
ext x y
-- Module: Mathlib.RingTheory.Congruence.Hom
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
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
⊢ (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

Tactic:
obtain ⟨x, rfl⟩ := c.mk'_surjective x

Premises used: RingCon.mk'_surjective, rfl