awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → (c : (a : M) → M → Prop) x y
⊢ sInf {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} ≤ c

Tactic:
exact sInf_le h
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r s : M → M → Prop
h : ∀ (x y : M), r x y → s x y
⊢ LE.le (α := Con M) (conGen r) (conGen s)

Tactic:
conGen_le fun x y hr => ConGen.Rel.of _ _ <| h x y hr

Premises used: Con.conGen_le, ConGen.Rel.of
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
rw : sInf {s : Con M | ∀ (x y : M), (c : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y} ≤ c
⊢ conGen (⇑c : (a : M) → M → Prop) ≤ c

Tactic:
rw [conGen_eq]

Premises used: Con.conGen_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ sInf {s : Con M | ∀ (x y : M), (c : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y} ≤ c

Tactic:
sInf_le fun _ _ => id

Premises used: id, sInf_le
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ sInf {s : Con M | ∀ (x y : M), (c : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y} ≤ c

Tactic:
exact sInf_le fun _ _ => id
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
⊢ Eq (α := Con M) (conGen (⇑(conGen r) : (a : M) → M → Prop)) (conGen r)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
rw :
  c ⊔ d =
    sInf
      {s : Con M |
        ∀ (x y : M), (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y}
⊢ c ⊔ d = conGen fun (x y : M) ↦ (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y

Tactic:
rw [conGen_eq]

Premises used: Con.conGen_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
apply :
  Eq.{u_1 + 1} (α := Set (Con M)) {x : Con M | c ≤ x ∧ d ≤ x}
    {s : Con M |
      ∀ (x y : M), (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y}
⊢ c ⊔ d =
    sInf
      {s : Con M |
        ∀ (x y : M), (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ Eq.{u_1 + 1} (α := Set (Con M)) {x : Con M | c ≤ x ∧ d ≤ x}
    {s : Con M |
      ∀ (x y : M), (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Premises used: or_imp, Con.le_def, forall_and
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
rw :
  Eq (α := Con M) (conGen fun (x y : M) ↦ (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y)
    (conGen ((⇑c : (a : M) → M → Prop) ⊔ (⇑d : (a : M) → M → Prop)))
⊢ c ⊔ d = conGen ((⇑c : (a : M) → M → Prop) ⊔ (⇑d : (a : M) → M → Prop))

Tactic:
rw [sup_eq_conGen]

Premises used: Con.sup_eq_conGen
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ Eq (α := Con M) (conGen fun (x y : M) ↦ (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y)
    (conGen ((⇑c : (a : M) → M → Prop) ⊔ (⇑d : (a : M) → M → Prop)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
rw : sSup S = sInf {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y}
⊢ sSup S = conGen fun (x y : M) ↦ ∃ c ∈ S, (c : (a : M) → M → Prop) x y

Tactic:
rw [conGen_eq]

Premises used: Con.conGen_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
apply :
  upperBounds S = {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y}
⊢ sSup S = sInf {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
h :
  ∀ (x : Con M),
    x ∈ upperBounds S ↔
      Membership.mem (γ := Set (Con M))
        {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y} x
⊢ upperBounds S = {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y}

Tactic:
ext
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x : Con M
⊢ x ∈ upperBounds S ↔
    Membership.mem (γ := Set (Con M))
      {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y} x

Tactic:
⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩

Premises used: _private.0.Con.sSup_eq_conGen.match_1, And.right, And.left, And.intro, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x : Con M
⊢ x ∈ upperBounds S ↔
    Membership.mem (γ := Set (Con M))
      {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y} x

Tactic:
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
rw :
  Eq.{u_1 + 1} (α := Con M) (conGen fun (x y : M) ↦ ∃ c ∈ S, (c : (a : M) → M → Prop) x y)
    (conGen (⨆ a ∈ S, (⇑a : (a : M) → M → Prop)))
⊢ sSup S = conGen (sSup (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S))

Tactic:
rw [sSup_eq_conGen, sSup_image]

Premises used: Con.sSup_eq_conGen, sSup_image
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
e_r : ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : M) → M → Prop)) x y
⊢ Eq.{u_1 + 1} (α := Con M) (conGen fun (x y : M) ↦ ∃ c ∈ S, (c : (a : M) → M → Prop) x y)
    (conGen (⨆ a ∈ S, (⇑a : (a : M) → M → Prop)))

Tactic:
congr with (x y)
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x y : M
⊢ (∃ c ∈ S, (c : (a : M) → M → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : M) → M → Prop)) x y

Tactic:
simp only [iSup_apply, iSup_Prop_eq, exists_prop]

Premises used: exists_prop, iSup_Prop_eq, iSup_apply
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid : M → M → Prop) w x
h2 : (Setoid.comap f c.toSetoid : M → M → Prop) y z
rw : (c : (a : N) → N → Prop) (f w * f y) (f x * f z)
⊢ (c : (a : N) → N → Prop) (f (w * y)) (f (x * z))

Tactic:
rw [H, H]
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid : M → M → Prop) w x
h2 : (Setoid.comap f c.toSetoid : M → M → Prop) y z
⊢ (c : (a : N) → N → Prop) (f w * f y) (f x * f z)

Tactic:
c.mul h1 h2

Premises used: Con.mul
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c_1 d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid : M → M → Prop) w x
h2 : (Setoid.comap f c.toSetoid : M → M → Prop) y z
⊢ (c : (a : N) → N → Prop) (f w * f y) (f x * f z)

Tactic:
exact c.mul h1 h2

Premises used: Con.mul
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
x y : M
⊢ (comap f H c : (a : M) → M → Prop) x y ↔ (c : (a : N) → N → Prop) (f x) (f y)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
inst_1 : One M
c : Con M
⊢ Eq.{u_1 + 1} (α := c.Quotient) (↑1 : c.Quotient) 1

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_4
inst : Monoid M
c : Con M
w x : M
h : (c : (a : M) → M → Prop) w x
⊢ (c : (a : M) → M → Prop) (HPow.hPow (β := ℕ) w 0) (HPow.hPow (β := ℕ) x 0)

Tactic:
simpa using c.refl _

Premises used: Con.refl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_4
inst : Monoid M
c : Con M
n : ℕ
w x : M
h : (c : (a : M) → M → Prop) w x
⊢ (c : (a : M) → M → Prop) (w ^ n.succ) (x ^ n.succ)

Tactic:
simpa [pow_succ] using c.mul (Con.pow c n h) h

Premises used: Con.mul, pow_succ
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
hf : ∀ (x : M), (c : (a : M) → M → Prop) (f x * x) 1
x y : M
h : (c : (a : M) → M → Prop) x y
simp :
  ∀ (hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1)
    (h : Eq (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)),
    Eq (α := c.Quotient) (↑(f x) : c.Quotient) (↑(f y) : c.Quotient)
⊢ (c : (a : M) → M → Prop) (f x) (f y)

Tactic:
simp only [← Con.eq, coe_one, coe_mul] at *

Premises used: Con.eq, Con.coe_one, Con.coe_mul
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x_1 y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x_1 : c.Quotient) (↑y : c.Quotient)
x : M
⊢ HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) =
    HMul.hMul (α := c.Quotient) (↑(f (f x)) : c.Quotient) (↑(f x) : c.Quotient) *
      HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient)

Tactic:
simp [hf]
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x_1 y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x_1 : c.Quotient) (↑y : c.Quotient)
x : M
⊢ HMul.hMul (α := c.Quotient) (↑(f (f x)) : c.Quotient) (↑(f x) : c.Quotient) *
      HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) =
    (↑(f (f x)) : c.Quotient) * HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) *
      (↑(f x) : c.Quotient)

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x_1 y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x_1 : c.Quotient) (↑y : c.Quotient)
x : M
⊢ (↑(f (f x)) : c.Quotient) * HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) *
      (↑(f x) : c.Quotient) =
    1

