awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : P
⊢ Eq (α := (M ∗ N) ∗ P)
    ((symm (coprodAssoc M N P) : (a : M ∗ (N ∗ P)) → (M ∗ N) ∗ P)
        ((inr : (a : N ∗ P) → M ∗ (N ∗ P)) ((inr : (a : P) → N ∗ P) x)) :
      (M ∗ N) ∗ P)
    ((inr : (a : P) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Sum.map, Quotient.liftOn', List.map, List.foldl, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
m : M i
⊢ Eq (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
    ((Con.mk' (conGen (Rel M)) : (a : FreeMonoid (Sigma M)) → (conGen (Rel M)).Quotient)
        (FreeMonoid.of (Sigma.mk (β := M) i m)) :
      Con.Quotient (conGen (Rel M)))

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((f.comp (Con.mk' (conGen (Rel M))) : (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i x)) :
      N)
    ((g.comp (Con.mk' (conGen (Rel M))) : (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i x)) :
      N)

Tactic:
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply]

Premises used: Monoid.CoprodI.of_apply, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
unfold :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)

Tactic:
unfold CoprodI

Premises used: Monoid.CoprodI
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
rw :
  Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
rw₁ :
  Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N) ((g.comp (of (M := M)) : (a : M i) → N) x : N)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := N) ((g.comp (of (M := M)) : (a : M i) → N) x : N) ((g.comp (of (M := M)) : (a : M i) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)

Tactic:
rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]

Premises used: MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N
i : ι
⊢ Eq.{u_3 + 1} (α := N)
    (((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)) :
          (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i 1)) :
      N)
    (((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)) :
          (a : FreeMonoid ((i : ι) × M i)) → N)
        1 :
      N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N
i : ι
x y : M i
⊢ Eq.{u_3 + 1} (α := N)
    (((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)) :
          (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i x) *
          FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i y)) :
      N)
    (((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)) :
          (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i (x * y))) :
      N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_3 + 1} (α := N)
      (((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N))
              ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                  Con.lift (conGen (Rel M))
                    ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                      fun (p : (i : ι) × M i) ↦
                      (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                    ⋯)
                fi)
              i :
            (a : M i) → N)
          x :
        N)
      ((fi i : (a : M i) → N) x : N)
⊢ (fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N))
      ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
          Con.lift (conGen (Rel M))
            ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
              (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
            ⋯)
        fi) =
    fi

Tactic:
ext i x
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N
i : ι
x : M i
⊢ Eq.{u_3 + 1} (α := N)
    (((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N))
            ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                Con.lift (conGen (Rel M))
                  ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                    fun (p : (i : ι) × M i) ↦
                    (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                  ⋯)
              fi)
            i :
          (a : M i) → N)
        x :
      N)
    ((fi i : (a : M i) → N) x : N)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f : CoprodI M →* N
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_3 + 1} (α := N)
      ((MonoidHom.comp
              ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                  Con.lift (conGen (Rel M))
                    ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                      fun (p : (i : ι) × M i) ↦
                      (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                    ⋯)
                ((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N)) f))
              (of (M := M)) :
            (a : M i) → N)
          x :
        N)
      ((f.comp (of (M := M)) : (a : M i) → N) x : N)
⊢ (fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
        Con.lift (conGen (Rel M))
          ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
          ⋯)
      ((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N)) f) =
    f

Tactic:
ext i x
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f : CoprodI M →* N
i : ι
x : M i
⊢ Eq.{u_3 + 1} (α := N)
    ((MonoidHom.comp
            ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                Con.lift (conGen (Rel M))
                  ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                    fun (p : (i : ι) × M i) ↦
                    (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                  ⋯)
              ((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N)) f))
            (of (M := M)) :
          (a : M i) → N)
        x :
      N)
    ((f.comp (of (M := M)) : (a : M i) → N) x : N)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
i : ι
⊢ MonoidHom.comp ((lift (M := M) : (a : (i : ι) → M i →* N) → CoprodI M →* N) fi) (of (M := M)) = fi i

Tactic:
congr_fun (lift.symm_apply_apply fi) i

