ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.Red L₁ L₂<GOAL>FreeGroup.reduce L₁ = FreeGroup.reduce L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.Red L₁ L₂<GOAL>FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>h : FreeAddGroup.Red L₁ L₂<GOAL>FreeAddGroup.Red L₁ (FreeAddGroup.reduce L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>h : FreeGroup.Red L₁ L₂<GOAL>FreeGroup.Red L₁ (FreeGroup.reduce L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>h : FreeAddGroup.Red L₁ L₂<GOAL>FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>h : FreeGroup.Red L₁ L₂<GOAL>FreeGroup.Red L₂ (FreeGroup.reduce L₁)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.mk L₁ = FreeGroup.mk L₂<GOAL>FreeGroup.reduce L₁ = FreeGroup.reduce L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂<GOAL>FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.reduce L₁ = FreeGroup.reduce L₂<GOAL>FreeGroup.mk L₁ = FreeGroup.mk L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂<GOAL>FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeGroup.mk (FreeGroup.reduce L) = FreeGroup.mk L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeAddGroup.mk (FreeAddGroup.reduce L) = FreeAddGroup.mk L
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.Red L₁ L₂<GOAL>FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.Red L₁ L₂<GOAL>FreeGroup.Red L₂ (FreeGroup.reduce L₁)
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>FreeGroup.mk x.toWord = x
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>FreeAddGroup.mk x.toWord = x
<VAR>α : Type u<VAR>DecidableEq α<GOAL>Function.Injective FreeGroup.toWord
<VAR>α : Type u<VAR>DecidableEq α<GOAL>Function.Injective FreeAddGroup.toWord
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : FreeGroup α<GOAL>x.toWord = y.toWord ↔ x = y
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : FreeAddGroup α<GOAL>x.toWord = y.toWord ↔ x = y
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>DecidableEq α<GOAL>(FreeAddGroup.mk L₁).toWord = FreeAddGroup.reduce L₁
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>DecidableEq α<GOAL>(FreeGroup.mk L₁).toWord = FreeGroup.reduce L₁
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>FreeAddGroup.reduce x.toWord = x.toWord
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>FreeGroup.reduce x.toWord = x.toWord
<VAR>α : Type u<VAR>DecidableEq α<GOAL>FreeAddGroup.toWord 0 = []
<VAR>α : Type u<VAR>DecidableEq α<GOAL>FreeGroup.toWord 1 = []
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>x.toWord = [] ↔ x = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>x.toWord = [] ↔ x = 0
<VAR>α : Type u<VAR>DecidableEq α<VAR>w : List (α × Bool)<GOAL>FreeAddGroup.reduce (FreeAddGroup.negRev w) = FreeAddGroup.negRev (FreeAddGroup.reduce w)
<VAR>α : Type u<VAR>DecidableEq α<VAR>w : List (α × Bool)<GOAL>FreeGroup.reduce (FreeGroup.invRev w) = FreeGroup.invRev (FreeGroup.reduce w)
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>x⁻¹.toWord = FreeGroup.invRev x.toWord
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>(-x).toWord = FreeAddGroup.negRev x.toWord
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : L₂ ∈ List.filter (fun b => decide (FreeGroup.Red L₁ b)) L₁.sublists<GOAL>FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.Red L₁ L₂<GOAL>L₂ ∈ FreeGroup.Red.enum L₁
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>(-x).norm = x.norm
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>x⁻¹.norm = x.norm
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeGroup α<GOAL>x.norm = 0 ↔ x = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : FreeAddGroup α<GOAL>x.norm = 0 ↔ x = 0
<VAR>α : Type u<VAR>DecidableEq α<GOAL>FreeAddGroup.norm 0 = 0
<VAR>α : Type u<VAR>DecidableEq α<GOAL>FreeGroup.norm 1 = 0
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>DecidableEq α<GOAL>(FreeAddGroup.mk L₁).norm ≤ L₁.length
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>DecidableEq α<GOAL>(FreeGroup.mk L₁).norm ≤ L₁.length
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : FreeAddGroup α<GOAL>(x + y).norm ≤ x.norm + y.norm
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : FreeGroup α<GOAL>(x * y).norm ≤ x.norm + y.norm
<VAR>α : Type u<VAR>Preorder α<GOAL>LeftOrdContinuous id
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>LeftOrdContinuous f → RightOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<VAR>x : α<VAR>h : IsGreatest s x<GOAL>IsGreatest (f '' s) (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : LeftOrdContinuous g<VAR>hf : LeftOrdContinuous f<GOAL>LeftOrdContinuous (g ∘ f)
<VAR>α : Type u<VAR>Preorder α<VAR>f : α → α<VAR>hf : LeftOrdContinuous f<VAR>n : ℕ<GOAL>LeftOrdContinuous f^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>x y : α<GOAL>f (x ⊔ y) = f x ⊔ f y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>h : Function.Injective f<VAR>x y : α<GOAL>f x ≤ f y ↔ x ≤ y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>h : Function.Injective f<VAR>x y : α<GOAL>f x < f y ↔ x < y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>h : Function.Injective f<GOAL>⇑(LeftOrdContinuous.toOrderEmbedding f hf h) = f
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<GOAL>f (sSup s) = ⨆ x ∈ s, f x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<VAR>sne : s.Nonempty<VAR>sbdd : BddAbove s<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<VAR>hg : BddAbove (Set.range g)<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u<VAR>Preorder α<GOAL>RightOrdContinuous id
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>s : Set α<VAR>x : α<VAR>h : IsLeast s x<GOAL>IsLeast (f '' s) (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : RightOrdContinuous g<VAR>hf : RightOrdContinuous f<GOAL>RightOrdContinuous (g ∘ f)
<VAR>α : Type u<VAR>Preorder α<VAR>f : α → α<VAR>hf : RightOrdContinuous f<VAR>n : ℕ<GOAL>RightOrdContinuous f^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>x y : α<GOAL>f (x ⊓ y) = f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>h : Function.Injective f<VAR>x y : α<GOAL>f x ≤ f y ↔ x ≤ y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>h : Function.Injective f<VAR>x y : α<GOAL>f x < f y ↔ x < y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>h : Function.Injective f<GOAL>⇑(RightOrdContinuous.toOrderEmbedding f hf h) = f
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>s : Set α<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>s : Set α<GOAL>f (sInf s) = ⨅ x ∈ s, f x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>g : ι → α<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>s : Set α<VAR>sne : s.Nonempty<VAR>sbdd : BddBelow s<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>f : α → β<VAR>hf : RightOrdContinuous f<VAR>g : ι → α<VAR>hg : BddBelow (Set.range g)<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>LeftOrdContinuous ⇑e
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>RightOrdContinuous ⇑e
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>⇑(QuotientAddGroup.mk' N) = QuotientAddGroup.mk
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>⇑(QuotientGroup.mk' N) = QuotientGroup.mk
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>(QuotientGroup.mk' N) x = ↑x
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>(QuotientAddGroup.mk' N) x = ↑x
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>Function.Surjective ⇑(QuotientGroup.mk' N)
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>Function.Surjective ⇑(QuotientAddGroup.mk' N)
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>(QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y ↔ ∃ z ∈ N, x * z = y
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>(QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y ↔ ∃ z ∈ N, x + z = y
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>U : Set (G ⧸ N)<VAR>g : ↥N.op<GOAL>g • ⇑(QuotientGroup.mk' N) ⁻¹' U = ⇑(QuotientGroup.mk' N) ⁻¹' U
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>U : Set (G ⧸ N)<VAR>g : ↥N.op<GOAL>g +ᵥ ⇑(QuotientAddGroup.mk' N) ⁻¹' U = ⇑(QuotientAddGroup.mk' N) ⁻¹' U
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>Monoid M<VAR>f g : G ⧸ N →* M<VAR>h : f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)<GOAL>f = g
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>AddMonoid M<VAR>f g : G ⧸ N →+ M<VAR>h : f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)<GOAL>f = g
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>↑x = 1 ↔ x ∈ N
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>↑x = 0 ↔ x ∈ N
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>I : Type w<VAR>AddGroup I<VAR>f : G →+ H<VAR>f.range.Normal<VAR>g : H →+ I<GOAL>g.ker ≤ f.range ↔ (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>I : Type w<VAR>Group I<VAR>f : G →* H<VAR>f.range.Normal<VAR>g : H →* I<GOAL>g.ker ≤ f.range ↔ (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>(QuotientAddGroup.mk' N).ker = N
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>(QuotientGroup.mk' N).ker = N
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>↑x = ↑y ↔ x - y ∈ N
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>↑x = ↑y ↔ x / y ∈ N
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>↑0 = 0
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>↑1 = 1
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>a b : G<GOAL>↑(a + b) = ↑a + ↑b
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a b : G<GOAL>↑(a * b) = ↑a * ↑b
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>a : G<GOAL>↑(-a) = -↑a
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : G<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a b : G<GOAL>↑(a / b) = ↑a / ↑b
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>a b : G<GOAL>↑(a - b) = ↑a - ↑b
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>a : G<VAR>n : ℕ<GOAL>↑(n • a) = n • ↑a
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : G<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : G<VAR>n : ℤ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>a : G<VAR>n : ℤ<GOAL>↑(n • a) = n • ↑a
<VAR>G : Type u_1<VAR>ι : Type u_2<VAR>CommGroup G<VAR>N : Subgroup G<VAR>s : Finset ι<VAR>f : ι → G<GOAL>↑(s.prod f) = ∏ i ∈ s, ↑(f i)
<VAR>G : Type u_1<VAR>ι : Type u_2<VAR>AddCommGroup G<VAR>N : AddSubgroup G<VAR>s : Finset ι<VAR>f : ι → G<GOAL>↑(s.sum f) = ∑ i ∈ s, ↑(f i)
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>Subgroup.map (QuotientGroup.mk' N) N = ⊥
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>AddSubgroup.map (QuotientAddGroup.mk' N) N = ⊥
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>AddMonoid M<VAR>φ : G →+ M<VAR>HN : N ≤ φ.ker<VAR>g : G<GOAL>(QuotientAddGroup.lift N φ HN) ↑g = φ g
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>Monoid M<VAR>φ : G →* M<VAR>HN : N ≤ φ.ker<VAR>g : G<GOAL>(QuotientGroup.lift N φ HN) ↑g = φ g
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>AddMonoid M<VAR>φ : G →+ M<VAR>HN : N ≤ φ.ker<VAR>g : G<GOAL>(QuotientAddGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>M : Type x<VAR>Monoid M<VAR>φ : G →* M<VAR>HN : N ≤ φ.ker<VAR>g : G<GOAL>(QuotientGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>Group H<VAR>M : Subgroup H<VAR>M.Normal<VAR>f : G →* H<VAR>h : N ≤ Subgroup.comap f M<VAR>x : G<GOAL>(QuotientGroup.map N M f h) ↑x = ↑(f x)
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>AddGroup H<VAR>M : AddSubgroup H<VAR>M.Normal<VAR>f : G →+ H<VAR>h : N ≤ AddSubgroup.comap f M<VAR>x : G<GOAL>(QuotientAddGroup.map N M f h) ↑x = ↑(f x)
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>Group H<VAR>M : Subgroup H<VAR>M.Normal<VAR>f : G →* H<VAR>h : N ≤ Subgroup.comap f M<VAR>x : G<GOAL>(QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = ↑(f x)
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>AddGroup H<VAR>M : AddSubgroup H<VAR>M.Normal<VAR>f : G →+ H<VAR>h : N ≤ AddSubgroup.comap f M<VAR>x : G<GOAL>(QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = ↑(f x)
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯<VAR>x : G ⧸ N<GOAL>(QuotientGroup.map N N (MonoidHom.id G) h) x = x
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯<VAR>x : G ⧸ N<GOAL>(QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯<GOAL>QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯<GOAL>QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>AddGroup H<VAR>I : Type u_1<VAR>AddGroup I<VAR>M : AddSubgroup H<VAR>O : AddSubgroup I<VAR>M.Normal<VAR>O.Normal<VAR>f : G →+ H<VAR>g : H →+ I<VAR>hf : N ≤ AddSubgroup.comap f M<VAR>hg : M ≤ AddSubgroup.comap g O<VAR>hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯<VAR>x : G ⧸ N<GOAL>(QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>Group H<VAR>I : Type u_1<VAR>Group I<VAR>M : Subgroup H<VAR>O : Subgroup I<VAR>M.Normal<VAR>O.Normal<VAR>f : G →* H<VAR>g : H →* I<VAR>hf : N ≤ Subgroup.comap f M<VAR>hg : M ≤ Subgroup.comap g O<VAR>hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯<VAR>x : G ⧸ N<GOAL>(QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>Group H<VAR>I : Type u_1<VAR>Group I<VAR>M : Subgroup H<VAR>O : Subgroup I<VAR>M.Normal<VAR>O.Normal<VAR>f : G →* H<VAR>g : H →* I<VAR>hf : N ≤ Subgroup.comap f M<VAR>hg : M ≤ Subgroup.comap g O<VAR>hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯<GOAL>(QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>AddGroup H<VAR>I : Type u_1<VAR>AddGroup I<VAR>M : AddSubgroup H<VAR>O : AddSubgroup I<VAR>M.Normal<VAR>O.Normal<VAR>f : G →+ H<VAR>g : H →+ I<VAR>hf : N ≤ AddSubgroup.comap f M<VAR>hg : M ≤ AddSubgroup.comap g O<VAR>hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯<GOAL>(QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<GOAL>QuotientGroup.mk '' ↑N = 1
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<GOAL>QuotientAddGroup.mk '' ↑N = 0
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>s : Set G<GOAL>QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ↑N * s
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>s : Set G<GOAL>QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ↑N + s
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>s t : Set G<GOAL>QuotientGroup.mk '' s = QuotientGroup.mk '' t ↔ ↑N * s = ↑N * t
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>s t : Set G<GOAL>QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t ↔ ↑N + s = ↑N + t
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>G' : Subgroup G<VAR>H' : Subgroup H<VAR>G'.Normal<VAR>H'.Normal<VAR>e : G ≃* H<VAR>he : Subgroup.map (↑e) G' = H'<VAR>x : G<GOAL>(QuotientGroup.congr G' H' e he) ↑x = ↑(e x)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>G' : Subgroup G<VAR>H' : Subgroup H<VAR>G'.Normal<VAR>H'.Normal<VAR>e : G ≃* H<VAR>he : Subgroup.map (↑e) G' = H'<VAR>x : G<GOAL>(QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>G' : Subgroup G<VAR>H' : Subgroup H<VAR>G'.Normal<VAR>H'.Normal<VAR>e : G ≃* H<VAR>he : Subgroup.map (↑e) G' = H'<VAR>x : G<GOAL>(QuotientGroup.congr G' H' e he) ↑x = (QuotientGroup.mk' H') (e x)
<VAR>G : Type u<VAR>Group G<VAR>G' : Subgroup G<VAR>G'.Normal<VAR>he : Subgroup.map (↑(MulEquiv.refl G)) G' = G' := ⋯<GOAL>QuotientGroup.congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>G' : Subgroup G<VAR>H' : Subgroup H<VAR>G'.Normal<VAR>H'.Normal<VAR>e : G ≃* H<VAR>he : Subgroup.map (↑e) G' = H'<GOAL>(QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm ⋯
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<VAR>g : G<GOAL>(QuotientAddGroup.kerLift φ) ↑g = φ g
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<VAR>g : G<GOAL>(QuotientGroup.kerLift φ) ↑g = φ g
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<GOAL>Function.Injective ⇑(QuotientGroup.kerLift φ)
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<GOAL>Function.Injective ⇑(QuotientAddGroup.kerLift φ)
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<GOAL>Function.Injective ⇑(QuotientAddGroup.rangeKerLift φ)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<GOAL>Function.Injective ⇑(QuotientGroup.rangeKerLift φ)
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<GOAL>Function.Surjective ⇑(QuotientAddGroup.rangeKerLift φ)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<GOAL>Function.Surjective ⇑(QuotientGroup.rangeKerLift φ)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<VAR>ψ : H → G<VAR>hφ : Function.RightInverse ψ ⇑φ<GOAL>∀ (a : H), (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientGroup.mk ∘ ψ) a
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<VAR>ψ : H → G<VAR>hφ : Function.RightInverse ψ ⇑φ<GOAL>∀ (a : H), (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientAddGroup.mk ∘ ψ) a
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>φ : G →* H<VAR>ψ : H → G<VAR>hφ : Function.RightInverse ψ ⇑φ<VAR>a : G ⧸ φ.ker<GOAL>(QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientGroup.kerLift φ) a
<VAR>G : Type u<VAR>AddGroup G<VAR>H : Type v<VAR>AddGroup H<VAR>φ : G →+ H<VAR>ψ : H → G<VAR>hφ : Function.RightInverse ψ ⇑φ<VAR>a : G ⧸ φ.ker<GOAL>(QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientAddGroup.kerLift φ) a
<VAR>G : Type u<VAR>AddGroup G<VAR>a : G ⧸ (AddMonoidHom.id G).ker<GOAL>QuotientAddGroup.quotientBot a = (QuotientAddGroup.kerLift (AddMonoidHom.id G)) a
<VAR>G : Type u<VAR>Group G<GOAL>∀ (a : G), QuotientGroup.quotientBot.symm a = ↑a
<VAR>G : Type u<VAR>Group G<VAR>a : G ⧸ (MonoidHom.id G).ker<GOAL>QuotientGroup.quotientBot a = (QuotientGroup.kerLift (MonoidHom.id G)) a
<VAR>G : Type u<VAR>AddGroup G<GOAL>∀ (a : G), QuotientAddGroup.quotientBot.symm a = ↑a
<VAR>G : Type u<VAR>Group G<VAR>M N : Subgroup G<VAR>M.Normal<VAR>N.Normal<VAR>h : M = N<VAR>x : G<GOAL>(QuotientGroup.quotientMulEquivOfEq h) ↑x = ↑x
<VAR>G : Type u<VAR>AddGroup G<VAR>M N : AddSubgroup G<VAR>M.Normal<VAR>N.Normal<VAR>h : M = N<VAR>x : G<GOAL>(QuotientAddGroup.quotientAddEquivOfEq h) ↑x = ↑x
<VAR>G : Type u<VAR>Group G<VAR>A' A B' B : Subgroup G<VAR>_hAN : (A'.subgroupOf A).Normal<VAR>_hBN : (B'.subgroupOf B).Normal<VAR>h' : A' ≤ B'<VAR>h : A ≤ B<VAR>x : ↥A<GOAL>(QuotientGroup.quotientMapSubgroupOfOfLe h' h) ↑x = ↑((Subgroup.inclusion h) x)
<VAR>G : Type u<VAR>AddGroup G<VAR>A' A B' B : AddSubgroup G<VAR>_hAN : (A'.addSubgroupOf A).Normal<VAR>_hBN : (B'.addSubgroupOf B).Normal<VAR>h' : A' ≤ B'<VAR>h : A ≤ B<VAR>x : ↥A<GOAL>(QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h) ↑x = ↑((AddSubgroup.inclusion h) x)
<VAR>A : Type u<VAR>CommGroup A<VAR>n : ℤ<GOAL>QuotientGroup.homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id (A ⧸ (zpowGroupHom n).range)