awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → (c : (a : M) → M → Prop) (x * y) 1 → (c : (a : M) → M → Prop) (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1) (x' y' : M)
    (hxy' : (c : (a : M) → M → Prop) (x' * y') 1) (hyx' : (c : (a : M) → M → Prop) (y' * x') 1),
    (c : (a : M) → M → Prop) x x' → (c : (a : M) → M → Prop) y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : (c : (a : M) → M → Prop) x x'
hy : (c : (a : M) → M → Prop) y y'
Hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1
Hxy' : HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1
refine_2 :
  (HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)
refine_2₁ :
  ∀ (a : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1)
    (a' : HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1),
    a ≍ a' →
      HEq.{u_4 + 1} (α := α)
        ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
              (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
            f x y ⋯ ⋯)
          x y Hxy a)
        (β := α)
        ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
              (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
            f x y ⋯ ⋯)
          x' y' Hxy' a')
⊢ HEq.{u_4 + 1} (α := (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) → α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x y Hxy)
    (β := (hyx : HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1) → α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x' y' Hxy')

Tactic:
refine Function.hfunext ?_ ?_

Premises used: Function.hfunext
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → (c : (a : M) → M → Prop) (x * y) 1 → (c : (a : M) → M → Prop) (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1) (x' y' : M)
    (hxy' : (c : (a : M) → M → Prop) (x' * y') 1) (hyx' : (c : (a : M) → M → Prop) (y' * x') 1),
    (c : (a : M) → M → Prop) x x' → (c : (a : M) → M → Prop) y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : (c : (a : M) → M → Prop) x x'
hy : (c : (a : M) → M → Prop) y y'
Hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1
Hxy' : HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1
refine_2 :
  (HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x' : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)
refine_2₁ refine_2₂ :
  (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)
⊢ (HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)

Tactic:
rw [c.eq.2 hx, c.eq.2 hy]

Premises used: Iff.mpr, Con.eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → (c : (a : M) → M → Prop) (x * y) 1 → (c : (a : M) → M → Prop) (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1) (x' y' : M)
    (hxy' : (c : (a : M) → M → Prop) (x' * y') 1) (hyx' : (c : (a : M) → M → Prop) (y' * x') 1),
    (c : (a : M) → M → Prop) x x' → (c : (a : M) → M → Prop) y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : (c : (a : M) → M → Prop) x x'
hy : (c : (a : M) → M → Prop) y y'
Hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1
Hxy' : HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1
Hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1
Hyx' : HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1
⊢ HEq.{u_4 + 1} (α := α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x y Hxy Hyx)
    (β := α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x' y' Hxy' Hyx')

Tactic:
heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

Premises used: heq_of_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → (c : (a : M) → M → Prop) (x * y) 1 → (c : (a : M) → M → Prop) (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1) (x' y' : M)
    (hxy' : (c : (a : M) → M → Prop) (x' * y') 1) (hyx' : (c : (a : M) → M → Prop) (y' * x') 1),
    (c : (a : M) → M → Prop) x x' → (c : (a : M) → M → Prop) y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : (c : (a : M) → M → Prop) x x'
hy : (c : (a : M) → M → Prop) y y'
Hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1
Hxy' : HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1
Hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1
Hyx' : HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1
⊢ HEq.{u_4 + 1} (α := α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x y Hxy Hyx)
    (β := α)
    ((fun (x y : M) (hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
          (hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) ↦
        f x y ⋯ ⋯)
      x' y' Hxy' Hyx')

Tactic:
exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

Premises used: heq_of_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
α : Type u_4
inst : Monoid M
c : Con M
f : (x y : M) → (c : (a : M) → M → Prop) (x * y) 1 → (c : (a : M) → M → Prop) (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1) (x' y' : M)
    (hxy' : (c : (a : M) → M → Prop) (x' * y') 1) (hyx' : (c : (a : M) → M → Prop) (y' * x') 1),
    (c : (a : M) → M → Prop) x x' → (c : (a : M) → M → Prop) y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y : M
hxy : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1
hyx : HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1
⊢ liftOnUnits { val := (↑x : c.Quotient), inv := (↑y : c.Quotient), val_inv := hxy, inv_val := hyx : c.Quotientˣ } f
      Hf =
    f x y ⋯ ⋯

Tactic:
rfl

Premises used: Con.hrecOn₂, Quotient.hrecOn₂', Quotient.hrecOn₂, Quot.hrecOn₂, Con.toQuotient, Con.liftOnUnits, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
p : c.Quotientˣ → Prop
u : c.Quotientˣ
H :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1),
    p { val := (↑x : c.Quotient), inv := (↑y : c.Quotient), val_inv := ⋯, inv_val := ⋯ }
mk :
  ∀ (val inv : c.Quotient) (x y : M)
    (h₁ :
      HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) = 1)
    (h₂ :
      HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) =
        1),
    p
      { val := Quot.mk (⇑c.toSetoid : M → M → Prop) x, inv := Quot.mk (⇑c.toSetoid : M → M → Prop) y, val_inv := h₁,
        inv_val := h₂ }
