-- 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:
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 : (comap ⇑f ⋯ (conGen rel)) a b
⊢ (conGen fun x y => rel (f x) (f y)) a b

Tactic:
simp only [Con.comap_rel] at h

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)
⊢ (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
⊢ comap ⇑f ⋯ (conGen rel) ≤ conGen fun x y => rel (f x) (f y)

Tactic:
intro a b h

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 : (comap ⇑f ⋯ (conGen rel)) a b
⊢ (conGen fun x y => rel (f x) (f y)) a b

Proof state:
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✝)

Tactic:
rwa [fa, fb]

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
⊢ comap ⇑f ⋯ (conGen rel) = conGen fun x y => rel (f x) (f y)

Tactic:
apply le_antisymm _ (le_comap_conGen f (map_mul f) rel)

Result:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
⊢ comap ⇑f ⋯ (conGen rel) ≤ conGen fun x y => rel (f x) (f y)

Proof state:
case trans
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✝ z✝ : N
a✝¹ : ConGen.Rel rel x✝ y✝
a✝ : ConGen.Rel rel y✝ z✝
ih : ∀ (a b : M), f a = x✝ → f b = y✝ → (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 = x✝ → f b = z✝ → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
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)

Result:
no goals

Proof state:
case symm
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
a✝ : ConGen.Rel rel x✝ y✝
h : ∀ (a b : M), f a = x✝ → f b = y✝ → (conGen fun x y => rel (f x) (f y)) a b
⊢ ∀ (a b : M), f a = y✝ → f b = x✝ → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)

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), f a = w✝ * y✝ → f b = x✝ * z✝ → (conGen fun x y => rel (f x) (f y)) a b

Tactic:
rename_i w x y z _ _

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), f a = w * y → f b = x * z → (conGen fun x y => rel (f x) (f y)) a b

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)) (f.symm w * f.symm y) (f.symm x * f.symm z)

Tactic:
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:
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)
⊢ ∀ (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

Tactic:
intro n1 n2 h

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)
n1 n2 : N
h : (conGen rel) n1 n2
⊢ ∀ (a b : M), f a = n1 → f b = n2 → (conGen fun x y => rel (f x) (f y)) a b

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 : f a = w * y
fb : f b = x * z
⊢ (conGen fun x y => rel (f x) (f y)) a b

Tactic:
rw [← f.eq_symm_apply, map_mul] at 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)) 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 w) = w

Tactic:
simp

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
fc : f a✝ = x
fd : f b✝ = x
⊢ (conGen fun x y => rel (f x) (f y)) a✝ b✝

Tactic:
rw [f.injective (fc.trans fd.symm)]

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)) b✝ 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 : N
h : (conGen rel) n1 n2
⊢ ∀ (a b : M), f a = n1 → f b = n2 → (conGen fun x y => rel (f x) (f y)) 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))

Result:
no goals