-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h_1 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 : N
h : (conGen rel : (a : N) → N → Prop) n1 n2
of :
  ∀ (x y : N) (h : rel x y) (a b : M),
    (f : (a : M) → N) a = x →
      (f : (a : M) → N) b = y →
        (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
refl :
  ∀ (x : N) (a b : M),
    (f : (a : M) → N) a = x →
      (f : (a : M) → N) b = x →
        (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
symm :
  ∀ {x y : N},
    ConGen.Rel rel x y →
      ∀
        (h :
          ∀ (a b : M),
            (f : (a : M) → N) a = x →
              (f : (a : M) → N) b = y →
                (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b)
        (a b : M),
        (f : (a : M) → N) a = y →
          (f : (a : M) → N) b = x →
            (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
trans :
  ∀ {x y z : N},
    ConGen.Rel rel x y →
      ConGen.Rel rel y z →
        ∀
          (ih :
            ∀ (a b : M),
              (f : (a : M) → N) a = x →
                (f : (a : M) → N) b = y →
                  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b)
          (ih1 :
            ∀ (a b : M),
              (f : (a : M) → N) a = y →
                (f : (a : M) → N) b = z →
                  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b)
          (a b : M),
          (f : (a : M) → N) a = x →
            (f : (a : M) → N) b = z →
              (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
mul :
  ∀ {w x y z : N},
    ConGen.Rel rel w x →
      ConGen.Rel rel y z →
        ∀
          (ih :
            ∀ (a b : M),
              (f : (a : M) → N) a = w →
                (f : (a : M) → N) b = x →
                  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b)
          (ih1 :
            ∀ (a b : M),
              (f : (a : M) → N) a = y →
                (f : (a : M) → N) b = z →
                  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b)
          (a b : M),
          (f : (a : M) → N) a = w * y →
            (f : (a : M) → N) b = x * z →
              (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
⊢ ∀ (a b : M),
    (f : (a : M) → N) a = n1 →
      (f : (a : M) → N) b = n2 →
        (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b

Tactic:
induction h with
    | of x y h =>
      intro _ _ fa fb
      apply ConGen.Rel.of
      rwa [fa, fb]
    | refl x =>
      intro _ _ fc fd
      rw [f.injective (fc.trans fd.symm)]
      exact ConGen.Rel.refl _
    | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
    | trans _ _ ih ih1 =>
      exact fun a b fa fb ↦ Exists.casesOn (f.surjective _) fun c' hc' ↦
      ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
    | mul _ _ ih ih1 =>
      rename_i w x y z _ _
      intro a b fa fb
      rw [← f.eq_symm_apply, map_mul] at fa fb
      rw [fa, fb]
      exact ConGen.Rel.mul (ih (f.symm w) (f.symm x) (by simp) (by simp))
        (ih1 (f.symm y) (f.symm z) (by simp) (by simp))

Premises used: MulEquiv.eq_symm_apply, map_mul, ConGen.Rel.refl, ConGen.Rel.of