⊢ p u

Tactic:
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1),
    p { val := (↑x : c.Quotient), inv := (↑y : c.Quotient), val_inv := ⋯, inv_val := ⋯ }
val inv : c.Quotient
x y : M
h₁ : HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) = 1
h₂ : HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) = 1
⊢ p
    { val := Quot.mk (⇑c.toSetoid : M → M → Prop) x, inv := Quot.mk (⇑c.toSetoid : M → M → Prop) y, val_inv := h₁,
      inv_val := h₂ }

Tactic:
H x y (c.eq.1 h₁) (c.eq.1 h₂)

Premises used: Con.eq, Iff.mp, Con.toQuotient
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H :
  ∀ (x y : M) (hxy : (c : (a : M) → M → Prop) (x * y) 1) (hyx : (c : (a : M) → M → Prop) (y * x) 1),
    p { val := (↑x : c.Quotient), inv := (↑y : c.Quotient), val_inv := ⋯, inv_val := ⋯ }
val inv : c.Quotient
x y : M
h₁ : HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) = 1
h₂ : HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) = 1
⊢ p
    { val := Quot.mk (⇑c.toSetoid : M → M → Prop) x, inv := Quot.mk (⇑c.toSetoid : M → M → Prop) y, val_inv := h₁,
      inv_val := h₂ }

Tactic:
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)

Premises used: Con.eq, Iff.mp
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
w x y z : M
h1 : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) w : N) ((f : (a : M) → N) x : N)
h2 : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) y : N) ((f : (a : M) → N) z : N)
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) w : N) ((f : (a : M) → N) y : N) = (f : (a : M) → N) (x * z)
rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) = (f : (a : M) → N) (x * z)
rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) z : N) = (f : (a : M) → N) (x * z)
rw₃ rw₄ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) z : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) z : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (w * y) : N) ((f : (a : M) → N) (x * z) : N)

Tactic:
rw [map_mul, h1, h2, map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
⊢ Eq (α := Con M) (ker (F := M →ₙ* N) (↑f : M →ₙ* N)) (ker f)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, Con.ker, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
x y : M
⊢ (ker f : (a : M) → M → Prop) x y ↔ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ ker c.mkMulHom = c

Tactic:
ext fun _ _ => Quotient.eq''

Premises used: Quotient.eq'', Con.ext
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
w x y z : N
h₁ : (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) w x
h₂ : (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) y z
rcases :
  ∀ (a b : M) (h1 : (c.toSetoid : M → M → Prop) a b),
    (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) (HMul.hMul (α := N) ((f : (a : M) → N) a : N) y)
      (HMul.hMul (α := N) ((f : (a : M) → N) b : N) z)
⊢ (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) (w * y) (x * z)

Tactic:
rcases h₁ with ⟨a, b, h1, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y z : N
h₂ : (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) y z
a b : M
h1 : (c.toSetoid : M → M → Prop) a b
rcases :
  ∀ (p q : M) (h2 : (c.toSetoid : M → M → Prop) p q),
    (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) p : N))
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) q : N))
⊢ (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) (HMul.hMul (α := N) ((f : (a : M) → N) a : N) y)
    (HMul.hMul (α := N) ((f : (a : M) → N) b : N) z)

