ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>FreeGroup.Red L L
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₃ → FreeAddGroup.Red L₁ L₃
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeAddGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeAddGroup.Red.Step ((x, b) :: (x, !b) :: L) L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeAddGroup.Red.Step ((x, !b) :: (x, b) :: L) L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeGroup.Red.Step ((x, !b) :: (x, b) :: L) L
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₂ L₃ → FreeAddGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₂ L₃ → FreeGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x : α × Bool<VAR>H : FreeAddGroup.Red.Step L₁ L₂<GOAL>FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x : α × Bool<VAR>H : FreeGroup.Red.Step L₁ L₂<GOAL>FreeGroup.Red.Step (x :: L₁) (x :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>¬FreeGroup.Red.Step [] L
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>¬FreeAddGroup.Red.Step [] L
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>a : α<VAR>b : Bool<GOAL>FreeAddGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ L, FreeAddGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>a : α<VAR>b : Bool<GOAL>FreeGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ L, FreeGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>p : α × Bool<GOAL>¬FreeGroup.Red.Step [p] L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>p : α × Bool<GOAL>¬FreeAddGroup.Red.Step [p] L
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeAddGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>L : List (α × Bool)<GOAL>FreeGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>L : List (α × Bool)<GOAL>FreeAddGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<GOAL>L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, FreeAddGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeAddGroup.Red.Step (L₃ ++ L₄) L₅
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<GOAL>L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, FreeGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeGroup.Red.Step (L₃ ++ L₄) L₅
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₁ L₃ → FreeAddGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ L₅, FreeAddGroup.Red.Step L₃ L₅ ∧ FreeAddGroup.Red.Step L₄ L₅
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₁ L₃ → FreeGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ L₅, FreeGroup.Red.Step L₃ L₅ ∧ FreeGroup.Red.Step L₄ L₅
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → Relation.Join FreeAddGroup.Red L₂ L₃
<VAR>α : Type u<VAR>L₁ L₂ L₃ : List (α × Bool)<GOAL>FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → Relation.Join FreeGroup.Red L₂ L₃
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (p :: L₁) (p :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeAddGroup.Red (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>p : α × Bool<GOAL>FreeGroup.Red (p :: L₁) (p :: L₂) ↔ FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>L : List (α × Bool)<GOAL>FreeAddGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>L : List (α × Bool)<GOAL>FreeGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>h₁ : FreeGroup.Red L₁ L₃<VAR>h₂ : FreeGroup.Red L₂ L₄<GOAL>FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
<VAR>α : Type u<VAR>L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>h₁ : FreeAddGroup.Red L₁ L₃<VAR>h₂ : FreeAddGroup.Red L₂ L₄<GOAL>FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
<VAR>α : Type u<VAR>L L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂
<VAR>α : Type u<VAR>L L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ FreeGroup.Red L₃ L₁ ∧ FreeGroup.Red L₄ L₂
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>FreeAddGroup.Red [] L ↔ L = []
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>FreeGroup.Red [] L ↔ L = []
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>x : α × Bool<GOAL>FreeAddGroup.Red [x] L₁ ↔ L₁ = [x]
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<VAR>x : α × Bool<GOAL>FreeGroup.Red [x] L₁ ↔ L₁ = [x]
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeAddGroup.Red ((x, b) :: L) [] ↔ FreeAddGroup.Red L [(x, !b)]
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeGroup.Red ((x, b) :: L) [] ↔ FreeGroup.Red L [(x, !b)]
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<GOAL>FreeAddGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>h : (x1, b1) ≠ (x2, b2)<GOAL>FreeGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>H1 : (x1, b1) ≠ (x2, b2)<VAR>H2 : FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)<GOAL>FreeAddGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>H1 : (x1, b1) ≠ (x2, b2)<VAR>H2 : FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)<GOAL>FreeGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>H : FreeAddGroup.Red.Step L₁ L₂<GOAL>L₂.Sublist L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>H : FreeGroup.Red.Step L₁ L₂<GOAL>L₂.Sublist L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red L₁ L₂ → L₂.Sublist L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red L₁ L₂ → L₂.Sublist L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeGroup.Red L₁ L₂<GOAL>L₂.length ≤ L₁.length
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeAddGroup.Red L₁ L₂<GOAL>L₂.length ≤ L₁.length
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeAddGroup.Red L₁ L₂<GOAL>∃ n, L₁.length = L₂.length + 2 * n
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeGroup.Red L₁ L₂<GOAL>∃ n, L₁.length = L₂.length + 2 * n
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h₁₂ : FreeAddGroup.Red L₁ L₂<VAR>h₂₁ : FreeAddGroup.Red L₂ L₁<GOAL>L₁ = L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h₁₂ : FreeGroup.Red L₁ L₂<VAR>h₂₁ : FreeGroup.Red L₂ L₁<GOAL>L₁ = L₂
<VAR>α : Type u<GOAL>Equivalence (Relation.Join FreeGroup.Red)
<VAR>α : Type u<GOAL>Equivalence (Relation.Join FreeAddGroup.Red)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeGroup.Red.Step L₁ L₂<GOAL>Relation.Join FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeAddGroup.Red.Step L₁ L₂<GOAL>Relation.Join FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>EqvGen FreeAddGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>EqvGen FreeGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>Quot.mk FreeAddGroup.Red.Step L = FreeAddGroup.mk L
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>Quot.mk FreeGroup.Red.Step L = FreeGroup.mk L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → β<VAR>H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂<GOAL>Quot.lift f H (FreeAddGroup.mk L) = f L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → β<VAR>H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂<GOAL>Quot.lift f H (FreeGroup.mk L) = f L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → β<VAR>H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂<GOAL>Quot.liftOn (FreeGroup.mk L) f H = f L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → β<VAR>H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂<GOAL>Quot.liftOn (FreeAddGroup.mk L) f H = f L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → List (β × Bool)<VAR>H : (FreeGroup.Red.Step ⇒ FreeGroup.Red.Step) f f<GOAL>Quot.map f H (FreeGroup.mk L) = FreeGroup.mk (f L)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : List (α × Bool) → List (β × Bool)<VAR>H : (FreeAddGroup.Red.Step ⇒ FreeAddGroup.Red.Step) f f<GOAL>Quot.map f H (FreeAddGroup.mk L) = FreeAddGroup.mk (f L)
<VAR>α : Type u<GOAL>1 = FreeGroup.mk []
<VAR>α : Type u<GOAL>0 = FreeAddGroup.mk []
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.mk L₁ + FreeAddGroup.mk L₂ = FreeAddGroup.mk (L₁ ++ L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<GOAL>(FreeAddGroup.negRev L₁).length = L₁.length
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<GOAL>(FreeGroup.invRev L₁).length = L₁.length
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<GOAL>FreeGroup.invRev (FreeGroup.invRev L₁) = L₁
<VAR>α : Type u<VAR>L₁ : List (α × Bool)<GOAL>FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁
<VAR>α : Type u<GOAL>FreeGroup.invRev [] = []
<VAR>α : Type u<GOAL>FreeAddGroup.negRev [] = []
<VAR>α : Type u<GOAL>Function.Involutive FreeAddGroup.negRev
<VAR>α : Type u<GOAL>Function.Involutive FreeGroup.invRev
<VAR>α : Type u<GOAL>Function.Injective FreeGroup.invRev
<VAR>α : Type u<GOAL>Function.Injective FreeAddGroup.negRev
<VAR>α : Type u<GOAL>Function.Surjective FreeAddGroup.negRev
<VAR>α : Type u<GOAL>Function.Surjective FreeGroup.invRev
<VAR>α : Type u<GOAL>Function.Bijective FreeAddGroup.negRev
<VAR>α : Type u<GOAL>Function.Bijective FreeGroup.invRev
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>(FreeGroup.mk L)⁻¹ = FreeGroup.mk (FreeGroup.invRev L)
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>-FreeAddGroup.mk L = FreeAddGroup.mk (FreeAddGroup.negRev L)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeGroup.Red.Step L₁ L₂<GOAL>FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeAddGroup.Red.Step L₁ L₂<GOAL>FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeAddGroup.Red L₁ L₂<GOAL>FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>h : FreeGroup.Red L₁ L₂<GOAL>FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red.Step L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<GOAL>FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
<VAR>α : Type u<GOAL>Function.Injective FreeAddGroup.of
<VAR>α : Type u<GOAL>Function.Injective FreeGroup.of
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<VAR>H : FreeAddGroup.Red.Step L₁ L₂<GOAL>FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>β : Type v<VAR>Group β<VAR>f : α → β<VAR>H : FreeGroup.Red.Step L₁ L₂<GOAL>FreeGroup.Lift.aux f L₁ = FreeGroup.Lift.aux f L₂
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>g : FreeGroup α →* β<GOAL>∀ (a : α), FreeGroup.lift.symm g a = (⇑g ∘ FreeGroup.of) a
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>g : FreeAddGroup α →+ β<GOAL>∀ (a : α), FreeAddGroup.lift.symm g a = (⇑g ∘ FreeAddGroup.of) a
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<GOAL>(FreeAddGroup.lift f) (FreeAddGroup.mk L) = (List.map (fun x => bif x.2 then f x.1 else -f x.1) L).sum
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>Group β<VAR>f : α → β<GOAL>(FreeGroup.lift f) (FreeGroup.mk L) = (List.map (fun x => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>f : α → β<VAR>x : α<GOAL>(FreeGroup.lift f) (FreeGroup.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddGroup.lift f) (FreeAddGroup.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<VAR>g : FreeAddGroup α →+ β<VAR>hg : ∀ (x : α), g (FreeAddGroup.of x) = f x<VAR>x : FreeAddGroup α<GOAL>g x = (FreeAddGroup.lift f) x
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>f : α → β<VAR>g : FreeGroup α →* β<VAR>hg : ∀ (x : α), g (FreeGroup.of x) = f x<VAR>x : FreeGroup α<GOAL>g x = (FreeGroup.lift f) x
<VAR>α : Type u<VAR>G : Type u_1<VAR>Group G<VAR>f g : FreeGroup α →* G<VAR>h : ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)<GOAL>f = g
<VAR>α : Type u<VAR>G : Type u_1<VAR>AddGroup G<VAR>f g : FreeAddGroup α →+ G<VAR>h : ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)<GOAL>f = g
<VAR>α : Type u_1<GOAL>FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)
<VAR>α : Type u_1<GOAL>FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)
<VAR>α : Type u<VAR>x : FreeGroup α<GOAL>(FreeGroup.lift FreeGroup.of) x = x
<VAR>α : Type u<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.lift FreeAddGroup.of) x = x
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>f : α → β<VAR>s : Subgroup β<VAR>H : Set.range f ⊆ ↑s<GOAL>(FreeGroup.lift f).range ≤ s
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<VAR>s : AddSubgroup β<VAR>H : Set.range f ⊆ ↑s<GOAL>(FreeAddGroup.lift f).range ≤ s
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>f : α → β<GOAL>(FreeGroup.lift f).range = Subgroup.closure (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<GOAL>(FreeAddGroup.lift f).range = AddSubgroup.closure (Set.range f)
<VAR>α : Type u_1<GOAL>Subgroup.closure (Set.range FreeGroup.of) = ⊤
<VAR>α : Type u_1<GOAL>AddSubgroup.closure (Set.range FreeAddGroup.of) = ⊤
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : α → β<GOAL>(FreeGroup.map f) (FreeGroup.mk L) = FreeGroup.mk (List.map (fun x => (f x.1, x.2)) L)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>β : Type v<VAR>f : α → β<GOAL>(FreeAddGroup.map f) (FreeAddGroup.mk L) = FreeAddGroup.mk (List.map (fun x => (f x.1, x.2)) L)
<VAR>α : Type u<VAR>x : FreeGroup α<GOAL>(FreeGroup.map id) x = x
<VAR>α : Type u<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.map id) x = x
<VAR>α : Type u<VAR>x : FreeGroup α<GOAL>(FreeGroup.map fun z => z) x = x
<VAR>α : Type u<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.map fun z => z) x = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.map g) ((FreeAddGroup.map f) x) = (FreeAddGroup.map (g ∘ f)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeGroup α<GOAL>(FreeGroup.map g) ((FreeGroup.map f) x) = (FreeGroup.map (g ∘ f)) x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeAddGroup.map f) (FreeAddGroup.of x) = FreeAddGroup.of (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeGroup.map f) (FreeGroup.of x) = FreeGroup.of (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : FreeAddGroup α →+ FreeAddGroup β<VAR>hg : ∀ (x : α), g (FreeAddGroup.of x) = FreeAddGroup.of (f x)<VAR>x : FreeAddGroup α<GOAL>g x = (FreeAddGroup.map f) x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : FreeGroup α →* FreeGroup β<VAR>hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)<VAR>x : FreeGroup α<GOAL>g x = (FreeGroup.map f) x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>(FreeGroup.map f) x = (FreeGroup.lift (FreeGroup.of ∘ f)) x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.map f) x = (FreeAddGroup.lift (FreeAddGroup.of ∘ f)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>a : FreeGroup α<GOAL>(FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>a : FreeAddGroup α<GOAL>(FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.map ⇑e) a
<VAR>α : Type u<GOAL>FreeAddGroup.freeAddGroupCongr (Equiv.refl α) = AddEquiv.refl (FreeAddGroup α)
<VAR>α : Type u<GOAL>FreeGroup.freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>(FreeAddGroup.freeAddGroupCongr e).symm = FreeAddGroup.freeAddGroupCongr e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>(FreeGroup.freeGroupCongr e).symm = FreeGroup.freeGroupCongr e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f : β ≃ γ<GOAL>(FreeAddGroup.freeAddGroupCongr e).trans (FreeAddGroup.freeAddGroupCongr f) = FreeAddGroup.freeAddGroupCongr (e.trans f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f : β ≃ γ<GOAL>(FreeGroup.freeGroupCongr e).trans (FreeGroup.freeGroupCongr f) = FreeGroup.freeGroupCongr (e.trans f)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>AddGroup α<GOAL>FreeAddGroup.sum (FreeAddGroup.mk L) = (List.map (fun x => bif x.2 then x.1 else -x.1) L).sum
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>Group α<GOAL>FreeGroup.prod (FreeGroup.mk L) = (List.map (fun x => bif x.2 then x.1 else x.1⁻¹) L).prod
<VAR>α : Type u<VAR>Group α<VAR>x : α<GOAL>FreeGroup.prod (FreeGroup.of x) = x
<VAR>α : Type u<VAR>AddGroup α<VAR>x : α<GOAL>FreeAddGroup.sum (FreeAddGroup.of x) = x
<VAR>α : Type u<VAR>Group α<VAR>g : FreeGroup α →* α<VAR>hg : ∀ (x : α), g (FreeGroup.of x) = x<VAR>x : FreeGroup α<GOAL>g x = FreeGroup.prod x
<VAR>α : Type u<VAR>AddGroup α<VAR>g : FreeAddGroup α →+ α<VAR>hg : ∀ (x : α), g (FreeAddGroup.of x) = x<VAR>x : FreeAddGroup α<GOAL>g x = FreeAddGroup.sum x
<VAR>α : Type u<VAR>β : Type v<VAR>Group β<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>(FreeGroup.lift f) x = FreeGroup.prod ((FreeGroup.map f) x)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f : α → β<VAR>x : FreeAddGroup α<GOAL>(FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>AddGroup α<GOAL>(FreeGroup.mk L).sum = (List.map (fun x => bif x.2 then x.1 else -x.1) L).sum
<VAR>α : Type u<VAR>AddGroup α<VAR>x : α<GOAL>(FreeGroup.of x).sum = x
<VAR>α : Type u<VAR>AddGroup α<VAR>x y : FreeGroup α<GOAL>(x * y).sum = x.sum + y.sum
<VAR>α : Type u<VAR>AddGroup α<GOAL>FreeGroup.sum 1 = 0
<VAR>α : Type u<VAR>AddGroup α<VAR>x : FreeGroup α<GOAL>x⁻¹.sum = -x.sum
<VAR>α : Type u<VAR>C : FreeAddGroup α → Prop<VAR>z : FreeAddGroup α<VAR>C1 : C 0<VAR>Cp : ∀ (x : α), C (pure x)<VAR>Ci : ∀ (x : α), C (pure x) → C (-pure x)<VAR>Cm : ∀ (x y : FreeAddGroup α), C x → C y → C (x + y)<GOAL>C z
<VAR>α : Type u<VAR>C : FreeGroup α → Prop<VAR>z : FreeGroup α<VAR>C1 : C 1<VAR>Cp : ∀ (x : α), C (pure x)<VAR>Ci : ∀ (x : α), C (pure x) → C (pure x)⁻¹<VAR>Cm : ∀ (x y : FreeGroup α), C x → C y → C (x * y)<GOAL>C z
<VAR>α β : Type u<VAR>f : α → β<GOAL>f <$> 1 = 1
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeAddGroup α<GOAL>f <$> (x + y) = f <$> x + f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeGroup α<GOAL>f <$> (x * y) = f <$> x * f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAddGroup α<GOAL>f <$> (-x) = -f <$> x
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>f <$> x⁻¹ = (f <$> x)⁻¹
<VAR>α β : Type u<VAR>f : α → FreeAddGroup β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeGroup β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeAddGroup β<GOAL>0 >>= f = 0
<VAR>α β : Type u<VAR>f : α → FreeGroup β<GOAL>1 >>= f = 1
<VAR>α β : Type u<VAR>f : α → FreeAddGroup β<VAR>x y : FreeAddGroup α<GOAL>x + y >>= f = (x >>= f) + (y >>= f)
<VAR>α β : Type u<VAR>f : α → FreeGroup β<VAR>x y : FreeGroup α<GOAL>x * y >>= f = (x >>= f) * (y >>= f)
<VAR>α β : Type u<VAR>f : α → FreeAddGroup β<VAR>x : FreeAddGroup α<GOAL>-x >>= f = -(x >>= f)
<VAR>α β : Type u<VAR>f : α → FreeGroup β<VAR>x : FreeGroup α<GOAL>x⁻¹ >>= f = (x >>= f)⁻¹
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<VAR>x : α × Bool<GOAL>FreeAddGroup.reduce (x :: L) = List.casesOn (FreeAddGroup.reduce L) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<VAR>x : α × Bool<GOAL>FreeGroup.reduce (x :: L) = List.casesOn (FreeGroup.reduce L) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeGroup.Red L (FreeGroup.reduce L)
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeAddGroup.Red L (FreeAddGroup.reduce L)
<VAR>α : Type u<VAR>DecidableEq α<VAR>p : Prop<VAR>L₁ L₂ L₃ : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p
<VAR>α : Type u<VAR>DecidableEq α<VAR>p : Prop<VAR>L₁ L₂ L₃ : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.Red (FreeGroup.reduce L₁) L₂<GOAL>FreeGroup.reduce L₁ = L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂<GOAL>FreeAddGroup.reduce L₁ = L₂
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeGroup.reduce (FreeGroup.reduce L) = FreeGroup.reduce L
<VAR>α : Type u<VAR>L : List (α × Bool)<VAR>DecidableEq α<GOAL>FreeAddGroup.reduce (FreeAddGroup.reduce L) = FreeAddGroup.reduce L
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeGroup.Red.Step L₁ L₂<GOAL>FreeGroup.reduce L₁ = FreeGroup.reduce L₂
<VAR>α : Type u<VAR>L₁ L₂ : List (α × Bool)<VAR>DecidableEq α<VAR>H : FreeAddGroup.Red.Step L₁ L₂<GOAL>FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