awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (comap (⇑f : (a : M) → N) ⋯ (conGen rel) : (a : M) → M → Prop) a b
⊢ (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)

Tactic:
simp only [Con.comap_rel] at h

Premises used: Con.comap_rel
-- 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 x y : N
h : rel x y
a_1 : M
of :
  ∀ (b : M),
    (f : (a : M) → N) a_1 = 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_1 b
⊢ ∀ (b : M),
    (f : (a : M) → N) a_1 = 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_1 b

Tactic:
_
-- 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 x y : N
h : rel x y
a_1 b_1 : M
fa : (f : (a : M) → N) a_1 = x
fb : (f : (a : M) → N) b_1 = y
of : rel ((f : (a : M) → N) a_1) ((f : (a : M) → N) b_1)
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a_1 b_1

Tactic:
apply ConGen.Rel.of

Premises used: ConGen.Rel.of
-- 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 x y : N
h : rel x y
a_1 b_1 : M
fa : (f : (a : M) → N) a_1 = x
fb : (f : (a : M) → N) b_1 = y
of : rel x ((f : (a : M) → N) b_1)
of₁ of₂ of₃ of₄ : rel x y
⊢ rel ((f : (a : M) → N) a_1) ((f : (a : M) → N) b_1)

Tactic:
rwa [fa, fb]
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x : N
a_1 : M
refl :
  ∀ (b : M),
    (f : (a : M) → N) a_1 = 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_1 b
⊢ ∀ (b : M),
    (f : (a : M) → N) a_1 = 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_1 b

Tactic:
_
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x : N
a_1 b_1 : M
fc : (f : (a : M) → N) a_1 = x
fd : (f : (a : M) → N) b_1 = x
refl : (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) b_1 b_1
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a_1 b_1

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

Premises used: Eq.symm, MulEquiv.injective, Eq.trans
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x : N
a_1 b_1 : M
fc : (f : (a : M) → N) a_1 = x
fd : (f : (a : M) → N) b_1 = x
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) b_1 b_1

Tactic:
ConGen.Rel.refl _

Premises used: ConGen.Rel.refl
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x : N
a_1 b_1 : M
fc : (f : (a : M) → N) a_1 = x
fd : (f : (a : M) → N) b_1 = x
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) b_1 b_1

Tactic:
exact ConGen.Rel.refl _

Premises used: ConGen.Rel.refl
-- 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 x y : N
h_2 : 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

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

Premises used: ConGen.Rel.symm
-- 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 x y : N
h_2 : 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

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

Premises used: ConGen.Rel.symm
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x y z : N
h_1 : ConGen.Rel rel x y
h_2 : 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

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

Premises used: MulEquiv.surjective, Exists.casesOn
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
n1 n2 x y z : N
h_1 : ConGen.Rel rel x y
h_2 : 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

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)
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : (f : (a : M) → N) a = w * y
fb : (f : (a : M) → N) b = x * z
⊢ a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)

Tactic:
rw [← f.eq_symm_apply, map_mul] at fa fb

Premises used: MulEquiv.eq_symm_apply, map_mul
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : (f : (a : M) → N) a = w * y
fb : (f : (a : M) → N) b = x * z
fa₁ : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
⊢ b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)

Tactic:
rw [← f.eq_symm_apply, map_mul] at fa fb

Premises used: MulEquiv.eq_symm_apply, map_mul
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
mul :
  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop)
    (HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M))
    (HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M))
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b

Tactic:
rw [fa, fb]
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
⊢ (f : (a : M) → N) ((f.symm : (a : N) → M) w : M) = w

Tactic:
simp
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
⊢ (f : (a : M) → N) ((f.symm : (a : N) → M) x : M) = x

Tactic:
simp
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
⊢ (f : (a : M) → N) ((f.symm : (a : N) → M) y : M) = y

Tactic:
simp
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
⊢ (f : (a : M) → N) ((f.symm : (a : N) → M) z : M) = z

Tactic:
simp
-- 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_1 b_1 : M
h : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a_1 : N) ((f : (a : M) → N) b_1)
n1 n2 w x y z : N
h_1 : ConGen.Rel rel w x
h_2 : 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
fa : a = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M)
fb : b = HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M)
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop)
    (HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) w : M) ((f.symm : (a : N) → M) y : M))
    (HMul.hMul (α := M) (β := M) ((f.symm : (a : N) → M) x : M) ((f.symm : (a : N) → M) z : M))

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