Tactic:
rcases h₂ with ⟨p, q, h2, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
h1 : (c.toSetoid : M → M → Prop) a b
p q : M
h2 : (c.toSetoid : M → M → Prop) p q
⊢ (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop)
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) p : N))
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) q : N))

Tactic:
⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

Premises used: Con.mul, HMul.hMul, map_mul, And.intro, Exists.intro, Relation.Map
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
h1 : (c.toSetoid : M → M → Prop) a b
p q : M
h2 : (c.toSetoid : M → M → Prop) p q
⊢ (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop)
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) p : N))
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) b : N) ((f : (a : M) → N) q : N))

Tactic:
exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw :
  Eq (α := Con N) (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N))
    (conGen (⇑(mapOfSurjective f h hf) : (a : N) → N → Prop))
⊢ mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) = mapOfSurjective f h hf

Tactic:
rw [← conGen_of_con (c.mapOfSurjective f h hf)]

Premises used: Con.conGen_of_con, Con.mapOfSurjective
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
F : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Eq (α := Con N) (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N))
    (conGen (⇑(mapOfSurjective f h hf) : (a : N) → N → Prop))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : { d : Con M // c ≤ d }
rw : c ≤ (↑d : Con M)
⊢ ker c.mkMulHom ≤ (↑d : Con M)

Tactic:
rw [Con.ker_mkMulHom_eq]

Premises used: Con.ker_mkMulHom_eq
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : { d : Con M // c ≤ d }
⊢ c ≤ (↑d : Con M)

Tactic:
d.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : { d : Con M // c ≤ d }
⊢ c ≤ (↑d : Con M)

Tactic:
exact d.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : (c : (a : M) → M → Prop) x y
rw : (d : (a : c.Quotient) → c.Quotient → Prop) (↑y : c.Quotient) (↑y : c.Quotient)
⊢ (d : (a : c.Quotient) → c.Quotient → Prop) (↑x : c.Quotient) (↑y : c.Quotient)

Tactic:
rw [c.eq.2 h]

Premises used: Iff.mpr, Con.eq
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : (c : (a : M) → M → Prop) x y
⊢ (d : (a : c.Quotient) → c.Quotient → Prop) (↑y : c.Quotient) (↑y : c.Quotient)

Tactic:
d.refl _

Premises used: Con.refl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : (c : (a : M) → M → Prop) x y
⊢ (d : (a : c.Quotient) → c.Quotient → Prop) (↑y : c.Quotient) (↑y : c.Quotient)

Tactic:
exact d.refl _

Premises used: Con.refl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : c.Quotient
⊢ ((fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯)
          ((fun (d : Con c.Quotient) ↦
              (Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯ : { d : Con M // c ≤ d }))
            d) :
        (a : c.Quotient) → c.Quotient → Prop)
      x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) x y

Tactic:
⟨?_, Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩

Premises used: Con.induction_on₂, Iff.intro
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : c.Quotient
refine :
  ((fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯)
          ((fun (d : Con c.Quotient) ↦
              (Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯ : { d : Con M // c ≤ d }))
            d) :
        (a : c.Quotient) → c.Quotient → Prop)
      x y →
    (d : (a : c.Quotient) → c.Quotient → Prop) x y
⊢ ((fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯)
          ((fun (d : Con c.Quotient) ↦
              (Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯ : { d : Con M // c ≤ d }))
            d) :
        (a : c.Quotient) → c.Quotient → Prop)
      x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) x y

Tactic:
refine ⟨?_, Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
a b : M
H : ((↑((fun (d : Con c.Quotient) ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d) : Con M).toSetoid : M → M → Prop) a b
⊢ (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) b)

Tactic:
H

Premises used: Con.toQuotient
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
d : Con c.Quotient
a b : M
H : ((↑((fun (d : Con c.Quotient) ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d) : Con M).toSetoid : M → M → Prop) a b
⊢ (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) b)

Tactic:
exact H
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
mp :
  LE.le (α := Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          s :
        Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          t :
        Con c.Quotient) →
    s ≤ t
mpr :
  s ≤ t →
    LE.le (α := Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          s :
        Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          t :
        Con c.Quotient)
⊢ LE.le (α := Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          s :
        Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          t :
        Con c.Quotient) ↔
    s ≤ t

Tactic:
constructor