Tactic:
simp [hf]
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)
⊢ ∀ (x : M), HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) = 1

Tactic:
have hf' : ∀ x : M, (x : c.Quotient) * f x = 1 := fun x ↦
    calc
      (x : c.Quotient) * f x = f (f x) * f x * (x * f x) := by simp [hf]
      _ = f (f x) * (f x * x) * f x := by simp_rw [mul_assoc]
      _ = 1 := by simp [hf]
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)
hf' : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) = 1
⊢ { val := (↑x : c.Quotient), inv := (↑(f x) : c.Quotient), val_inv := ⋯, inv_val := ⋯ : c.Quotientˣ } =
    { val := (↑y : c.Quotient), inv := (↑(f y) : c.Quotient), val_inv := ⋯, inv_val := ⋯ }

Tactic:
have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)
hf' : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) = 1
this :
  { val := (↑x : c.Quotient), inv := (↑(f x) : c.Quotient), val_inv := ⋯, inv_val := ⋯ : c.Quotientˣ } =
    { val := (↑y : c.Quotient), inv := (↑(f y) : c.Quotient), val_inv := ⋯, inv_val := ⋯ }
⊢ Eq (α := c.Quotient) (↑(f x) : c.Quotient) (↑(f y) : c.Quotient)

Tactic:
congr_arg Units.inv this

