-- 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
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
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)
mul :
  ∀ {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)
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1

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 _ _⟩

Premises used: rfl