awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
rw :
  Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₁ :
  Eq (α := (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₂ :
  Eq (α := (a : M) → M → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₃ :
  Eq (α := (a : M) → M → Prop) (iInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
have rw₄ : Eq.{u_1 + 1} (α := (a : M) → M → Prop) (⨅ (x : ι), (⇑(f x) : (a : M) → M → Prop))
  (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ c.toSetoid = ⊤ ↔ c = ⊤
have rw : c.toSetoid = toSetoid ⊤ ↔ c = ⊤
Tactic: rw [← toSetoid_top, toSetoid_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c : Con M
rw : c.toSetoid = toSetoid ⊤ ↔ c = ⊤
⊢ c.toSetoid = ⊤ ↔ c = ⊤
have rw₁ : c = ⊤ ↔ c = ⊤
Tactic: rw [← toSetoid_top, toSetoid_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ c.toSetoid = ⊥ ↔ c = ⊥
have rw : c.toSetoid = toSetoid ⊥ ↔ c = ⊥
Tactic: rw [← toSetoid_bot, toSetoid_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c : Con M
rw : c.toSetoid = toSetoid ⊥ ↔ c = ⊥
⊢ c.toSetoid = ⊥ ↔ c = ⊥
have rw₁ : c = ⊥ ↔ c = ⊥
Tactic: rw [← toSetoid_bot, toSetoid_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ (s : (a : M) → M → Prop) x y
have of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
Tactic: apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
⊢ (s : (a : M) → M → Prop) x y
have refl : ∀ (x : M), (s : (a : M) → M → Prop) x x
Tactic: apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
refl : ∀ (x : M), (s : (a : M) → M → Prop) x x
⊢ (s : (a : M) → M → Prop) x y
have symm : ∀ {x y : M}, ConGen.Rel r x y → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y x
Tactic: apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
refl : ∀ (x : M), (s : (a : M) → M → Prop) x x
symm : ∀ {x y : M}, ConGen.Rel r x y → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y x
⊢ (s : (a : M) → M → Prop) x y
have trans : ∀ {x y z : M},
  ConGen.Rel r x y →
    ConGen.Rel r y z → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) x z
Tactic: apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
refl : ∀ (x : M), (s : (a : M) → M → Prop) x x
symm : ∀ {x y : M}, ConGen.Rel r x y → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y x
trans :
  ∀ {x y z : M},
    ConGen.Rel r x y →
      ConGen.Rel r y z → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) x z
⊢ (s : (a : M) → M → Prop) x y
have mul : ∀ {w x y z : M},
  ConGen.Rel r w x →
    ConGen.Rel r y z →
      (s : (a : M) → M → Prop) w x → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) (w * y) (x * z)
Tactic: apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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
⊢ conGen r ≤ c
have rw : sInf {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} ≤ c
Tactic: rw [conGen_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ conGen (⇑c : (a : M) → M → Prop) ≤ c
have rw : sInf {s : Con M | ∀ (x y : M), (c : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) x y} ≤ c
Tactic: rw [conGen_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ c ⊔ d = conGen fun (x y : M) ↦ (c : (a : M) → M → Prop) x y ∨ (d : (a : M) → M → Prop) x y
have 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}
Tactic: rw [conGen_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ 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}
have 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}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ c ⊔ d = conGen ((⇑c : (a : M) → M → Prop) ⊔ (⇑d : (a : M) → M → Prop))
have 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)))
Tactic: rw [sup_eq_conGen]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ sSup S = conGen fun (x y : M) ↦ ∃ c ∈ S, (c : (a : M) → M → Prop) x y
have 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}
Tactic: rw [conGen_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ 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}
have 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}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ upperBounds S = {s : Con M | ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) → (s : (a : M) → M → Prop) x y}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ sSup S = conGen (sSup (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S))
have 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)))
Tactic: rw [sSup_eq_conGen, sSup_image]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ 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)))
have e_r : ∀ (x y : M), (∃ c ∈ S, (c : (a : M) → M → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : M) → M → Prop)) x y
Tactic: congr with (x y)
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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 * y)) (f (x * z))
have rw : (c : (a : N) → N → Prop) (f w * f y) (f x * f z)
Tactic: rw [H, H]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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
⊢ (c : (a : M) → M → Prop) (f x) (f y)
have 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)
Tactic: simp only [← Con.eq, coe_one, coe_mul] at *
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (hypothesis)
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)
⊢ Eq (α := c.Quotient) (↑(f x) : c.Quotient) (↑(f y) : c.Quotient)
have hf' : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (hypothesis)
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
⊢ Eq (α := c.Quotient) (↑(f x) : c.Quotient) (↑(f y) : c.Quotient)
have this : { val := (↑x : c.Quotient), inv := (↑(f x) : c.Quotient), val_inv := sorry, inv_val := sorry : c.Quotientˣ } =
  { val := (↑y : c.Quotient), inv := (↑(f y) : c.Quotient), val_inv := sorry, inv_val := sorry }
Tactic: have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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'
⊢ α
have 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 sorry sorry)
      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 sorry sorry)
      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
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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')
have refine_1 : (HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1) =
  (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
Tactic: refine Function.hfunext ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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)
⊢ 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')
have 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 sorry sorry)
        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 sorry sorry)
        x' y' a')
Tactic: refine Function.hfunext ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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'
⊢ (HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
have refine_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]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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)
⊢ (HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑x' : c.Quotient) (↑y' : c.Quotient) = 1)
have refine_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]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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')
have refine_2 : (HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) =
  (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)
Tactic: refine Function.hfunext ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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)
⊢ 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')
have 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 sorry sorry)
        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 sorry sorry)
        x' y' Hxy' a')
Tactic: refine Function.hfunext ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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
⊢ (HMul.hMul (α := c.Quotient) (↑y : c.Quotient) (↑x : c.Quotient) = 1) =
    (HMul.hMul (α := c.Quotient) (↑y' : c.Quotient) (↑x' : c.Quotient) = 1)
have refine_2 : (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]