awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
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 := ⋯ }
⊢ p u
have 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₂ }
Tactic: rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (w * y) : N) ((f : (a : M) → N) (x * z) : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) w : N) ((f : (a : M) → N) y : N) = (f : (a : M) → N) (x * z)
Tactic: rw [map_mul, h1, h2, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (w * y) : N) ((f : (a : M) → N) (x * z) : N)
have rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) = (f : (a : M) → N) (x * z)
Tactic: rw [map_mul, h1, h2, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (w * y) : N) ((f : (a : M) → N) (x * z) : N)
have rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) z : N) = (f : (a : M) → N) (x * z)
Tactic: rw [map_mul, h1, h2, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (w * y) : N) ((f : (a : M) → N) (x * z) : N)
have 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)
Tactic: rw [map_mul, h1, h2, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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
⊢ (c.mapOfSurjective (⇑f : (a : M) → N) h hf : N → N → Prop) (w * y) (x * z)
have 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)
Tactic: rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
Cleared hypotheses: w, x, h₁
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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
⊢ (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)
have 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))
Tactic: rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
Cleared hypotheses: y, z, h₂
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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)
⊢ mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) = mapOfSurjective f h hf
have 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))
Tactic: rw [← conGen_of_con (c.mapOfSurjective f h hf)]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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 }
⊢ ker c.mkMulHom ≤ (↑d : Con M)
have rw : c ≤ (↑d : Con M)
Tactic: rw [Con.ker_mkMulHom_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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) (↑x : c.Quotient) (↑y : c.Quotient)
have rw : (d : (a : c.Quotient) → c.Quotient → Prop) (↑y : c.Quotient) (↑y : c.Quotient)
Tactic: rw [c.eq.2 h]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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
have refine : ((fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom sorry sorry)
        ((fun (d : Con c.Quotient) ↦
            (Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient sorry d) sorry : { 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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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 }
⊢ 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
have mp : LE.le (α := Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom sorry sorry,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient sorry d) sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        s :
      Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom sorry sorry,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient sorry d) sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        t :
      Con c.Quotient) →
  s ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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
⊢ 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
have mpr : s ≤ t →
  LE.le (α := Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom sorry sorry,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient sorry d) sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        s :
      Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom sorry sorry,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient sorry d) sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        t :
      Con c.Quotient)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
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 }
h :
  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)
x y : M
hs : ((↑s : Con M) : (a : M) → M → Prop) x y
⊢ ((↑t : Con M) : (a : M) → M → Prop) x y
have mp : ∀ (a b : M) (ht : ((↑t : Con M).toSetoid : M → M → Prop) a b)
  (hx :
    Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
      ((c.mkMulHom : (a : M) → c.Quotient) x : c.Quotient))
  (hy :
    Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) b : c.Quotient)
      ((c.mkMulHom : (a : M) → c.Quotient) y : c.Quotient)),
  ((↑t : Con M) : (a : M) → M → Prop) x y
Tactic: rcases h ⟨x, y, hs, rfl, rfl⟩ with ⟨a, b, ht, hx, hy⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ (c : (a : M) → M → Prop) ((f : (a : N) → M) x : M) ((f : (a : N) → M) y) ↔
    Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) x) : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) y) : c.Quotient)
have rw : Eq.{u_1 + 1} (α := c.Quotient) ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)
    ((↑((f : (a : N) → M) y) : c.Quotient) : c.Quotient) ↔
  Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) x) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) y) : c.Quotient)
Tactic: rw [← c.eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (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 y : M
f : M →* P
H : c ≤ ker f
⊢ Eq.{u_3 + 1} (α := P) (Con.liftOn (c := c) 1 (⇑f : (a : M) → P) ⋯) 1
have rw : Eq.{u_3 + 1} (α := P) (Con.liftOn (c := c) 1 (⇑f : (a : M) → P) sorry : P) ((f : (a : M) → P) 1 : P)
Tactic: rw [← f.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (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 : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ Con.liftOn (HMul.hMul (α := c.Quotient) (↑m : c.Quotient) (↑n : c.Quotient)) (⇑f : (a : M) → P) ⋯ =
    HMul.hMul (α := P) (Con.liftOn (c := c) (↑m : c.Quotient) (⇑f : (a : M) → P) ⋯)
      (Con.liftOn (c := c) (↑n : c.Quotient) (⇑f : (a : M) → P) ⋯)
have dsimp : (f : (a : M) → P) (m * n) = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)
Tactic: dsimp only [← coe_mul, Con.liftOn_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (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 : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ (f : (a : M) → P) (m * n) = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)
have rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P) =
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f
have h : ∀ (x : M), Eq.{u_3 + 1} (α := P) (((c.lift f H).comp c.mk' : (a : M) → P) x : P) ((f : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (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 : M →* P
f : MonoidHom.{u_1, u_3} c.Quotient P
x y : M
h : (c : (a : M) → M → Prop) x y
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑x : c.Quotient) : P)
    ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
have rw : Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
  ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
Tactic: rw [c.eq.2 h]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : MonoidHom.{u_1, u_3} c.Quotient P
⊢ c.lift (f.comp c.mk') ⋯ = f
have h : ∀ (x : c.Quotient),
  Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') sorry : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : MonoidHom.{u_1, u_3} c.Quotient P
x : c.Quotient
⊢ Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)
have h : ∀ (a : M),
  Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') sorry : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
    ((f : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
Tactic: rcases x with ⟨⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Hom (goal)
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f g : MonoidHom.{u_1, u_3} c.Quotient P
h : f.comp c.mk' = g.comp c.mk'
⊢ f = g
have rw : c.lift (f.comp c.mk') sorry = c.lift (g.comp c.mk') sorry
Tactic: rw [← lift_apply_mk' f, ← lift_apply_mk' g]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Opposite (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
have mp : (∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y) →
  ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Opposite (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
mp :
  (∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y) →
    ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
⊢ (∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
have mpr : (∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y) →
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
m : M ∗ N
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
⊢ C m
have rcases : ∀ (x : FreeMonoid (M ⊕ N)), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x)
Tactic: rcases mk_surjective m with ⟨x, rfl⟩
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
x : M ⊕ N
xs : FreeMonoid (M ⊕ N)
ih : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) xs)
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of x * xs))
have mul_of : ∀ (m : M), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inl m) * xs))
Tactic: cases x with
    | inl m => simpa using inl_mul m _ ih
    | inr n => simpa using inr_mul n _ ih
Cleared hypotheses: x