ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(Monoid.PushoutI.base φ) h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(Monoid.PushoutI.of i) g • w = (Monoid.PushoutI.NormalWord.equivPair i).symm (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w; { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(Monoid.PushoutI.of i) g • w = g • w
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(Monoid.PushoutI.base φ) h • w = h • w
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>Monoid.PushoutI.NormalWord.cons g w hmw hgr = (Monoid.PushoutI.of i) g • w
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(g • w).prod = (Monoid.PushoutI.of i) g * w.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>h : H<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(h • w).prod = (Monoid.PushoutI.base φ) h * w.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>g : Monoid.PushoutI φ<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>(g • w).prod = g * w.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<GOAL>Monoid.PushoutI.NormalWord.empty.prod = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>(Monoid.PushoutI.NormalWord.cons g w hmw hgr).prod = (Monoid.PushoutI.of i) g * w.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>w.prod • Monoid.PushoutI.NormalWord.empty = w
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<GOAL>Function.Injective Monoid.PushoutI.NormalWord.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Function.Injective ⇑(φ i)<VAR>i : ι<GOAL>Function.Injective ⇑(Monoid.PushoutI.of i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Function.Injective ⇑(φ i)<GOAL>Function.Injective ⇑(Monoid.PushoutI.base φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>w : Monoid.CoprodI.Word G<VAR>hw : Monoid.PushoutI.Reduced φ w<GOAL>∃ w', w'.prod = Monoid.PushoutI.ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Function.Injective ⇑(φ i)<VAR>w : Monoid.CoprodI.Word G<VAR>hw : Monoid.PushoutI.Reduced φ w<VAR>h : Monoid.PushoutI.ofCoprodI w.prod ∈ (Monoid.PushoutI.base φ).range<GOAL>w = Monoid.CoprodI.Word.empty
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Function.Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(Monoid.PushoutI.of i).range ⊓ (Monoid.PushoutI.of j).range = (Monoid.PushoutI.base φ).range
<VAR>G : Type u_1<VAR>CategoryTheory.Groupoid G<VAR>self : IsFreeGroupoid G<VAR>X : Type v<VAR>Group X<VAR>f : Quiver.Labelling (IsFreeGroupoid.Generators G) X<GOAL>∃! F, ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (IsFreeGroupoid.of g) = f g
<VAR>G : Type u_1<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>X : Type v<VAR>Group X<VAR>f g : G ⥤ CategoryTheory.SingleObj X<VAR>h : ∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)<GOAL>f = g
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<VAR>a : G<VAR>p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a<GOAL>IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<GOAL>IsFreeGroupoid.SpanningTree.treeHom T (IsFreeGroupoid.SpanningTree.root' T) = 𝟙 (IsFreeGroupoid.SpanningTree.root' T)
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<VAR>a b : IsFreeGroupoid.Generators G<VAR>e : a ⟶ b<VAR>H : e ∈ Quiver.wideSubquiverSymmetrify T a b<GOAL>IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e) = 𝟙 (IsFreeGroupoid.SpanningTree.root' T)
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<VAR>X : Type u_1<VAR>Monoid X<VAR>f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T) →* X<GOAL>∀ (x : G), (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).obj x = ()
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<VAR>X : Type u_1<VAR>Monoid X<VAR>f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T) →* X<GOAL>∀ {X_1 Y : G} (p : X_1 ⟶ Y), (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).map p = f (IsFreeGroupoid.SpanningTree.loopOfHom T p)
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))<VAR>Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)<GOAL>IsFreeGroup (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T))
<VAR>G : Type u<VAR>CategoryTheory.Groupoid G<VAR>IsFreeGroupoid G<VAR>a b : G<GOAL>Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β<VAR>x : m α<GOAL>f <$> x = x >>= pure ∘ f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>a : α<GOAL>PLift.map f { down := a } = { down := f a }
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>x : α<GOAL>({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
<VAR>α : Sort u<VAR>β : Sort v<VAR>a : α<VAR>f : α → PLift β<GOAL>{ down := a }.bind f = f a
<VAR>α : Sort u<VAR>β : Type v<VAR>b : β<GOAL>(PLift.rec fun x => b) = fun x => b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>ULift.map f { down := a } = { down := f a }
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : α → ULift β<GOAL>{ down := a }.bind f = f a
<VAR>α : Type u<VAR>β : Sort v<VAR>b : β<GOAL>(ULift.rec fun x => b) = fun x => b
<VAR>M : Type u → Type v<VAR>α ω : Type u<VAR>x x' : WriterT ω M α<VAR>h : x.run = x'.run<GOAL>x = x'
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>self : Monoid.CoprodI.Word M<GOAL>List.Chain' (fun l l' => l.fst ≠ l'.fst) self.toList
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>self : Monoid.CoprodI.Word M<VAR>l : (i : ι) × M i<GOAL>l ∈ self.toList → l.snd ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>m : M i<GOAL>Monoid.CoprodI.of m = (conGen (Monoid.CoprodI.Rel M)).mk' (FreeMonoid.of ⟨i, m⟩)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>Monoid N<VAR>f g : Monoid.CoprodI M →* N<VAR>h : ∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of<GOAL>f = g
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>Monoid N<VAR>f : Monoid.CoprodI M →* N<VAR>i : ι<GOAL>Monoid.CoprodI.lift.symm f i = f.comp Monoid.CoprodI.of
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_4<VAR>Monoid N<VAR>fi : (i : ι) → M i →* N<VAR>i : ι<GOAL>(Monoid.CoprodI.lift fi).comp Monoid.CoprodI.of = fi i
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_4<VAR>Monoid N<VAR>fi : (i : ι) → M i →* N<VAR>i : ι<VAR>m : M i<GOAL>(Monoid.CoprodI.lift fi) (Monoid.CoprodI.of m) = (fi i) m
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_4<VAR>Monoid N<VAR>f : Monoid.CoprodI M →* N<GOAL>(Monoid.CoprodI.lift fun i => f.comp Monoid.CoprodI.of) = f
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>(Monoid.CoprodI.lift fun i => Monoid.CoprodI.of) = MonoidHom.id (Monoid.CoprodI M)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>Function.LeftInverse ⇑(Monoid.CoprodI.lift (Pi.mulSingle i (MonoidHom.id (M i)))) ⇑Monoid.CoprodI.of
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<GOAL>Function.Injective ⇑Monoid.CoprodI.of
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_4<VAR>Monoid N<VAR>f : (i : ι) → M i →* N<GOAL>MonoidHom.mrange (Monoid.CoprodI.lift f) = ⨆ i, MonoidHom.mrange (f i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>N : Type u_4<VAR>Monoid N<VAR>f : (i : ι) → M i →* N<VAR>s : Submonoid N<GOAL>MonoidHom.mrange (Monoid.CoprodI.lift f) ≤ s ↔ ∀ (i : ι), MonoidHom.mrange (f i) ≤ s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>⨆ i, MonoidHom.mrange Monoid.CoprodI.of = ⊤
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>Submonoid.closure (⋃ i, Set.range ⇑Monoid.CoprodI.of) = ⊤
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>C : Monoid.CoprodI M → Prop<VAR>m : Monoid.CoprodI M<VAR>one : C 1<VAR>mul : ∀ {i : ι} (m : M i) (x : Monoid.CoprodI M), C x → C (Monoid.CoprodI.of m * x)<GOAL>C m
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>C : Monoid.CoprodI M → Prop<VAR>m : Monoid.CoprodI M<VAR>h_one : C 1<VAR>h_of : ∀ (i : ι) (m : M i), C (Monoid.CoprodI.of m)<VAR>h_mul : ∀ (x y : Monoid.CoprodI M), C x → C y → C (x * y)<GOAL>C m
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>x : Monoid.CoprodI G<GOAL>x⁻¹ = MulOpposite.unop ((Monoid.CoprodI.lift fun i => (MonoidHom.op Monoid.CoprodI.of).comp (MulEquiv.inv' (G i)).toMonoidHom) x)
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>N : Type u_5<VAR>Group N<VAR>f : (i : ι) → G i →* N<VAR>s : Subgroup N<VAR>h : ∀ (i : ι), (f i).range ≤ s<GOAL>(Monoid.CoprodI.lift f).range ≤ s
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>N : Type u_5<VAR>Group N<VAR>f : (i : ι) → G i →* N<GOAL>(Monoid.CoprodI.lift f).range = ⨆ i, (f i).range
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>Monoid.CoprodI.Word.empty.toList = []
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>Monoid.CoprodI.Word.empty.prod = 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>w : Monoid.CoprodI.Word M<VAR>i : ι<GOAL>w.fstIdx ≠ some i ↔ ∀ l ∈ w.toList.head?, i ≠ l.fst
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>self : Monoid.CoprodI.Word.Pair M i<GOAL>self.tail.fstIdx ≠ some i
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<VAR>hmw : w.fstIdx ≠ some i<VAR>h1 : m ≠ 1<GOAL>(Monoid.CoprodI.Word.cons m w hmw h1).toList = ⟨i, m⟩ :: w.toList
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>p : Monoid.CoprodI.Word.Pair M i<GOAL>(Monoid.CoprodI.Word.rcons p).prod = Monoid.CoprodI.of p.head * p.tail.prod
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>i : ι<GOAL>Function.Injective Monoid.CoprodI.Word.rcons
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>i j : ι<VAR>p : Monoid.CoprodI.Word.Pair M i<VAR>m : M j<GOAL>⟨j, m⟩ ∈ (Monoid.CoprodI.Word.rcons p).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ ∃ (h : i = j), m = h ▸ p.head
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<VAR>hmw : w.fstIdx ≠ some i<VAR>h1 : m ≠ 1<GOAL>(Monoid.CoprodI.Word.cons m w hmw h1).fstIdx = some i
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<VAR>h1 : m ≠ 1<VAR>h2 : w.fstIdx ≠ some i<GOAL>(Monoid.CoprodI.Word.cons m w h2 h1).prod = Monoid.CoprodI.of m * w.prod
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>motive : Monoid.CoprodI.Word M → Sort u_4<VAR>h_empty : motive Monoid.CoprodI.Word.empty<VAR>h_cons : (i : ι) → (m : M i) → (w : Monoid.CoprodI.Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Monoid.CoprodI.Word.cons m w h1 h2)<GOAL>Monoid.CoprodI.Word.consRecOn Monoid.CoprodI.Word.empty h_empty h_cons = h_empty
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>motive : Monoid.CoprodI.Word M → Sort u_4<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<VAR>h1 : w.fstIdx ≠ some i<VAR>h2 : m ≠ 1<VAR>h_empty : motive Monoid.CoprodI.Word.empty<VAR>h_cons : (i : ι) → (m : M i) → (w : Monoid.CoprodI.Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Monoid.CoprodI.Word.cons m w h1 h2)<GOAL>Monoid.CoprodI.Word.consRecOn (Monoid.CoprodI.Word.cons m w h1 h2) h_empty h_cons = h_cons i m w h1 h2 (Monoid.CoprodI.Word.consRecOn w h_empty h_cons)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>p : Monoid.CoprodI.Word.Pair M i<GOAL>(Monoid.CoprodI.Word.equivPair i).symm p = Monoid.CoprodI.Word.rcons p
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>w : Monoid.CoprodI.Word M<VAR>h : w.fstIdx ≠ some i<GOAL>(Monoid.CoprodI.Word.equivPair i) w = { head := 1, tail := w, fstIdx_ne := h }
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>w : Monoid.CoprodI.Word M<VAR>m : M i<GOAL>⟨i, m⟩ ∈ ((Monoid.CoprodI.Word.equivPair j) w).tail.toList ↔ ⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>w : Monoid.CoprodI.Word M<VAR>m : M i<GOAL>⟨i, m⟩ ∈ ((Monoid.CoprodI.Word.equivPair j) w).tail.toList → ⟨i, m⟩ ∈ w.toList
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>w : Monoid.CoprodI.Word M<GOAL>((Monoid.CoprodI.Word.equivPair i) w).head = if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<GOAL>m • w = Monoid.CoprodI.Word.rcons (let __src := (Monoid.CoprodI.Word.equivPair i) w; { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>w : Monoid.CoprodI.Word M<VAR>m : M i<GOAL>Monoid.CoprodI.of m • w = Monoid.CoprodI.Word.rcons (let __src := (Monoid.CoprodI.Word.equivPair i) w; { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<GOAL>(Monoid.CoprodI.Word.equivPair i) (Monoid.CoprodI.of m • w) = { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := ((Monoid.CoprodI.Word.equivPair i) w).tail, fstIdx_ne := ⋯ }
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>p : Monoid.CoprodI.Word.Pair M i<GOAL>(Monoid.CoprodI.Word.equivPair i) p.tail = { head := 1, tail := p.tail, fstIdx_ne := ⋯ }
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>w : Monoid.CoprodI.Word M<GOAL>m • w = Monoid.CoprodI.of m • w
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>m₁ : M i<VAR>m₂ : M j<VAR>w : Monoid.CoprodI.Word M<GOAL>⟨i, m₁⟩ ∈ (Monoid.CoprodI.of m₂ • w).toList ↔ ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨ m₁ ≠ 1 ∧ ∃ (hij : i = j), ⟨i, m₁⟩ ∈ w.toList.tail ∨ (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>m₁ : M i<VAR>m₂ : M j<VAR>w : Monoid.CoprodI.Word M<GOAL>⟨i, m₁⟩ ∈ (Monoid.CoprodI.of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>ls : Monoid.CoprodI.Word M<VAR>h1 : ls.fstIdx ≠ some i<VAR>h2 : m ≠ 1<GOAL>Monoid.CoprodI.Word.cons m ls h1 h2 = Monoid.CoprodI.of m • ls
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>p : Monoid.CoprodI.Word.Pair M i<GOAL>Monoid.CoprodI.Word.rcons p = Monoid.CoprodI.of p.head • p.tail
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>w : Monoid.CoprodI.Word M<GOAL>Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head • ((Monoid.CoprodI.Word.equivPair i) w).tail = w
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>w : Monoid.CoprodI.Word G<GOAL>((Monoid.CoprodI.Word.equivPair i) w).tail = (Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head)⁻¹ • w
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>C : Monoid.CoprodI.Word M → Prop<VAR>h_empty : C Monoid.CoprodI.Word.empty<VAR>h_smul : ∀ (i : ι) (m : M i) (w : Monoid.CoprodI.Word M), C w → C (Monoid.CoprodI.of m • w)<VAR>w : Monoid.CoprodI.Word M<GOAL>C w
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>(i : ι) → DecidableEq (M i)<VAR>DecidableEq ι<VAR>m : Monoid.CoprodI M<VAR>w : Monoid.CoprodI.Word M<GOAL>(m • w).prod = m * w.prod
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord M i j<GOAL>w.toList ≠ []
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord M i j<GOAL>w.toList.head? = some ⟨i, w.head⟩
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord M i j<GOAL>w.toList.getLast? = some ⟨j, w.last⟩
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>w : Monoid.CoprodI.Word M<VAR>h : w ≠ Monoid.CoprodI.Word.empty<GOAL>∃ i j w', w'.toWord = w
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>x : M i<VAR>hne_one : x ≠ 1<GOAL>(Monoid.CoprodI.NeWord.singleton x hne_one).head = x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>x : M i<VAR>hne_one : x ≠ 1<GOAL>(Monoid.CoprodI.NeWord.singleton x hne_one).last = x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i : ι<VAR>x : M i<VAR>hne_one : x ≠ 1<GOAL>(Monoid.CoprodI.NeWord.singleton x hne_one).prod = Monoid.CoprodI.of x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j k l : ι<VAR>w₁ : Monoid.CoprodI.NeWord M i j<VAR>hne : j ≠ k<VAR>w₂ : Monoid.CoprodI.NeWord M k l<GOAL>(w₁.append hne w₂).head = w₁.head
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j k l : ι<VAR>w₁ : Monoid.CoprodI.NeWord M i j<VAR>hne : j ≠ k<VAR>w₂ : Monoid.CoprodI.NeWord M k l<GOAL>(w₁.append hne w₂).last = w₂.last
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j k l : ι<VAR>w₁ : Monoid.CoprodI.NeWord M i j<VAR>hne : j ≠ k<VAR>w₂ : Monoid.CoprodI.NeWord M k l<GOAL>(w₁.append hne w₂).prod = w₁.prod * w₂.prod
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>x : M i<VAR>hnotone : x ≠ 1<VAR>w : Monoid.CoprodI.NeWord M i j<GOAL>(Monoid.CoprodI.NeWord.replaceHead x hnotone w).head = x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord M i j<VAR>x : M i<VAR>hnotone : x * w.head ≠ 1<GOAL>(w.mulHead x hnotone).head = x * w.head
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord M i j<VAR>x : M i<VAR>hnotone : x * w.head ≠ 1<GOAL>(w.mulHead x hnotone).prod = Monoid.CoprodI.of x * w.prod
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord G i j<GOAL>w.inv.prod = w.prod⁻¹
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord G i j<GOAL>w.inv.head = w.last⁻¹
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Group (G i)<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord G i j<GOAL>w.inv.last = w.head⁻¹