Premises used: Equiv.symm_apply_apply, Monoid.CoprodI.lift, congr_fun
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
i : ι
m : M i
⊢ Eq.{u_4 + 1} (α := N)
    ((((lift (M := M) : (a : (i : ι) → M i →* N) → CoprodI M →* N) fi : CoprodI M →* N) : (a : CoprodI M) → N)
        ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) :
      N)
    ((fi i : (a : M i) → N) m : N)

Tactic:
DFunLike.congr_fun (lift_comp_of ..) m

Premises used: DFunLike.congr_fun, FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, Monoid.CoprodI.lift_comp_of
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
f : CoprodI M →* N
⊢ ((lift (M := fun (i : ι) ↦ M i) : (a : (i : ι) → M i →* N) → (CoprodI fun (i : ι) ↦ M i) →* N) fun (i : ι) ↦
      f.comp (of (M := M))) =
    f

Tactic:
lift.apply_symm_apply f

Premises used: Equiv.apply_symm_apply, Monoid.CoprodI.lift
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
⊢ Eq (α := CoprodI M →* CoprodI M)
    ((lift (M := M) : (a : (i : ι) → M i →* CoprodI M) → CoprodI M →* CoprodI M) fun (i : ι) ↦ of (M := M))
    (MonoidHom.id (CoprodI M))

Tactic:
lift_comp_of' (.id _)

Premises used: MonoidHom.id, Con.toQuotient, Monoid.CoprodI.lift_comp_of'
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
⊢ (((lift (M := M) : (a : (i_1 : ι) → M i_1 →* M i) → CoprodI M →* M i)
            (Pi.mulSingle (M := fun (i_1 : ι) ↦ M i_1 →* M i) i (MonoidHom.id (M i))) :
          CoprodI M →* M i) :
        (a : CoprodI M) → M i)
      ((of (M := M) : (a : M i) → CoprodI M) x) =
    x

Tactic:
simp only [lift_of, Pi.mulSingle_eq_same, MonoidHom.id_apply]

Premises used: Monoid.CoprodI.lift_of, Pi.mulSingle_eq_same, MonoidHom.id_apply
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective (α := M i) (β := CoprodI M) (⇑(of (M := M)) : (a : M i) → CoprodI M)

Tactic:
(of_leftInverse i).injective

Premises used: Function.LeftInverse.injective, Monoid.CoprodI.of_leftInverse
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective (α := M i) (β := CoprodI M) (⇑(of (M := M)) : (a : M i) → CoprodI M)

Tactic:
exact (of_leftInverse i).injective

Premises used: Function.LeftInverse.injective, Monoid.CoprodI.of_leftInverse
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective (α := M i) (β := CoprodI M) (⇑(of (M := M)) : (a : M i) → CoprodI M)

Tactic:
classical exact (of_leftInverse i).injective
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
f : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
rw :
  Eq.{u_4 + 1} (α := Submonoid N)
    (⨆ (i : ι),
      Submonoid.closure
        (range fun (b : M i) ↦
          (f ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).fst (β := fun (i : ι) ↦ M i)) : (a : M ⟨i, b⟩.fst) → N)
            ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).snd (β := fun (i : ι) ↦ M i))))
    (⨆ (i : ι), MonoidHom.mrange (f i))
⊢ Eq (α := Submonoid N)
    (MonoidHom.mrange (F := CoprodI M →* N)
      ((lift (M := M) : (a : (i : ι) → M i →* N) → CoprodI M →* N) f : CoprodI M →* N))
    (⨆ (i : ι), MonoidHom.mrange (f i))

Tactic:
rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
    range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]

Premises used: Set.range_sigma_eq_iUnion_range, Monoid.CoprodI.lift, FreeMonoid.mrange_lift, Equiv.coe_fn_mk, Con.lift_range, Submonoid.closure_iUnion
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
f : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
⊢ Eq.{u_4 + 1} (α := Submonoid N)
    (⨆ (i : ι),
      Submonoid.closure
        (range fun (b : M i) ↦
          (f ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).fst (β := fun (i : ι) ↦ M i)) : (a : M ⟨i, b⟩.fst) → N)
            ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).snd (β := fun (i : ι) ↦ M i))))
    (⨆ (i : ι), MonoidHom.mrange (f i))

