awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
rwa :
  ∀ (h1 : (↑(h * h') : G) = (↑1 : G)),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
⊢ (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
have rwa₁ : ∀ (h1 : (↑(h * h') : G) = 1),
  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
Tactic: rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
rwa :
  ∀ (h1 : (↑(h * h') : G) = (↑1 : G)),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
rwa₁ :
  ∀ (h1 : (↑(h * h') : G) = 1),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
⊢ (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
have rwa₂ : ∀ (h1 : (↑h : G) * (↑h' : G) = 1),
  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
Tactic: rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (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 c d : Con M
h : c = d
x y : c.Quotient
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x * (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) sorry).toFun y
Tactic: rcases x with ⟨⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (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 c d : Con M
h : c = d
x y : c.Quotient
a : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun y
have mk : ∀ (a_1 : M),
  (Quotient.congr (Equiv.refl M) sorry).toFun
      (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) sorry).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
Tactic: rcases y with ⟨⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
rel : N → N → Prop
⊢ Eq (α := Con M) (comap (⇑f : (a : M) → N) ⋯ (conGen rel))
    (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y))
have apply : LE.le (α := Con M) (comap (⇑f : (a : M) → N) sorry (conGen rel))
  (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y))
Tactic: apply le_antisymm _ (le_comap_conGen f (map_mul f) rel)
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (hypothesis)
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 fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a_1 b_1
have of : rel ((f : (a : M) → N) a_1) ((f : (a : M) → N) b_1)
Tactic: apply ConGen.Rel.of
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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
⊢ rel ((f : (a : M) → N) a_1) ((f : (a : M) → N) b_1)
have of : rel x ((f : (a : M) → N) b_1)
Tactic: rwa [fa, fb]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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) a_1 b_1
have 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
Tactic: rw [f.injective (fc.trans fd.symm)]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (hypothesis)
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
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
have fa₁ : 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
Cleared hypotheses: fa, fb
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (hypothesis)
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)
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
have fb₁ : 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
Cleared hypotheses: fa, fb
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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) a b
have 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))
Tactic: rw [fa, fb]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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 : N
h : (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
have of : ∀ (x y : N) (h : rel x y) (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
Tactic: induction h with
    | of x y h =>
      intro _ _ fa fb
      apply ConGen.Rel.of
      rwa [fa, fb]
    | refl x =>
      intro _ _ fc fd
      rw [f.injective (fc.trans fd.symm)]
      exact ConGen.Rel.refl _
    | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
    | trans _ _ ih ih1 =>
      exact fun a b fa fb ↦ Exists.casesOn (f.surjective _) fun c' hc' ↦
      ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
    | mul _ _ ih ih1 =>
      rename_i w x y z _ _
      intro a b fa fb
      rw [← f.eq_symm_apply, map_mul] at fa fb
      rw [fa, fb]
      exact ConGen.Rel.mul (ih (f.symm w) (f.symm x) (by simp) (by simp))
        (ih1 (f.symm y) (f.symm z) (by simp) (by simp))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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 : N
h : (conGen rel : (a : N) → N → Prop) n1 n2
of :
  ∀ (x y : N) (h : rel x y) (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 = 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
have refl : ∀ (x : N) (a b : M),
  (f : (a : M) → N) a = 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 b
Tactic: induction h with
    | of x y h =>
      intro _ _ fa fb
      apply ConGen.Rel.of
      rwa [fa, fb]
    | refl x =>
      intro _ _ fc fd
      rw [f.injective (fc.trans fd.symm)]
      exact ConGen.Rel.refl _
    | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
    | trans _ _ ih ih1 =>
      exact fun a b fa fb ↦ Exists.casesOn (f.surjective _) fun c' hc' ↦
      ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
    | mul _ _ ih ih1 =>
      rename_i w x y z _ _
      intro a b fa fb
      rw [← f.eq_symm_apply, map_mul] at fa fb
      rw [fa, fb]
      exact ConGen.Rel.mul (ih (f.symm w) (f.symm x) (by simp) (by simp))
        (ih1 (f.symm y) (f.symm z) (by simp) (by simp))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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 : N
h : (conGen rel : (a : N) → N → Prop) n1 n2
of :
  ∀ (x y : N) (h : rel x y) (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
refl :
  ∀ (x : N) (a b : M),
    (f : (a : M) → N) a = 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 b
⊢ ∀ (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
have symm : ∀ {x y : N},
  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: 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))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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 : N
h : (conGen rel : (a : N) → N → Prop) n1 n2
of :
  ∀ (x y : N) (h : rel x y) (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
refl :
  ∀ (x : N) (a b : M),
    (f : (a : M) → N) a = 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 b
symm :
  ∀ {x y : N},
    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
⊢ ∀ (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
have trans : ∀ {x y z : N},
  ConGen.Rel rel x y →
    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: 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))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (hypothesis)
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)
⊢ (conGen fun (x y : M) ↦ rel ((f : (a : M) → N) x) ((f : (a : M) → N) y) : (a : M) → M → Prop) a b
have 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
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))
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
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)))
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) x : P)
    ((kerLift f : (a : (ker f).Quotient) → P) y : P)
have 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)
Tactic: rcases x with ⟨⟩
Cleared hypotheses: h