-- Mathlib/GroupTheory/Congruence/Basic.lean
theorem comap_conGen_equiv {M N : Type*} [Mul M] [Mul N] (f : MulEquiv M N) (rel : N → N → Prop) :
    Con.comap f (map_mul f) (conGen rel) = conGen (fun x y ↦ rel (f x) (f y))

Proof state:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
⊢ ∀ (a b : M), f a = w * y → f b = x * z → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
intro a b fa fb

Result:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : f a = w * y
fb : f b = x * z
⊢ (conGen fun x y => rel (f x) (f y)) a b

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm z) = z

Tactic:
simp

Result:
no goals

Proof state:
case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h✝ : (conGen rel) (f a) (f b)
n1 n2 x y : N
h : rel x y
⊢ ∀ (a b : M), f a = x → f b = y → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
intro _ _ fa fb

Result:
case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h✝ : (conGen rel) (f a) (f b)
n1 n2 x y : N
h : rel x y
a✝ b✝ : M
fa : f a✝ = x
fb : f b✝ = y
⊢ (conGen fun x y => rel (f x) (f y)) a✝ b✝

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
H : ∀ (n1 n2 : N), (conGen rel) n1 n2 → ∀ (a b : M), f a = n1 → f b = n2 → (conGen fun x y => rel (f x) (f y)) a b
⊢ (conGen fun x y => rel (f x) (f y)) a b

Tactic:
exact H (f a) (f b) h a b (refl _) (refl _)

Result:
no goals

Proof state:
case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
n1 n2 x : N
⊢ ∀ (a b : M), f a = x → f b = x → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
intro _ _ fc fd

Result:
case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
n1 n2 x : N
a✝ b✝ : M
fc : f a✝ = x
fd : f b✝ = x
⊢ (conGen fun x y => rel (f x) (f y)) a✝ b✝

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm y) = y

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
⊢ (conGen fun x y => rel (f x) (f y)) a b

Tactic:
have H : ∀ n1 n2, (conGen rel) n1 n2 → ∀ a b, f a = n1 → f b = n2 →
    (conGen fun x y ↦ rel (f x) (f y)) a b := by
  intro n1 n2 h
  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))

Result:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
H : ∀ (n1 n2 : N), (conGen rel) n1 n2 → ∀ (a b : M), f a = n1 → f b = n2 → (conGen fun x y => rel (f x) (f y)) a b
⊢ (conGen fun x y => rel (f x) (f y)) a b

Proof state:
case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
n1 n2 x : N
a✝ b✝ : M
fc : f a✝ = x
fd : f b✝ = x
⊢ (conGen fun x y => rel (f x) (f y)) b✝ b✝

Tactic:
exact ConGen.Rel.refl _

Result:
no goals

Proof state:
case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h✝ : (conGen rel) (f a) (f b)
n1 n2 x y : N
h : rel x y
a✝ b✝ : M
fa : f a✝ = x
fb : f b✝ = y
⊢ (conGen fun x y => rel (f x) (f y)) a✝ b✝

Tactic:
apply ConGen.Rel.of

Result:
case of.a
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h✝ : (conGen rel) (f a) (f b)
n1 n2 x y : N
h : rel x y
a✝ b✝ : M
fa : f a✝ = x
fb : f b✝ = y
⊢ rel (f a✝) (f b✝)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm x) = x

Tactic:
simp

Result:
no goals

Proof state:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y => rel (f x) (f y)) a b

Tactic:
rw [fa, fb]

Result:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a✝² b✝ : M
h : (conGen rel) (f a✝²) (f b✝)
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ (a b : M), f a = w → f b = x → (conGen fun x y => rel (f x) (f y)) a b
ih1 : ∀ (a b : M), f a = y → f b = z → (conGen fun x y => rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y => rel (f x) (f y)) (f.symm w * f.symm y) (f.symm x * f.symm z)