awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
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 ι
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:
exact lift_word_prod_nontrivial_of_not_empty f hcard X hXnonempty hXdisj hpp w h

Premises used: Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty
-- Module: Mathlib.GroupTheory.CoprodI
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)

Tactic:
apply (injective_iff_map_eq_one (lift f)).mpr

Premises used: Iff.mpr, Monoid.CoprodI.lift, DFunLike.coe, injective_iff_map_eq_one
-- Module: Mathlib.GroupTheory.CoprodI
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 ι
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)
⊢ ∀ (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:
rw [(CoprodI.Word.equiv).forall_congr_left]

Premises used: Equiv.forall_congr_left, Monoid.CoprodI.Word.equiv
-- Module: Mathlib.GroupTheory.CoprodI
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)
dsimp : w.prod (M := H) = 1
⊢ Eq (α := CoprodI H) ((Equiv.symm (Word.equiv (M := H)) : (a : Word H) → CoprodI H) w : CoprodI H) (1 : CoprodI H)

Tactic:
dsimp [Word.equiv] at *

Premises used: Monoid.CoprodI.Word.equiv
-- Module: Mathlib.GroupTheory.CoprodI
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
rw₁ rw₂ : Eq (α := CoprodI H) 1 1
⊢ w.prod (M := H) = 1

Tactic:
rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]

Premises used: Monoid.CoprodI.empty_of_word_prod_eq_one, Monoid.CoprodI.Word.prod_empty
-- Module: Mathlib.GroupTheory.CoprodI
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)
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
⊢ Function.Injective (α := CoprodI H) (β := G)
    (⇑((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)

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]

Premises used: Iff.mpr, Equiv.forall_congr_left, Monoid.CoprodI.lift, Monoid.CoprodI.Word.equiv, Monoid.CoprodI.Word.prod_empty, DFunLike.coe, injective_iff_map_eq_one
-- Module: Mathlib.GroupTheory.CoprodI
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)
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))
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.GroupTheory.CoprodI
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)
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:
simp
-- Module: Mathlib.GroupTheory.CoprodI
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)
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)))
⊢ 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))

Tactic:
ext1 i
-- Module: Mathlib.GroupTheory.CoprodI
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 : ι
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)
⊢ 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:
apply (B i).ext_hom

Premises used: FreeGroupBasis.ext_hom
-- Module: Mathlib.GroupTheory.CoprodI
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 : ι
⊢ ∀ (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:
simp
-- Module: Mathlib.GroupTheory.CoprodI
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
G : ι → Type u_5
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), IsFreeGroup.{u_5} (G i)
⊢ IsFreeGroup (CoprodI G)

Tactic:
(FreeGroupBasis.coprodI (fun i ↦ IsFreeGroup.basis (G i))).isFreeGroup

Premises used: FreeGroupBasis.isFreeGroup, Monoid.CoprodI.FreeGroupBasis.coprodI, IsFreeGroup.basis
-- Module: Mathlib.GroupTheory.CoprodI
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 ι))
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))
⊢ FreeGroup ι ≃* CoprodI fun (x : ι) ↦ FreeGroup Unit

Tactic:
refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_

Premises used: MonoidHom.toMulEquiv
-- Module: Mathlib.GroupTheory.CoprodI
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

Tactic:
exact FreeGroup.lift fun i => @CoprodI.of ι _ _ i (FreeGroup.of Unit.unit)

Premises used: FreeGroup.of, Unit.unit, Monoid.CoprodI.of, FreeGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι

Tactic:
exact CoprodI.lift fun i => FreeGroup.lift fun _ => FreeGroup.of i

Premises used: FreeGroup.of, Monoid.CoprodI.lift, FreeGroup.lift, DFunLike.coe
-- Module: Mathlib.GroupTheory.CoprodI
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_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 ι)
⊢ 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:
ext
-- Module: Mathlib.GroupTheory.CoprodI
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
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:
simp