awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
h :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
⊢ w = Word.empty (M := H)
have by_contra : ∀ (hnotempty : ¬w = Word.empty (M := H)), False
Tactic: by_contra hnotempty
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
h :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
hnotempty : ¬w = Word.empty (M := H)
⊢ False
have obtain : ∀ (i j : ι) (w : NeWord H i j)
  (h :
    Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.toWord (M := H).prod (M := H)) :
        G)
      (1 : G))
  (hnotempty : ¬w.toWord (M := H) = Word.empty (M := H)), False
Tactic: obtain ⟨i, j, w, rfl⟩ := NeWord.of_word w hnotempty
Cleared hypotheses: w, h, hnotempty
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
⊢ Function.Injective (α := CoprodI H) (β := G)
    (⇑((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
have apply : ∀ (a : CoprodI H),
  Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G) a : G)
      (1 : G) →
    a = 1
Tactic: apply (injective_iff_map_eq_one (lift f)).mpr
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
⊢ ∀ (a : CoprodI H),
    Eq.{u_4 + 1} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G) a : G)
        (1 : G) →
      a = 1
have rw : ∀ (b : Word H),
  Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) b : CoprodI H) :
        G)
      (1 : G) →
    Eq (α := CoprodI H) ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) b : CoprodI H) (1 : CoprodI H)
Tactic: rw [(CoprodI.Word.equiv).forall_congr_left]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
Heq :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) w : CoprodI H) :
      G)
    (1 : G)
⊢ Eq (α := CoprodI H) ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) w : CoprodI H) (1 : CoprodI H)
have dsimp : w.prod (M := H) = 1
Tactic: dsimp [Word.equiv] at *
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), ¬h = 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
Heq :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
⊢ w.prod (M := H) = 1
have rw : Eq (α := CoprodI H) (Word.prod (M := H) (Word.empty (M := H))) 1
Tactic: rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), ¬h = 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
w : Word H
Heq :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
rw : Eq (α := CoprodI H) (Word.prod (M := H) (Word.empty (M := H))) 1
⊢ w.prod (M := H) = 1
have rw₁ : Eq (α := CoprodI H) 1 1
Tactic: rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
⊢ Function.Injective (α := CoprodI H) (β := G)
    (⇑((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
have apply : ∀ (a : CoprodI H),
  Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G) a : G)
      (1 : G) →
    a = 1
Tactic: classical
    apply (injective_iff_map_eq_one (lift f)).mpr
    rw [(CoprodI.Word.equiv).forall_congr_left]
    intro w Heq
    dsimp [Word.equiv] at *
    rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
apply :
  ∀ (a : CoprodI H),
    Eq.{u_4 + 1} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G) a : G)
        (1 : G) →
      a = 1
⊢ Function.Injective (α := CoprodI H) (β := G)
    (⇑((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
have apply₁ : ∀ (b : Word H),
  Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) b : CoprodI H) :
        G)
      (1 : G) →
    Eq (α := CoprodI H) ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) b : CoprodI H) (1 : CoprodI H)
Tactic: classical
    apply (injective_iff_map_eq_one (lift f)).mpr
    rw [(CoprodI.Word.equiv).forall_congr_left]
    intro w Heq
    dsimp [Word.equiv] at *
    rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
apply :
  ∀ (a : CoprodI H),
    Eq.{u_4 + 1} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G) a : G)
        (1 : G) →
      a = 1
apply₁ apply₂ :
  ∀ (w : Word H)
    (Heq :
      Eq.{u_4 + 1} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) w : CoprodI H) :
          G)
        (1 : G)),
    Eq (α := CoprodI H) ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) w : CoprodI H) (1 : CoprodI H)
