ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>DecidableEq J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>L₁.HasMapBifunctor L₂ F c<VAR>j : J<GOAL>(HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j = (K₁.mapBifunctor K₂ F c).d j (c.next j) ≫ HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j + HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j (c.prev j) ≫ (L₁.mapBifunctor L₂ F c).d (c.prev j) j + (HomologicalComplex.mapBifunctorMap f₁' f₂ F c).f j
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>self : SMulWithZero R M<VAR>m : M<GOAL>0 • m = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>m : M<GOAL>0 • m = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>a : R<VAR>h : a = 0<VAR>b : M<GOAL>a • b = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>a : R<VAR>b : M<GOAL>a • b ≠ 0 → a ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>self : MulActionWithZero R M<VAR>m : M<GOAL>0 • m = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>self : MulActionWithZero R M<VAR>r : R<GOAL>r • 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>Subsingleton R<GOAL>Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>Nontrivial M<GOAL>Nontrivial R
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>p : Prop<VAR>Decidable p<VAR>a : R<VAR>b : M<GOAL>(if p then a else 0) • b = if p then a • b else 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>p : Prop<VAR>Decidable p<VAR>a : M<GOAL>(if p then 1 else 0) • a = if p then a else 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>x : M<VAR>i j : ι<GOAL>Pi.single i 1 j • x = Pi.single i x j
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>GroupWithZero α<VAR>GroupWithZero β<VAR>MulActionWithZero α β<VAR>SMulCommClass α β β<VAR>IsScalarTower α β β<VAR>c : α<VAR>x : β<GOAL>(c • x)⁻¹ = c⁻¹ • x⁻¹
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MonoidWithZero α<VAR>MulZeroOneClass β<VAR>MulActionWithZero α β<VAR>IsScalarTower α β β<VAR>SMulCommClass α β β<GOAL>∀ (a : α × β), smulMonoidWithZeroHom a = (↑smulMonoidHom).toFun a
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M<GOAL>(finsuppLEquivDirectSum R M ι) (Finsupp.single i m) = (DirectSum.lof R ι (fun i => M) i) m
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M<GOAL>(finsuppLEquivDirectSum R M ι).symm ((DirectSum.lof R ι (fun x => M) i) m) = Finsupp.single i m
<VAR>R : Type u<GOAL>Function.Injective Tropical.trop
<VAR>R : Type u<GOAL>Function.Injective Tropical.untrop
<VAR>R : Type u<VAR>x y : R<GOAL>Tropical.trop x = Tropical.trop y ↔ x = y
<VAR>R : Type u<VAR>x y : Tropical R<GOAL>Tropical.untrop x = Tropical.untrop y ↔ x = y
<VAR>R : Type u<VAR>x : Tropical R<GOAL>Tropical.trop (Tropical.untrop x) = x
<VAR>R : Type u<VAR>x : R<GOAL>Tropical.untrop (Tropical.trop x) = x
<VAR>R : Type u<GOAL>Function.LeftInverse Tropical.trop Tropical.untrop
<VAR>R : Type u<GOAL>Function.RightInverse Tropical.trop Tropical.untrop
<VAR>R : Type u<GOAL>⇑Tropical.tropEquiv = Tropical.trop
<VAR>R : Type u<GOAL>⇑Tropical.tropEquiv.symm = Tropical.untrop
<VAR>R : Type u<VAR>x : R<VAR>y : Tropical R<GOAL>Tropical.trop x = y ↔ x = Tropical.untrop y
<VAR>R : Type u<VAR>x : Tropical R<VAR>y : R<GOAL>Tropical.untrop x = y ↔ x = Tropical.trop y
<VAR>R : Type u<GOAL>Function.Surjective Tropical.trop
<VAR>R : Type u<GOAL>Function.Surjective Tropical.untrop
<VAR>R : Type u<VAR>LE R<VAR>x y : Tropical R<GOAL>Tropical.untrop x ≤ Tropical.untrop y ↔ x ≤ y
<VAR>R : Type u<VAR>LT R<VAR>x y : Tropical R<GOAL>Tropical.untrop x < Tropical.untrop y ↔ x < y
<VAR>R : Type u<VAR>Preorder R<GOAL>⇑Tropical.tropOrderIso = Tropical.trop
<VAR>R : Type u<VAR>Preorder R<GOAL>⇑Tropical.tropOrderIso.symm = Tropical.untrop
<VAR>R : Type u<VAR>Preorder R<GOAL>Monotone Tropical.trop
<VAR>R : Type u<VAR>Preorder R<GOAL>Monotone Tropical.untrop
<VAR>R : Type u<VAR>Top R<GOAL>Tropical.untrop 0 = ⊤
<VAR>R : Type u<VAR>Top R<GOAL>Tropical.trop ⊤ = 0
<VAR>R : Type u<VAR>x : R<GOAL>Tropical.trop ↑x ≠ 0
<VAR>R : Type u<VAR>x : R<GOAL>0 ≠ Tropical.trop ↑x
<VAR>R : Type u<VAR>LE R<VAR>OrderTop R<VAR>x : Tropical R<GOAL>x ≤ 0
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>Tropical.untrop (x + y) = min (Tropical.untrop x) (Tropical.untrop y)
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : R<GOAL>Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : R<GOAL>Tropical.trop (x ⊓ y) = Tropical.trop x + Tropical.trop y
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>x + y = Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y))
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>Tropical.untrop (x ⊔ y) = Tropical.untrop x ⊔ Tropical.untrop y
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)
<VAR>R : Type u<VAR>LinearOrder R<GOAL>min = fun x x_1 => x + x_1
<VAR>R : Type u<VAR>LinearOrder R<GOAL>(fun x x_1 => x ⊓ x_1) = fun x x_1 => x + x_1
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>x ⊔ y = Tropical.trop (Tropical.untrop x ⊔ Tropical.untrop y)
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<VAR>h : x ≤ y<GOAL>x + y = x
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<VAR>h : y ≤ x<GOAL>x + y = y
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>x + y = x ↔ x ≤ y
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y : Tropical R<GOAL>x + y = y ↔ y ≤ x
<VAR>R : Type u<VAR>LinearOrder R<VAR>x : Tropical R<GOAL>x + x = x
<VAR>R : Type u<VAR>LinearOrder R<VAR>x y z : Tropical R<GOAL>x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
<VAR>R : Type u<VAR>LinearOrder R<VAR>a b : Tropical (WithTop R)<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>R : Type u<VAR>Add R<VAR>x y : R<GOAL>Tropical.trop (x + y) = Tropical.trop x * Tropical.trop y
<VAR>R : Type u<VAR>Add R<VAR>x y : Tropical R<GOAL>Tropical.untrop (x * y) = Tropical.untrop x + Tropical.untrop y
<VAR>R : Type u<VAR>Add R<VAR>x y : Tropical R<GOAL>x * y = Tropical.trop (Tropical.untrop x + Tropical.untrop y)
<VAR>R : Type u<VAR>Zero R<GOAL>Tropical.trop 0 = 1
<VAR>R : Type u<VAR>Zero R<GOAL>Tropical.untrop 1 = 0
<VAR>R : Type u<VAR>Neg R<VAR>x : Tropical R<GOAL>Tropical.untrop x⁻¹ = -Tropical.untrop x
<VAR>R : Type u<VAR>Sub R<VAR>x y : Tropical R<GOAL>Tropical.untrop (x / y) = Tropical.untrop x - Tropical.untrop y
<VAR>R : Type u<VAR>α : Type u_1<VAR>SMul α R<VAR>x : Tropical R<VAR>n : α<GOAL>Tropical.untrop (x ^ n) = n • Tropical.untrop x
<VAR>R : Type u<VAR>α : Type u_1<VAR>SMul α R<VAR>x : R<VAR>n : α<GOAL>Tropical.trop (n • x) = Tropical.trop x ^ n
<VAR>R : Type u<VAR>AddMonoid R<VAR>x : R<VAR>n : ℕ<GOAL>Tropical.trop (n • x) = Tropical.trop x ^ n
<VAR>R : Type u<VAR>AddGroup R<VAR>x : Tropical R<VAR>n : ℤ<GOAL>Tropical.untrop (x ^ n) = n • Tropical.untrop x
<VAR>R : Type u<VAR>AddGroup R<VAR>x : R<VAR>n : ℤ<GOAL>Tropical.trop (n • x) = Tropical.trop x ^ n
<VAR>R : Type u<VAR>LinearOrder R<VAR>AddMonoid R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : Tropical R<VAR>n : ℕ<GOAL>(x + y) ^ n = x ^ n + y ^ n
<VAR>R : Type u_1<VAR>LinearOrder R<VAR>OrderTop R<VAR>x : Tropical R<VAR>n : ℕ<GOAL>(n + 1) • x = x
<VAR>R : Type u_1<VAR>LinearOrderedAddCommMonoid R<VAR>a b : Tropical (WithTop R)<GOAL>a * b = 0 ↔ a = 0 ∨ b = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasLimit (F ⋙ HomologicalComplex.eval C c n)<VAR>n m : ι<GOAL>(HomologicalComplex.coneOfHasLimitEval F).pt.d n m = CategoryTheory.Limits.limMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasLimit (F ⋙ HomologicalComplex.eval C c n)<VAR>n : ι<GOAL>(HomologicalComplex.coneOfHasLimitEval F).pt.X n = CategoryTheory.Limits.limit (F ⋙ HomologicalComplex.eval C c n)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasLimit (F ⋙ HomologicalComplex.eval C c n)<VAR>j : J<VAR>n : ι<GOAL>((HomologicalComplex.coneOfHasLimitEval F).π.app j).f n = CategoryTheory.Limits.limit.π (F ⋙ HomologicalComplex.eval C c n) j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasColimit (F ⋙ HomologicalComplex.eval C c n)<VAR>j : J<VAR>n : ι<GOAL>((HomologicalComplex.coconeOfHasColimitEval F).ι.app j).f n = CategoryTheory.Limits.colimit.ι (F ⋙ HomologicalComplex.eval C c n) j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasColimit (F ⋙ HomologicalComplex.eval C c n)<VAR>n m : ι<GOAL>(HomologicalComplex.coconeOfHasColimitEval F).pt.d n m = CategoryTheory.Limits.colimMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_3} J<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>∀ (n : ι), CategoryTheory.Limits.HasColimit (F ⋙ HomologicalComplex.eval C c n)<VAR>n : ι<GOAL>(HomologicalComplex.coconeOfHasColimitEval F).pt.X n = CategoryTheory.Limits.colimit (F ⋙ HomologicalComplex.eval C c n)
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b c : α<GOAL>(a + b) / c = a / c + b / c
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b c : α<GOAL>a / c + b / c = (a + b) / c
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>h : b ≠ 0<GOAL>(b + a) / b = 1 + a / b
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>h : b ≠ 0<GOAL>(a + b) / b = a / b + 1
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>h : b ≠ 0<GOAL>1 + a / b = (b + a) / b
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>h : b ≠ 0<GOAL>a / b + 1 = (a + b) / b
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>c : α<VAR>a b : α<VAR>hc : c ≠ 0<GOAL>a + b / c = (a * c + b) / c
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>b + a / c = (b * c + a) / c
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a / c + b = (a + b * c) / c
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b c d : α<VAR>hbc : Commute b c<VAR>hbd : Commute b d<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b + c / d = (a * d + b * c) / (b * d)
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>hab : Commute a b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a + 1 / b = (a + b) / (a * b)
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a b : α<VAR>hab : Commute a b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ + b⁻¹ = (a + b) / (a * b)
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<GOAL>1 / -1 = -1
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a : K<GOAL>1 / -a = -(1 / a)
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a b : K<GOAL>b / -a = -(b / a)
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a b : K<GOAL>-b / a = -(b / a)
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a b : K<GOAL>-(b / a) = -b / a
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a b : K<GOAL>-a / -b = a / b
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a : K<GOAL>-a⁻¹ = (-a)⁻¹
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>b : K<VAR>a : K<GOAL>a / -b = -(a / b)
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<VAR>a : K<GOAL>(-a)⁻¹ = -a⁻¹
<VAR>K : Type u_3<VAR>DivisionMonoid K<VAR>HasDistribNeg K<GOAL>(-1)⁻¹ = -1
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a : K<VAR>h : a ≠ 0<GOAL>a / -a = -1
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a : K<VAR>h : a ≠ 0<GOAL>-a / a = -1
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b c : K<GOAL>a / c - b / c = (a - b) / c
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>h : b ≠ 0<GOAL>(b - a) / b = 1 - a / b
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>h : b ≠ 0<GOAL>1 - a / b = (b - a) / b
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>h : b ≠ 0<GOAL>(a - b) / b = a / b - 1
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>h : b ≠ 0<GOAL>a / b - 1 = (a - b) / b
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b c : K<GOAL>(a - b) / c = a / c - b / c
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b c d : K<VAR>hbc : Commute b c<VAR>hbd : Commute b d<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b - c / d = (a * d - b * c) / (b * d)
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a b : K<VAR>hab : Commute a b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ - b⁻¹ = (b - a) / (a * b)
<VAR>α : Type u_1<VAR>Semifield α<VAR>b d : α<VAR>a c : α<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b + c / d = (a * d + b * c) / (b * d)
<VAR>α : Type u_1<VAR>Semifield α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a + 1 / b = (a + b) / (a * b)
<VAR>α : Type u_1<VAR>Semifield α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ + b⁻¹ = (a + b) / (a * b)
<VAR>K : Type u_3<VAR>Field K<VAR>a : K<VAR>b : K<VAR>c : K<VAR>d : K<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b - c / d = (a * d - b * c) / (b * d)
<VAR>K : Type u_3<VAR>Field K<VAR>a b : K<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ - b⁻¹ = (b - a) / (a * b)
<VAR>K : Type u_3<VAR>Field K<VAR>a b c : K<VAR>hc : c ≠ 0<GOAL>b - a / c = (b * c - a) / c
<VAR>K : Type u_3<VAR>Field K<VAR>a b c : K<VAR>hc : c ≠ 0<GOAL>a / c - b = (a - c * b) / c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DivisionRing α<VAR>Semiring β<VAR>Nontrivial β<VAR>f : α →+* β<GOAL>Function.Injective ⇑f
<VAR>α : Type u_1<VAR>RatCast α<VAR>n : ℚ<GOAL>OrderDual.toDual ↑n = ↑n
<VAR>α : Type u_1<VAR>RatCast α<VAR>n : ℚ<GOAL>OrderDual.ofDual ↑n = ↑n
<VAR>α : Type u_1<VAR>RatCast α<VAR>n : ℚ<GOAL>toLex ↑n = ↑n
<VAR>α : Type u_1<VAR>RatCast α<VAR>n : ℚ<GOAL>ofLex ↑n = ↑n
<VAR>G : outParam (Type u_1)<VAR>P : Type u_2<VAR>AddGroup G<VAR>self : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ p₂ +ᵥ p₂ = p₁
<VAR>G : outParam (Type u_1)<VAR>P : Type u_2<VAR>AddGroup G<VAR>self : AddTorsor G P<VAR>g : G<VAR>p : P<GOAL>g +ᵥ p -ᵥ p = g
<VAR>G : outParam (Type u_1)<VAR>P : Type u_2<VAR>AddGroup G<VAR>self : AddTorsor G P<GOAL>Nonempty P
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g₁ g₂ : G<GOAL>g₁ -ᵥ g₂ = g₁ - g₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ p₂ +ᵥ p₂ = p₁
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p : P<GOAL>g +ᵥ p -ᵥ p = g
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>g₁ g₂ : G<VAR>p : P<VAR>h : g₁ +ᵥ p = g₂ +ᵥ p<GOAL>g₁ = g₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>g₁ g₂ : G<VAR>p : P<GOAL>g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>Function.Injective fun x => x +ᵥ p
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p₁ p₂ : P<GOAL>g +ᵥ p₁ -ᵥ p₂ = g + (p₁ -ᵥ p₂)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>p -ᵥ p = 0
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<VAR>h : p₁ -ᵥ p₂ = 0<GOAL>p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p q : P<GOAL>p -ᵥ q ≠ 0 ↔ p ≠ q
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>-(p₁ -ᵥ p₂) = p₂ -ᵥ p₁
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p q : P<GOAL>g +ᵥ p -ᵥ q = g - (q -ᵥ p)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<VAR>g : G<GOAL>p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ : P<VAR>g : G<VAR>p₂ : P<GOAL>p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>v₁ v₂ : G<VAR>p₁ p₂ : P<GOAL>v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>{p} -ᵥ {p} = {0}
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>v₁ v₂ : G<VAR>p : P<GOAL>v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<VAR>h : p₁ -ᵥ p = p₂ -ᵥ p<GOAL>p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<GOAL>p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>Function.Injective fun x => x -ᵥ p
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<VAR>h : p -ᵥ p₁ = p -ᵥ p₂<GOAL>p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<GOAL>p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>Function.Injective fun x => p -ᵥ x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>v : G<VAR>p₁ p₂ : P<GOAL>v +ᵥ p₁ -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ +ᵥ p₃ = p₃ -ᵥ p₂ +ᵥ p₁
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>v₁ v₂ : G<VAR>p₁ p₂ : P<GOAL>v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>v : G × G'<VAR>p : P × P'<GOAL>(v +ᵥ p).1 = v.1 +ᵥ p.1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>v : G × G'<VAR>p : P × P'<GOAL>(v +ᵥ p).2 = v.2 +ᵥ p.2
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>v : G<VAR>v' : G'<VAR>p : P<VAR>p' : P'<GOAL>(v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>p₁ p₂ : P × P'<GOAL>(p₁ -ᵥ p₂).1 = p₁.1 -ᵥ p₂.1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>p₁ p₂ : P × P'<GOAL>(p₁ -ᵥ p₂).2 = p₁.2 -ᵥ p₂.2
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>P : Type u_3<VAR>P' : Type u_4<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddTorsor G P<VAR>AddTorsor G' P'<VAR>p₁ p₂ : P<VAR>p₁' p₂' : P'<GOAL>(p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>p : P<GOAL>⇑(Equiv.vaddConst p) = fun v => v +ᵥ p
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>p : P<GOAL>⇑(Equiv.vaddConst p).symm = fun p' => p' -ᵥ p
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>p : P<GOAL>⇑(Equiv.constVSub p) = fun x => p -ᵥ x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>p : P<GOAL>⇑(Equiv.constVSub p).symm = fun v => -v +ᵥ p
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>v : G<GOAL>⇑(Equiv.constVAdd P v) = fun x => v +ᵥ x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<GOAL>Equiv.constVAdd P 0 = 1
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>v₁ v₂ : G<GOAL>Equiv.constVAdd P (v₁ + v₂) = Equiv.constVAdd P v₁ * Equiv.constVAdd P v₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<GOAL>(Equiv.pointReflection x) y = x -ᵥ y +ᵥ x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<GOAL>(Equiv.pointReflection x) y -ᵥ x = x -ᵥ y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<GOAL>x -ᵥ (Equiv.pointReflection x) y = y -ᵥ x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<GOAL>(Equiv.pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<GOAL>y -ᵥ (Equiv.pointReflection x) y = 2 • (y -ᵥ x)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x : P<GOAL>Equiv.symm (Equiv.pointReflection x) = Equiv.pointReflection x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x : P<GOAL>(Equiv.pointReflection x) x = x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x : P<GOAL>Function.Involutive ⇑(Equiv.pointReflection x)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>x y : P<VAR>h : Function.Injective fun x => 2 • x<GOAL>(Equiv.pointReflection x) y = y ↔ y = x
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup G<VAR>AddTorsor G P<VAR>h : Function.Injective fun x => 2 • x<VAR>y : P<GOAL>Function.Injective fun x => (Equiv.pointReflection x) y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<GOAL>Subsingleton G ↔ Subsingleton P