Tactic:
simp +instances only [MonoidHom.mclosure_range]

Premises used: MonoidHom.mclosure_range
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
f : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
s : Submonoid N
⊢ MonoidHom.mrange (F := CoprodI M →* N)
        ((lift (M := M) : (a : (i : ι) → M i →* N) → CoprodI M →* N) f : CoprodI M →* N) ≤
      s ↔
    ∀ (i : ι), MonoidHom.mrange (f i) ≤ s

Tactic:
simp [mrange_eq_iSup]

Premises used: Monoid.CoprodI.mrange_eq_iSup
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
⊢ Eq (α := Submonoid (CoprodI M)) (⨆ (i : ι), MonoidHom.mrange (F := M i →* CoprodI M) (of (M := M))) ⊤

Tactic:
simp [← mrange_eq_iSup]

Premises used: Monoid.CoprodI.mrange_eq_iSup
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
⊢ Eq (α := Submonoid (CoprodI M))
    (Submonoid.closure (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M))) ⊤

Tactic:
simp [Submonoid.closure_iUnion]

Premises used: Submonoid.closure_iUnion
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
⊢ motive 1

Tactic:
one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
⊢ motive 1

Tactic:
exact one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
x : CoprodI M
hx : Membership.mem (γ := Set (CoprodI M)) (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M)) x
y : CoprodI M
ihy : motive y
⊢ ∃ (i : ι) (m : M i), (of (M := M) : (a : M i) → CoprodI M) m = x

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
x : CoprodI M
hx : Membership.mem (γ := Set (CoprodI M)) (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M)) x
y : CoprodI M
ihy : motive y
mul_left :
  ∀ (i : ι) (m : M i)
    (hx :
      Membership.mem (α := CoprodI M) (γ := Set (CoprodI M))
        (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M))
        ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)),
    motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) y)
⊢ motive (x * y)

Tactic:
obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
y : CoprodI M
ihy : motive y
i : ι
m : M i
hx :
  Membership.mem (α := CoprodI M) (γ := Set (CoprodI M))
    (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M))
    ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
⊢ motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) y)

Tactic:
mul m y ihy
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
y : CoprodI M
ihy : motive y
i : ι
m : M i
hx :
  Membership.mem (α := CoprodI M) (γ := Set (CoprodI M))
    (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M))
    ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
⊢ motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) y)

Tactic:
exact mul m y ihy
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
m : CoprodI M
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
one₁ : motive 1
mul_left :
  ∀ (x : CoprodI M)
    (hx :
      Membership.mem (γ := Set (CoprodI M)) (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M)) x)
    (y : CoprodI M) (ihy : motive y), motive (x * y)
⊢ motive m

Tactic:
induction m using Submonoid.induction_of_closure_eq_top_left mclosure_iUnion_range_of with
  | one => exact one
  | mul_left x hx y ihy =>
    obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
    exact mul m y ihy

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
m : CoprodI M
one : motive 1
of : ∀ (i : ι) (m : M i), motive ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m)
mul : ∀ (x y : CoprodI M), motive x → motive y → motive (x * y)
⊢ motive m

Tactic:
induction_left m one fun {_} _ _ ↦ mul _ _ (of _ _)

Premises used: Monoid.CoprodI.induction_left
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
x : CoprodI G
⊢ x⁻¹ =
    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)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.CoprodI
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
rw :
  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
⊢ m⁻¹ * m = 1

Tactic:
rw [inv_def]

Premises used: Monoid.CoprodI.inv_def
-- Module: Mathlib.GroupTheory.CoprodI
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
one₂ one₃ : Eq (α := CoprodI G) 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

Tactic:
rw [map_one, MulOpposite.unop_one, one_mul]

Premises used: map_one, MulOpposite.unop_one, one_mul
-- Module: Mathlib.GroupTheory.CoprodI
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 :
  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
⊢ 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)ᵐᵒᵖ) (CoprodI.of (M := G)) :
                    (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                  (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
              (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
            ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih)) :
        CoprodI G)
      ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1

Tactic:
change of _⁻¹ * of _ = 1

Premises used: Monoid.CoprodI.of, Inv.inv, DFunLike.coe