⊢ Function.Injective (α := CoprodI H) (β := G)
    (⇑((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
have apply₃ : ∀ (w : Word H)
  (Heq :
    Eq.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)),
  w.prod (M := H) = 1
Tactic: classical
    apply (injective_iff_map_eq_one (lift f)).mpr
    rw [(CoprodI.Word.equiv).forall_congr_left]
    intro w Heq
    dsimp [Word.equiv] at *
    rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst_2 : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis.{u_5, u_6} (X i) (G i)
⊢ Eq (α := FreeGroup ((i : ι) × X i) →* FreeGroup ((i : ι) × X i))
    (MonoidHom.comp (N := CoprodI G)
      ((lift (M := G) : (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
        fun (i : ι) ↦
        ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i)) fun (x : X i) ↦
          FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x))
      ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
        fun (x : (i : ι) × X i) ↦
        (of (M := G) : (a : G x.fst) → CoprodI G)
          ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i)))))
    (MonoidHom.id (FreeGroup ((i : ι) × X i)))
have h : ∀ (a : (i : ι) × X i),
  Eq (α := FreeGroup ((i : ι) × X i))
    ((MonoidHom.comp (N := CoprodI G)
            ((lift (M := G) : (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
              fun (i : ι) ↦
              ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i)) fun (x : X i) ↦
                FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x))
            ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
              fun (x : (i : ι) × X i) ↦
              (of (M := G) : (a : G x.fst) → CoprodI G)
                ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i)))) :
          (a : FreeGroup ((i : ι) × X i)) → FreeGroup ((i : ι) × X i))
        (FreeGroup.of a) :
      FreeGroup ((i : ι) × X i))
    ((MonoidHom.id (FreeGroup ((i : ι) × X i)) : (a : FreeGroup ((i : ι) × X i)) → FreeGroup ((i : ι) × X i))
        (FreeGroup.of a) :
      FreeGroup ((i : ι) × X i))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst_2 : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis.{u_5, u_6} (X i) (G i)
⊢ Eq (α := CoprodI G →* CoprodI G)
    (MonoidHom.comp (N := FreeGroup ((i : ι) × X i))
      ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
        fun (x : (i : ι) × X i) ↦
        (of (M := G) : (a : G x.fst) → CoprodI G)
          ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i))))
      ((lift (M := G) : (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
        fun (i : ι) ↦
        ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i)) fun (x : X i) ↦
          FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x)))
    (MonoidHom.id (CoprodI G))
have h : ∀ (i : ι),
  Eq (α := G i →* CoprodI G)
    (MonoidHom.comp (N := CoprodI G)
      (MonoidHom.comp (N := FreeGroup ((i : ι) × X i))
        ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
          fun (x : (i : ι) × X i) ↦
          (of (M := G) : (a : G x.fst) → CoprodI G)
            ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i))))
        ((lift (M := G) : (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
          fun (i : ι) ↦
          ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i)) fun (x : X i) ↦
            FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x)))
      (of (M := G)))
    (MonoidHom.comp (MonoidHom.id (CoprodI G)) (of (M := G)))
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst_2 : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis.{u_5, u_6} (X i) (G i)
i : ι
⊢ Eq (α := G i →* CoprodI G)
    (MonoidHom.comp (N := CoprodI G)
      (MonoidHom.comp (N := FreeGroup ((i : ι) × X i))
        ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
          fun (x : (i : ι) × X i) ↦
          (of (M := G) : (a : G x.fst) → CoprodI G)
            ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i))))
        ((lift (M := G) : (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
          fun (i : ι) ↦
          ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i)) fun (x : X i) ↦
            FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x)))
      (of (M := G)))
    (MonoidHom.comp (MonoidHom.id (CoprodI G)) (of (M := G)))