Premises used: congr_arg, Con.toQuotient, Units.inv
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑(f x) : c.Quotient) (↑x : c.Quotient) = 1
h : Eq (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)
hf' : ∀ (x : M), HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑(f x) : c.Quotient) = 1
this :
  { val := (↑x : c.Quotient), inv := (↑(f x) : c.Quotient), val_inv := ⋯, inv_val := ⋯ : c.Quotientˣ } =
    { val := (↑y : c.Quotient), inv := (↑(f y) : c.Quotient), val_inv := ⋯, inv_val := ⋯ }
⊢ Eq (α := c.Quotient) (↑(f x) : c.Quotient) (↑(f y) : c.Quotient)

Tactic:
exact congr_arg Units.inv this

Premises used: congr_arg, Units.inv
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Group M
c : Con M
x_1 y : M
h : (c : (a : M) → M → Prop) x_1 y
x : M
⊢ (c : (a : M) → M → Prop) (x⁻¹ * x) 1

Tactic:
simp only [inv_mul_cancel, c.refl 1]

Premises used: inv_mul_cancel, Con.refl, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Group M
c : Con M
w x y z : M
h1 : (c : (a : M) → M → Prop) w x
h2 : (c : (a : M) → M → Prop) y z
⊢ (c : (a : M) → M → Prop) (w / y) (x / z)

Tactic:
simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)

Premises used: Con.mul, Con.inv, div_eq_mul_inv
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Group M
c : Con M
n : ℕ
w x : M
h : (c : (a : M) → M → Prop) w x
⊢ (c : (a : M) → M → Prop) (w ^ Int.ofNat n) (x ^ Int.ofNat n)

Tactic:
simpa only [zpow_natCast, Int.ofNat_eq_natCast] using c.pow n h

Premises used: zpow_natCast, Int.ofNat_eq_natCast, Con.pow
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Group M
c : Con M
n : ℕ
w x : M
h : (c : (a : M) → M → Prop) w x
⊢ (c : (a : M) → M → Prop) (w ^ Int.negSucc n) (x ^ Int.negSucc n)

Tactic:
simpa only [zpow_negSucc] using c.inv (c.pow _ h)

Premises used: Con.inv, zpow_negSucc, Con.pow
-- 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'
fun :
  ∀ (x y x' y' : M) (hx : (c : (a : M) → M → Prop) x x') (hy : (c : (a : M) → M → Prop) y y'),
    HEq.{u_4 + 1} (α := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x : c.Quotient) (↑y : c.Quotient))
      ((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)
      (β := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x' : c.Quotient) (↑y' : c.Quotient))
      ((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')
⊢ α

Tactic:
refine
    Con.hrecOn₂ (cN := c) (φ := fun x y => x * y = 1 → y * x = 1 → α) (u : c.Quotient)
      (↑u⁻¹ : c.Quotient)
      (fun (x y : M) (hxy : (x * y : c.Quotient) = 1) (hyx : (y * x : c.Quotient) = 1) =>
        f x y (c.eq.1 hxy) (c.eq.1 hyx))
      (fun x y x' y' hx hy => ?_) u.3 u.4

Premises used: Units.val, Units.inv_val, Con.eq, Con.hrecOn₂, Inv.inv, Iff.mp, Units.val_inv
-- 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'
⊢ HEq.{u_4 + 1} (α := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x : c.Quotient) (↑y : c.Quotient))
    ((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)
    (β := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x' : c.Quotient) (↑y' : c.Quotient))
    ((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')

Tactic:
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'
refine_1 :
  (HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
refine_2 :
  ∀ (a : HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1)
    (a' : HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1),
    a ≍ 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 a)
        (β := (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' a')
⊢ HEq.{u_4 + 1} (α := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x : c.Quotient) (↑y : c.Quotient))
    ((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)
    (β := (fun (x y : c.Quotient) ↦ x * y = 1 → y * x = 1 → α) (↑x' : c.Quotient) (↑y' : c.Quotient))
    ((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')

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'
refine_1 :
  (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
refine_1₁ refine_1₂ :
  (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
⊢ (HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : 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
⊢ 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:
Function.hfunext ?_ ?_

Premises used: Function.hfunext