awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
one : HMul.hMul (α := CoprodI G) (MulOpposite.unop 1) 1 = 1
⊢ HMul.hMul (α := CoprodI G)
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          1))
      1 =
    1
have one₁ : HMul.hMul (α := CoprodI G) 1 1 = 1
Tactic: rw [map_one, MulOpposite.unop_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
one : HMul.hMul (α := CoprodI G) (MulOpposite.unop 1) 1 = 1
one₁ : HMul.hMul (α := CoprodI G) 1 1 = 1
⊢ HMul.hMul (α := CoprodI G)
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          1))
      1 =
    1
have one₂ : Eq (α := CoprodI G) 1 1
Tactic: rw [map_one, MulOpposite.unop_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : ι
ih : G m
⊢ HMul.hMul (α := CoprodI G) (β := CoprodI G)
      (MulOpposite.unop
          (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                  ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                    (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                  (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
              (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
            ((of (M := G) : (a : G m) → CoprodI G) ih)) :
        CoprodI G)
      ((of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1
have of : HMul.hMul (α := CoprodI G) (β := CoprodI G)
    ((of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ :
      CoprodI G)
    ((of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
  1
Tactic: change of _⁻¹ * of _ = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : ι
ih : G m
⊢ HMul.hMul (α := CoprodI G) (β := CoprodI G)
      ((of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ :
        CoprodI G)
      ((of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1
have of : Eq (α := CoprodI G)
  ((of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
      (((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ * ih) :
    CoprodI G)
  (1 : CoprodI G)
Tactic: rw [← of.map_mul, inv_mul_cancel, of.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : ι
ih : G m
of :
  Eq (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
        (((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ * ih) :
      CoprodI G)
    (1 : CoprodI G)
⊢ HMul.hMul (α := CoprodI G) (β := CoprodI G)
      ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ :
        CoprodI G)
      ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1
have of₁ : Eq (α := CoprodI G) ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G) 1) 1
Tactic: rw [← of.map_mul, inv_mul_cancel, of.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : ι
ih : G m
of :
  Eq (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
        (((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ * ih) :
      CoprodI G)
    (1 : CoprodI G)
of₁ : Eq (α := CoprodI G) ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G) 1) 1
⊢ HMul.hMul (α := CoprodI G) (β := CoprodI G)
      ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ :
        CoprodI G)
      ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1
have of₂ : Eq (α := CoprodI G) 1 1
Tactic: rw [← of.map_mul, inv_mul_cancel, of.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
x y : CoprodI G
ihx :
  MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          x) *
      x =
    1
ihy :
  MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          y) *
      y =
    1
⊢ MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          (x * y)) *
      (x * y) =
    1
have mul : MulOpposite.unop
      (HMul.hMul (α := (CoprodI G)ᵐᵒᵖ) (β := (CoprodI G)ᵐᵒᵖ)
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                  ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                    (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                  (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
              (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
            x :
          (CoprodI G)ᵐᵒᵖ)
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                  ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                    (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                  (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
              (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
            y :
          (CoprodI G)ᵐᵒᵖ)) *
    (x * y) =
  1
Tactic: rw [map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul,
          ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : CoprodI G
⊢ MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          m) *
      m =
    1
have one : HMul.hMul (α := CoprodI G)
    (MulOpposite.unop
      (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
            MonoidHom.comp (N := (G i)ᵐᵒᵖ)
              ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
              (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
          (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
        1))
    1 =
  1
Tactic: induction m using CoprodI.induction_on with
      | one => rw [map_one, MulOpposite.unop_one, one_mul]
      | of m ih =>
        change of _⁻¹ * of _ = 1
        rw [← of.map_mul, inv_mul_cancel, of.map_one]
      | mul x y ihx ihy =>
        rw [map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul,
          ihy]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : CoprodI G
one :
  HMul.hMul (α := CoprodI G)
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          1))
      1 =
    1
⊢ MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          m) *
      m =
    1
have of : ∀ (m : ι) (ih : G m),
  HMul.hMul (α := CoprodI G) (β := CoprodI G)
      (MulOpposite.unop
          (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                  ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                    (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                  (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
              (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
            ((of (M := G) : (a : G m) → CoprodI G) ih)) :
        CoprodI G)
      ((of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1
Tactic: induction m using CoprodI.induction_on with
      | one => rw [map_one, MulOpposite.unop_one, one_mul]
      | of m ih =>
        change of _⁻¹ * of _ = 1
        rw [← of.map_mul, inv_mul_cancel, of.map_one]
      | mul x y ihx ihy =>
        rw [map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul,
          ihy]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
        ((of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
      N)
have of : Membership.mem (α := N) s ((f i : (a : G i) → N) x : N)
Tactic: simp only [lift_of]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
hy :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N)
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) (x * y) :
      N)
have mul : HMul.hMul (α := N) (β := N)
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N) ∈
  s
Tactic: simp only [map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x : CoprodI G
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
have one : Membership.mem (α := N) s
  ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)
Tactic: induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x : CoprodI G
one :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
have of : ∀ (i : ι) (x : G i),
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
        ((of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
      N)
Tactic: induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x : CoprodI G
one :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)
of :
  ∀ (i : ι) (x : G i),
    Membership.mem (α := N) s
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
        N)
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
have mul : ∀ (x y : CoprodI G)
  (hx :
    Membership.mem (α := N) s
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N))
  (hy :
    Membership.mem (α := N) s
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N)),
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) (x * y) :
      N)
Tactic: induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
⊢ Eq.{u_5 + 1} (α := Subgroup N)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
    (⨆ (i : ι), (f i).range)
have apply : LE.le.{u_5} (α := Subgroup N) (⨆ (i : ι), (f i).range)
  (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
Tactic: apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
⊢ LE.le.{u_5} (α := Subgroup N) (⨆ (i : ι), (f i).range)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
have apply : ∀ (i : ι),
  (f i).range ≤ MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f)
Tactic: apply iSup_le _
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
⊢ ∀ l ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i m :: w.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have simp : ∀ (l : (i : ι) × M i),
  l = Sigma.mk (β := fun (i : ι) ↦ M i) i m ∨ l ∈ w.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: simp only [List.mem_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw : prod (M := M)
    (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) sorry h) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_pos hm, hm, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₁ : p.tail (M := M).prod (M := M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_pos hm, hm, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  p.tail (M := M).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₂ : p.tail (M := M).prod (M := M) = (of (M := M) : (a : M i) → CoprodI M) 1 * p.tail (M := M).prod (M := M)
Tactic: rw [rcons, dif_pos hm, hm, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  p.tail (M := M).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ : p.tail (M := M).prod (M := M) = (of (M := M) : (a : M i) → CoprodI M) 1 * p.tail (M := M).prod (M := M)
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₃ : p.tail (M := M).prod (M := M) = 1 * p.tail (M := M).prod (M := M)
Tactic: rw [rcons, dif_pos hm, hm, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  p.tail (M := M).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ : p.tail (M := M).prod (M := M) = (of (M := M) : (a : M i) → CoprodI M) 1 * p.tail (M := M).prod (M := M)
rw₃ : p.tail (M := M).prod (M := M) = 1 * p.tail (M := M).prod (M := M)
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₄ : p.tail (M := M).prod (M := M) = p.tail (M := M).prod (M := M)
Tactic: rw [rcons, dif_pos hm, hm, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw : prod (M := M)
    (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) sorry h) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]