Premises used: ConGen.Rel.mul, MulEquiv.symm, DFunLike.coe
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
⊢ ∀ (n1 n2 : N),
    (conGen rel : (a : N) → N → Prop) n1 n2 →
      ∀ (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:
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))
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
H :
  ∀ (n1 n2 : N),
    (conGen rel : (a : N) → N → Prop) n1 n2 →
      ∀ (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
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b

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

Premises used: refl, DFunLike.coe
-- 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 : (conGen rel : (a : N) → N → Prop) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b)
H :
  ∀ (n1 n2 : N),
    (conGen rel : (a : N) → N → Prop) n1 n2 →
      ∀ (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
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b

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

Premises used: refl, DFunLike.coe
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M → N
hf : Bijective f
H : ∀ (x y : M), f (x * y) = f x * f y
rel : N → N → Prop
⊢ comap f H (conGen rel) = conGen fun (x y : M) ↦ rel (f x) (f y)

Tactic:
comap_conGen_equiv (MulEquiv.ofBijective (MulHom.mk f H) hf) rel

Premises used: MulHom.mk, MulEquiv.ofBijective, Con.comap_conGen_equiv
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
inst : MulOneClass M
c : Con M
x y : M
⊢ (x, y) ∈ (↑c : Submonoid (M × M)) ↔ (x, y) ∈ c

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
inst : MulOneClass M
c d : Con M
H : (↑c : Submonoid (M × M)) = (↑d : Submonoid (M × M))
⊢ c = d

Tactic:
ext fun x y => show (x, y) ∈ c.submonoid ↔ (x, y) ∈ d from H ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, Con.ext, Eq.symm
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
inst : MulOneClass M
c d : Con M
⊢ c ≤ d ↔ (↑c : Submonoid (M × M)) ≤ (↑d : Submonoid (M × M))

Tactic:
⟨fun h _ H => h H, fun h x y hc => h <| show (x, y) ∈ c from hc⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
inst : MulOneClass M
c : Con M
⊢ Eq (α := Submonoid c.Quotient) (MonoidHom.mrange c.mk') ⊤

Tactic:
MonoidHom.mrange_eq_top.2 mk'_surjective

Premises used: Iff.mpr, Con.mk'_surjective, MonoidHom.mrange_eq_top
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w : c.Quotient
y : M
hy : (c.lift f H : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) = x
⊢ Membership.mem (γ := Submonoid P) (MonoidHom.mrange f) x

Tactic:
⟨y, hy⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w : c.Quotient
y : M
hy : (c.lift f H : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) = x
⊢ Membership.mem (γ := Submonoid P) (MonoidHom.mrange f) x

Tactic:
exact ⟨y, hy⟩
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
f : M →* P
⊢ Eq (α := Submonoid P) (MonoidHom.mrange (kerLift f)) (MonoidHom.mrange f)

Tactic:
lift_range fun _ _ => id

Premises used: id, Con.lift_range, Con.kerLift
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y_1 : M
f_1 f : M →* P
x y : Con.Quotient (ker f)
h :
  Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) x :
      ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) y :
      ↥(MonoidHom.mrange (kerLift f)))
mk :
  ∀ (a : M)
    (h :
      Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
        (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
            (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
          ↥(MonoidHom.mrange (kerLift f)))
        (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) y :
          ↥(MonoidHom.mrange (kerLift f)))),
    Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
      ((kerLift f : (a : (ker f).Quotient) → P) y : P)
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) x : P)
    ((kerLift f : (a : (ker f).Quotient) → P) y : P)

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y_1 : M
f_1 f : M →* P
x y : Con.Quotient (ker f)
a : M
h :
  Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
        (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
      ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) y :
      ↥(MonoidHom.mrange (kerLift f)))
mk :
  ∀ (a_1 : M)
    (h :
      Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
        (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
            (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
          ↥(MonoidHom.mrange (kerLift f)))
        (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
            (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) :
          ↥(MonoidHom.mrange (kerLift f)))),
    Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
      ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) : P)
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) y : P)

Tactic:
rcases y with ⟨⟩