have h : ∀ (i_1 : X i),
  Eq (α := CoprodI G)
    (((MonoidHom.comp (N := CoprodI G)
              (MonoidHom.comp (N := FreeGroup ((i : ι) × X i))
                ((FreeGroup.lift : (a : (i : ι) × X i → CoprodI G) → FreeGroup ((i : ι) × X i) →* CoprodI G)
                  fun (x : (i : ι) × X i) ↦
                  (of (M := G) : (a : G x.fst) → CoprodI G)
                    ((B (x.fst (β := fun (i : ι) ↦ X i)) : (a : X x.fst) → G x.fst) (x.snd (β := fun (i : ι) ↦ X i))))
                ((lift (M := G) :
                    (a : (i : ι) → G i →* FreeGroup ((i : ι) × X i)) → CoprodI G →* FreeGroup ((i : ι) × X i))
                  fun (i : ι) ↦
                  ((B i).lift : (a : X i → FreeGroup ((i : ι) × X i)) → G i →* FreeGroup ((i : ι) × X i))
                    fun (x : X i) ↦ FreeGroup.of (Sigma.mk (β := fun (i : ι) ↦ X i) i x)))
              (of (M := G)) :
            G i →* CoprodI G) :
          (a : G i) → CoprodI G)
        ((B i : (a : X i) → G i) i_1) :
      CoprodI G)
    ((MonoidHom.comp (MonoidHom.id (CoprodI G)) (of (M := G)) : (a : G i) → CoprodI G) ((B i : (a : X i) → G i) i_1) :
      CoprodI G)
Tactic: apply (B i).ext_hom
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
⊢ FreeGroup ι ≃* CoprodI fun (x : ι) ↦ FreeGroup Unit
have refine_1 : FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit
Tactic: refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
refine_1 : FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit
⊢ FreeGroup ι ≃* CoprodI fun (x : ι) ↦ FreeGroup Unit
have refine_2 : (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι
Tactic: refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
refine_1 : FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit
refine_2 : (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι
⊢ FreeGroup ι ≃* CoprodI fun (x : ι) ↦ FreeGroup Unit
have refine_3 : Eq.{u_1 + 1} (α := FreeGroup ι →* FreeGroup ι)
  (MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
    ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
        (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
      fun (i : ι) ↦
      (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦ FreeGroup.of i)
    ((FreeGroup.lift :
        (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
      fun (i : ι) ↦
      ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) : FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of ())))
  (MonoidHom.id (FreeGroup ι))
Tactic: refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
refine_1 : FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit
refine_2 : (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι
refine_3 :
  Eq.{u_1 + 1} (α := FreeGroup ι →* FreeGroup ι)
    (MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
      ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
          (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
        fun (i : ι) ↦
        (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦ FreeGroup.of i)
      ((FreeGroup.lift :
          (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
        fun (i : ι) ↦
        ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) : FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
            (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
          (FreeGroup.of ())))
    (MonoidHom.id (FreeGroup ι))
⊢ FreeGroup ι ≃* CoprodI fun (x : ι) ↦ FreeGroup Unit
have refine_4 : Eq.{u_1 + 1} (α := (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
  (MonoidHom.comp (N := FreeGroup ι)
    ((FreeGroup.lift :
        (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
      fun (i : ι) ↦
      ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) : FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of ()))
    ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
        (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
      fun (i : ι) ↦
      (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦ FreeGroup.of i))
  (MonoidHom.id (CoprodI fun (x : ι) ↦ FreeGroup Unit))
Tactic: refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeGroup ι →* FreeGroup ι)
    (MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
      ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
          (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
        fun (i : ι) ↦
        (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦ FreeGroup.of i)
      ((FreeGroup.lift :
          (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
        fun (i : ι) ↦
        ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) : FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
            (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
          (FreeGroup.of ())))
    (MonoidHom.id (FreeGroup ι))
have refine_3 : ∀ (a : ι),
  Eq (α := FreeGroup ι)
    ((MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
            ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
                (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
              fun (i : ι) ↦
              (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦
                FreeGroup.of i)
            ((FreeGroup.lift :
                (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
              fun (i : ι) ↦
              ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) :
                    FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
                  (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
                (FreeGroup.of ())) :
          (a : FreeGroup ι) → FreeGroup ι)
        (FreeGroup.of a) :
      FreeGroup ι)
    ((MonoidHom.id (FreeGroup ι) : (a : FreeGroup ι) → FreeGroup ι) (FreeGroup.of a) : FreeGroup ι)
Tactic: ext