ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → SetTheory.Game<GOAL>BddBelow (Set.range f)
<VAR>s : Set SetTheory.Game<VAR>Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>a : SetTheory.PGame<GOAL>⟦-a⟧ = -⟦a⟧
<VAR>a b : SetTheory.PGame<GOAL>⟦a + b⟧ = ⟦a⟧ + ⟦b⟧
<VAR>a b : SetTheory.PGame<GOAL>⟦a - b⟧ = ⟦a⟧ - ⟦b⟧
<VAR>x y : SetTheory.PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), ⟦x.moveLeft i⟧ = ⟦y.moveLeft (L i)⟧<VAR>hr : ∀ (j : x.RightMoves), ⟦x.moveRight j⟧ = ⟦y.moveRight (R j)⟧<GOAL>⟦x⟧ = ⟦y⟧
<VAR>x y : SetTheory.PGame<GOAL>(x * y).LeftMoves = (x.LeftMoves × y.LeftMoves ⊕ x.RightMoves × y.RightMoves)
<VAR>x y : SetTheory.PGame<GOAL>(x * y).RightMoves = (x.LeftMoves × y.RightMoves ⊕ x.RightMoves × y.LeftMoves)
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xl<VAR>j : yl<GOAL>(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inl (i, j)) = xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xL i * yL j
<VAR>x y : SetTheory.PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>(x * y).moveLeft (SetTheory.PGame.toLeftMovesMul (Sum.inl (i, j))) = x.moveLeft i * y + x * y.moveLeft j - x.moveLeft i * y.moveLeft j
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xr<VAR>j : yr<GOAL>(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inr (i, j)) = xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xR i * yR j
<VAR>x y : SetTheory.PGame<VAR>i : x.RightMoves<VAR>j : y.RightMoves<GOAL>(x * y).moveLeft (SetTheory.PGame.toLeftMovesMul (Sum.inr (i, j))) = x.moveRight i * y + x * y.moveRight j - x.moveRight i * y.moveRight j
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xl<VAR>j : yr<GOAL>(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inl (i, j)) = xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xL i * yR j
<VAR>x y : SetTheory.PGame<VAR>i : x.LeftMoves<VAR>j : y.RightMoves<GOAL>(x * y).moveRight (SetTheory.PGame.toRightMovesMul (Sum.inl (i, j))) = x.moveLeft i * y + x * y.moveRight j - x.moveLeft i * y.moveRight j
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xr<VAR>j : yl<GOAL>(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inr (i, j)) = xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xR i * yL j
<VAR>x y : SetTheory.PGame<VAR>i : x.RightMoves<VAR>j : y.LeftMoves<GOAL>(x * y).moveRight (SetTheory.PGame.toRightMovesMul (Sum.inr (i, j))) = x.moveRight i * y + x * y.moveLeft j - x.moveRight i * y.moveLeft j
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xl<VAR>j : yr<GOAL>(-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)).moveLeft (Sum.inl (i, j)) = -(xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xL i * yR j)
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xr<VAR>j : yl<GOAL>(-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)).moveLeft (Sum.inr (i, j)) = -(xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xR i * yL j)
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xl<VAR>j : yl<GOAL>(-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)).moveRight (Sum.inl (i, j)) = -(xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xL i * yL j)
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xr<VAR>j : yr<GOAL>(-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)).moveRight (Sum.inr (i, j)) = -(xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xR i * yR j)
<VAR>x y : SetTheory.PGame<VAR>k : (x * y).LeftMoves<VAR>P : (x * y).LeftMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (SetTheory.PGame.toLeftMovesMul (Sum.inl (ix, iy)))<VAR>hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (SetTheory.PGame.toLeftMovesMul (Sum.inr (jx, jy)))<GOAL>P k
<VAR>x y : SetTheory.PGame<VAR>k : (x * y).RightMoves<VAR>P : (x * y).RightMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (SetTheory.PGame.toRightMovesMul (Sum.inl (ix, jy)))<VAR>hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (SetTheory.PGame.toRightMovesMul (Sum.inr (jx, iy)))<GOAL>P k
<VAR>x y : SetTheory.PGame<GOAL>⟦x * y⟧ = ⟦y * x⟧
<VAR>x y : SetTheory.PGame<GOAL>x * y ≈ y * x
<VAR>x : SetTheory.PGame<GOAL>x * 0 ≈ 0
<VAR>x : SetTheory.PGame<GOAL>⟦x * 0⟧ = ⟦0⟧
<VAR>x : SetTheory.PGame<GOAL>0 * x ≈ 0
<VAR>x : SetTheory.PGame<GOAL>⟦0 * x⟧ = ⟦0⟧
<VAR>x y : SetTheory.PGame<GOAL>⟦-x * y⟧ = -⟦x * y⟧
<VAR>x y : SetTheory.PGame<GOAL>⟦x * -y⟧ = -⟦x * y⟧
<VAR>x y : SetTheory.PGame<GOAL>⟦-x * -y⟧ = ⟦x * y⟧
<VAR>x y z : SetTheory.PGame<GOAL>⟦x * (y + z)⟧ = ⟦x * y⟧ + ⟦x * z⟧
<VAR>x y z : SetTheory.PGame<GOAL>x * (y + z) ≈ x * y + x * z
<VAR>x y z : SetTheory.PGame<GOAL>⟦x * (y - z)⟧ = ⟦x * y⟧ - ⟦x * z⟧
<VAR>x y z : SetTheory.PGame<GOAL>⟦(x + y) * z⟧ = ⟦x * z⟧ + ⟦y * z⟧
<VAR>x y z : SetTheory.PGame<GOAL>(x + y) * z ≈ x * z + y * z
<VAR>x y z : SetTheory.PGame<GOAL>⟦(y - z) * x⟧ = ⟦y * x⟧ - ⟦z * x⟧
<VAR>x : SetTheory.PGame<GOAL>⟦x * 1⟧ = ⟦x⟧
<VAR>x : SetTheory.PGame<GOAL>x * 1 ≈ x
<VAR>x : SetTheory.PGame<GOAL>⟦1 * x⟧ = ⟦x⟧
<VAR>x : SetTheory.PGame<GOAL>1 * x ≈ x
<VAR>x y z : SetTheory.PGame<GOAL>⟦x * y * z⟧ = ⟦x * (y * z)⟧
<VAR>x y z : SetTheory.PGame<GOAL>x * y * z ≈ x * (y * z)
<VAR>x : SetTheory.PGame<VAR>y : SetTheory.PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>x.mulOption y i j = x.mulOption (- -y) i (SetTheory.PGame.toLeftMovesNeg (SetTheory.PGame.toRightMovesNeg j))
<VAR>x y : SetTheory.PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.mulOption y i j⟧ = ⟦y.mulOption x j i⟧
<VAR>x y : SetTheory.PGame<VAR>P : SetTheory.Game → Prop<GOAL>(∀ (k : (x * y).LeftMoves), P ⟦(x * y).moveLeft k⟧) ↔ (∀ (i : x.LeftMoves) (j : y.LeftMoves), P ⟦x.mulOption y i j⟧) ∧ ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), P ⟦(-x).mulOption (-y) i j⟧
<VAR>x y : SetTheory.PGame<VAR>P : SetTheory.Game → Prop<GOAL>(∀ (k : (x * y).RightMoves), P ⟦(x * y).moveRight k⟧) ↔ (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), P (-⟦x.mulOption (-y) i j⟧)) ∧ ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), P (-⟦(-x).mulOption y i j⟧)
<VAR>l r : Type u<VAR>b : Bool<VAR>L : l → SetTheory.PGame<VAR>R : r → SetTheory.PGame<VAR>IHl : l → SetTheory.PGame<VAR>IHr : r → SetTheory.PGame<VAR>i : SetTheory.PGame.InvTy l r b<VAR>x : SetTheory.PGame<VAR>IsEmpty l<VAR>IsEmpty r<GOAL>SetTheory.PGame.invVal L R IHl IHr x i = 0
<VAR>x : SetTheory.PGame<GOAL>SetTheory.PGame.LF 0 x.inv'
<GOAL>SetTheory.PGame.inv' 0 ≈ 1
<GOAL>SetTheory.PGame.inv' 1 ≈ 1
<VAR>x : SetTheory.PGame<VAR>h : x ≈ 0<GOAL>x⁻¹ = 0
<VAR>x : SetTheory.PGame<VAR>h : 0 < x<GOAL>x⁻¹ = x.inv'
<VAR>x : SetTheory.PGame<VAR>h : x.LF 0<GOAL>x⁻¹ = -(-x).inv'
<VAR>α : Sort u_1<VAR>a c b : α<VAR>hab : a ≠ c<VAR>hbc : a = b<GOAL>b ≠ c
<VAR>A : Type u_1<VAR>a b : A<VAR>PartialOrder A<GOAL>a ≤ b → b ≠ a → a < b
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>StrictOrderedSemiring A<VAR>h : Mathlib.Meta.NormNum.IsNat e n<VAR>w : Nat.ble 1 n = true<GOAL>0 < e
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>OrderedSemiring A<VAR>h : Mathlib.Meta.NormNum.IsNat e n<GOAL>0 ≤ e
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>StrictOrderedRing A<VAR>h : Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.ble 1 n = true<GOAL>e ≠ 0
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>LinearOrderedRing A<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (0 < n) = true → 0 < e
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>LinearOrderedRing A<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (n = 0) = true → 0 ≤ e
<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>LinearOrderedRing A<GOAL>Mathlib.Meta.NormNum.IsRat e n d → decide (n < 0) = true → e ≠ 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h i j : C<VAR>α : f ⟶ g<VAR>β : g ⟶ h<VAR>η : h ⟶ i<VAR>ηs : i ⟶ j<GOAL>CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp β (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β) (CategoryTheory.CategoryStruct.comp η ηs)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h : C<VAR>α : f ⟶ g<VAR>β : g ⟶ h<GOAL>CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.comp α β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h i j : C<VAR>α : f ⟶ g<VAR>η : g ⟶ h<VAR>ηs : h ⟶ i<VAR>θ : i ⟶ j<VAR>ι : h ⟶ j<VAR>pf_ι : CategoryTheory.CategoryStruct.comp ηs θ = ι<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs)) θ = CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ι)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>g h : C<VAR>f : C<VAR>α : g ⟶ h<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft f α = CategoryTheory.MonoidalCategory.whiskerLeft f α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h i j : C<VAR>α : g ⟶ h<VAR>η : h ⟶ i<VAR>ηs : i ⟶ j<VAR>θ : CategoryTheory.MonoidalCategory.tensorObj f i ⟶ CategoryTheory.MonoidalCategory.tensorObj f j<VAR>pf_θ : CategoryTheory.MonoidalCategory.whiskerLeft f ηs = θ<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft f α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft f η) θ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h i : C<VAR>η : h ⟶ i<VAR>θ : CategoryTheory.MonoidalCategory.tensorObj g h ⟶ CategoryTheory.MonoidalCategory.tensorObj g i<VAR>ι : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g i)<VAR>ι' : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i<VAR>ι'' : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i<VAR>pf_θ : CategoryTheory.MonoidalCategory.whiskerLeft g η = θ<VAR>pf_ι : CategoryTheory.MonoidalCategory.whiskerLeft f θ = ι<VAR>pf_ι' : CategoryTheory.CategoryStruct.comp ι (CategoryTheory.MonoidalCategory.associator f g i).inv = ι'<VAR>pf_ι'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).hom ι' = ι''<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj f g) η = ι''
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g : C<VAR>η : f ⟶ g<VAR>η' : f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g<VAR>η'' : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g<VAR>pf_η' : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.leftUnitor g).inv = η'<VAR>pf_η'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor f).hom η' = η''<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) η = η''
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h : C<VAR>η η' : f ⟶ g<VAR>θ θ' : g ⟶ h<VAR>ι : f ⟶ h<VAR>pf_η : η = η'<VAR>pf_θ : θ = θ'<VAR>pf_ηθ : CategoryTheory.CategoryStruct.comp η' θ' = ι<GOAL>CategoryTheory.CategoryStruct.comp η θ = ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h : C<VAR>η η' : g ⟶ h<VAR>θ : CategoryTheory.MonoidalCategory.tensorObj f g ⟶ CategoryTheory.MonoidalCategory.tensorObj f h<VAR>pf_η : η = η'<VAR>pf_θ : CategoryTheory.MonoidalCategory.whiskerLeft f η' = θ<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft f η = θ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h : C<VAR>η η' : f ⟶ g<VAR>θ : CategoryTheory.MonoidalCategory.tensorObj f h ⟶ CategoryTheory.MonoidalCategory.tensorObj g h<VAR>pf_η : η = η'<VAR>pf_θ : CategoryTheory.MonoidalCategory.whiskerRight η' h = θ<GOAL>CategoryTheory.MonoidalCategory.whiskerRight η h = θ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : C<VAR>η : f ⟶ g<GOAL>η = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id f) (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id g))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g : C<VAR>α : f ⟶ g<VAR>h : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight α h = CategoryTheory.MonoidalCategory.whiskerRight α h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h i j : C<VAR>α : f ⟶ g<VAR>η : g ⟶ h<VAR>ηs : h ⟶ i<VAR>θ : CategoryTheory.MonoidalCategory.tensorObj h j ⟶ CategoryTheory.MonoidalCategory.tensorObj i j<VAR>pf_θ : CategoryTheory.MonoidalCategory.whiskerRight ηs j = θ<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs)) j = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight α j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight η j) θ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g h i j : C<VAR>α : g ⟶ CategoryTheory.MonoidalCategory.tensorObj f h<VAR>η : h ⟶ i<VAR>ηs : CategoryTheory.MonoidalCategory.tensorObj f i ⟶ j<VAR>k : C<VAR>η₁ : CategoryTheory.MonoidalCategory.tensorObj h k ⟶ CategoryTheory.MonoidalCategory.tensorObj i k<VAR>η₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k)<VAR>ηs₁ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f i) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k<VAR>ηs₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k<VAR>η₃ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k<VAR>η₄ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f h) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k<VAR>η₅ : CategoryTheory.MonoidalCategory.tensorObj g k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k<VAR>pf_η₁ : CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id h) (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id i))) k = η₁<VAR>pf_η₂ : CategoryTheory.MonoidalCategory.whiskerLeft f η₁ = η₂<VAR>pf_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs k = ηs₁<VAR>pf_ηs₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f i k).inv ηs₁ = ηs₂<VAR>pf_η₃ : CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃<VAR>pf_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f h k).hom η₃ = η₄<VAR>pf_η₅ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight α k) η₄ = η₅<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft f η) ηs)) k = η₅
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f f' g h : C<VAR>η : f ⟶ f'<VAR>η₁ : CategoryTheory.MonoidalCategory.tensorObj f g ⟶ CategoryTheory.MonoidalCategory.tensorObj f' g<VAR>η₂ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f' g) h<VAR>η₃ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)<VAR>η₄ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)<VAR>pf_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η g = η₁<VAR>pf_η₂ : CategoryTheory.MonoidalCategory.whiskerRight η₁ h = η₂<VAR>pf_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategory.associator f' g h).hom = η₃<VAR>pf_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).inv η₃ = η₄<GOAL>CategoryTheory.MonoidalCategory.whiskerRight η (CategoryTheory.MonoidalCategory.tensorObj g h) = η₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f g : C<VAR>η : f ⟶ g<VAR>η₁ : f ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)<VAR>η₂ : CategoryTheory.MonoidalCategory.tensorObj f (𝟙_ C) ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)<VAR>pf_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.rightUnitor g).inv = η₁<VAR>pf_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor f).hom η₁ = η₂<GOAL>CategoryTheory.MonoidalCategory.whiskerRight η (𝟙_ C) = η₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h i : C<VAR>η η' : f ⟶ g<VAR>α : g ⟶ h<VAR>θ θ' : h ⟶ i<VAR>αθ : g ⟶ i<VAR>ηαθ : f ⟶ i<VAR>pf_η : η = η'<VAR>pf_θ : θ = θ'<VAR>pf_αθ : CategoryTheory.CategoryStruct.comp α θ' = αθ<VAR>pf_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ<GOAL>CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α θ) = ηαθ
<VAR>α : Type u_1<VAR>a b a' b' : α<VAR>ha : a = a'<VAR>hb : b = b'<VAR>h : a' = b'<GOAL>a = b
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>k : α<VAR>n : ℕ<VAR>x a a' : α<VAR>h : k + a = a'<GOAL>k + Mathlib.Tactic.Abel.term n x a = Mathlib.Tactic.Abel.term n x a'
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>k : α<VAR>n : ℤ<VAR>x a a' : α<VAR>h : k + a = a'<GOAL>k + Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n x a'
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>x a k a' : α<VAR>h : a + k = a'<GOAL>Mathlib.Tactic.Abel.term n x a + k = Mathlib.Tactic.Abel.term n x a'
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n : ℤ<VAR>x a k a' : α<VAR>h : a + k = a'<GOAL>Mathlib.Tactic.Abel.termg n x a + k = Mathlib.Tactic.Abel.termg n x a'
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n₁ : ℕ<VAR>x a₁ : α<VAR>n₂ : ℕ<VAR>a₂ : α<VAR>n' : ℕ<VAR>a' : α<VAR>h₁ : n₁ + n₂ = n'<VAR>h₂ : a₁ + a₂ = a'<GOAL>Mathlib.Tactic.Abel.term n₁ x a₁ + Mathlib.Tactic.Abel.term n₂ x a₂ = Mathlib.Tactic.Abel.term n' x a'
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n₁ : ℤ<VAR>x a₁ : α<VAR>n₂ : ℤ<VAR>a₂ : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : n₁ + n₂ = n'<VAR>h₂ : a₁ + a₂ = a'<GOAL>Mathlib.Tactic.Abel.termg n₁ x a₁ + Mathlib.Tactic.Abel.termg n₂ x a₂ = Mathlib.Tactic.Abel.termg n' x a'
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>x a : α<GOAL>Mathlib.Tactic.Abel.term 0 x a = a
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>x a : α<GOAL>Mathlib.Tactic.Abel.termg 0 x a = a
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n : ℤ<VAR>x a : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : -n = n'<VAR>h₂ : -a = a'<GOAL>-Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n' x a'
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>c : ℕ<GOAL>Mathlib.Tactic.Abel.smul c 0 = 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>c : ℤ<GOAL>Mathlib.Tactic.Abel.smulg c 0 = 0
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>c n : ℕ<VAR>x a : α<VAR>n' : ℕ<VAR>a' : α<VAR>h₁ : c * n = n'<VAR>h₂ : Mathlib.Tactic.Abel.smul c a = a'<GOAL>Mathlib.Tactic.Abel.smul c (Mathlib.Tactic.Abel.term n x a) = Mathlib.Tactic.Abel.term n' x a'
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>c n : ℤ<VAR>x a : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : c * n = n'<VAR>h₂ : Mathlib.Tactic.Abel.smulg c a = a'<GOAL>Mathlib.Tactic.Abel.smulg c (Mathlib.Tactic.Abel.termg n x a) = Mathlib.Tactic.Abel.termg n' x a'
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>x : α<GOAL>x = Mathlib.Tactic.Abel.term 1 x 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>x : α<GOAL>x = Mathlib.Tactic.Abel.termg 1 x 0
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>x x' : α<VAR>h : x = x'<GOAL>x = Mathlib.Tactic.Abel.term 1 x' 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>x x' : α<VAR>h : x = x'<GOAL>x = Mathlib.Tactic.Abel.termg 1 x' 0
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : a + -b = c<GOAL>a - b = c
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>x y : α<VAR>h : Mathlib.Tactic.Abel.smul n x = y<GOAL>n • x = y
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n : ℕ<VAR>x y : α<VAR>h : Mathlib.Tactic.Abel.smulg (Int.ofNat n) x = y<GOAL>↑n • x = y
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n : ℤ<VAR>x y : α<VAR>h : Mathlib.Tactic.Abel.smulg n x = y<GOAL>n • x = y
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>l : ℕ<VAR>r : α<VAR>tl : ℕ<VAR>tr t : α<VAR>prl : l = tl<VAR>prr : r = tr<VAR>prt : Mathlib.Tactic.Abel.smul tl tr = t<GOAL>Mathlib.Tactic.Abel.smul l r = t
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>l : ℤ<VAR>r : α<VAR>tl : ℤ<VAR>tr t : α<VAR>prl : l = tl<VAR>prr : r = tr<VAR>prt : Mathlib.Tactic.Abel.smulg tl tr = t<GOAL>Mathlib.Tactic.Abel.smulg l r = t
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>l : ℕ<VAR>r : α<VAR>tl : ℕ<VAR>zl : ℤ<VAR>tr t : α<VAR>prl₁ : l = tl<VAR>prl₂ : ↑tl = zl<VAR>prr : r = tr<VAR>prt : Mathlib.Tactic.Abel.smulg zl tr = t<GOAL>Mathlib.Tactic.Abel.smul l r = t
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>l r tl tr t : α<VAR>prl : l = tl<VAR>prr : r = tr<VAR>prt : tl + tr = t<GOAL>l + r = t
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>l r tl tr t : α<VAR>prl : l = tl<VAR>prr : r = tr<VAR>prt : tl + tr = t<GOAL>l + r = t
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>a ta t : α<VAR>pra : a = ta<VAR>prt : -ta = t<GOAL>-a = t
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>x a : α<GOAL>Mathlib.Tactic.Abel.term n x a = n • x + a
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>n : ℤ<VAR>x a : α<GOAL>Mathlib.Tactic.Abel.termg n x a = n • x + a
<VAR>p : Prop<VAR>α : Type u<VAR>h₁ : Subsingleton α → p<VAR>h₂ : Nontrivial α → p<GOAL>p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c : R<GOAL>a + (b + c) = a + b + c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c : R<GOAL>a * (b * c) = a * b * c
<VAR>R : Type u_2<VAR>Ring R<VAR>a b : R<GOAL>a * -b = -(a * b)
<VAR>R : Type u_2<VAR>Ring R<VAR>a b : R<GOAL>a + -b = a - b
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>Nat.rawCast 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>Nat.rawCast 1 = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>n.rawCast = OfNat.ofNat n
<VAR>n : ℕ<VAR>R : Type u_2<VAR>Ring R<GOAL>(Int.negOfNat n).rawCast = -n.rawCast
<VAR>n d : ℕ<VAR>R : Type u_2<VAR>DivisionRing R<GOAL>Rat.rawCast (Int.ofNat n) d = n.rawCast / d.rawCast
<VAR>n d : ℕ<VAR>R : Type u_2<VAR>DivisionRing R<GOAL>Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>coe : outParam (β → α)<VAR>cond : outParam (α → Prop)<VAR>self : CanLift α β coe cond<VAR>x : α<GOAL>cond x → ∃ y, coe y = x
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>ne : ∀ (i : ι), Nonempty (α i)<VAR>p : ι → Prop<VAR>f : (i : Subtype p) → α i.val<GOAL>∃ g, (fun i => g i.val) = f
<VAR>α : Type u_1<VAR>a b : α<VAR>Add α<VAR>p : a = b<VAR>c : α<GOAL>a + c = b + c