mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.substInvFun.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ => h_3 n) =
    h_2 ()
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.category_id_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (X : CategoryTheory.Kleisli T),
  (CategoryTheory.CategoryStruct.id X).of = T.η.app X.of
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprNoopConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.NoopConfig
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- A continuous linear equivalence of two spaces induces a continuous equivalence of algebras of
their endomorphisms.  -/
ContinuousLinearEquiv.conjContinuousAlgEquiv : {𝕜 : Type u_1} →
  {G : Type u_4} →
    {H : Type u_5} →
      [inst : AddCommGroup G] →
        [inst_1 : AddCommGroup H] →
          [inst_2 : NormedField 𝕜] →
            [inst_3 : Module 𝕜 G] →
              [inst_4 : Module 𝕜 H] →
                [inst_5 : TopologicalSpace G] →
                  [inst_6 : TopologicalSpace H] →
                    [inst_7 : IsTopologicalAddGroup G] →
                      [inst_8 : IsTopologicalAddGroup H] →
                        [inst_9 : ContinuousConstSMul 𝕜 G] →
                          [inst_10 : ContinuousConstSMul 𝕜 H] → (G ≃L[𝕜] H) → (G →L[𝕜] G) ≃A[𝕜] H →L[𝕜] H
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
/-- Filter for approaching `i∞`.  -/
UpperHalfPlane.atImInfty : Filter UpperHalfPlane
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_left_unitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X)
      ((self.map f).toFunctor.map ((self.mapId a).hom.toNatTrans.app X))
-- Mathlib.Order.Ideal
Order.Ideal.instLattice : {P : Type u_1} → [inst : SemilatticeSup P] → [IsCodirectedOrder P] → Lattice (Order.Ideal P)
-- Mathlib.LinearAlgebra.Projection
Submodule.existsUnique_add_of_isCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E},
  IsCompl p q → ∀ (x : E), ∃ u v, ↑u + ↑v = x ∧ ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = u ∧ s = v
-- Mathlib.Algebra.Group.Submonoid.Basic
MonoidHom.coe_ofClosureMEqTopRight : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {s : Set M} (f : M → N)
  (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y),
  ⇑(MonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_subset_neighborSet_left : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), G.commonNeighbors v w ⊆ G.neighborSet v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.inter_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.inter_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₁.inter m₂ = ↑(Std.DHashMap.Internal.Raw₀.inter ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩)
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.instInhabited : (X : Pointed) → Inhabited (X.Hom X)
-- Std.Data.ExtTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.ExtTreeMap.foldrM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] → [LawfulMonad m] → [Std.TransCmp cmp] → (α → β → δ → m δ) → δ → Std.ExtTreeMap α β cmp → m δ
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The basis constructed in `DirectSum.IsInternal.subordinateOrthonormalBasis` is subordinate to
the `OrthogonalFamily` in question.  -/
DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  (DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV') a ∈
    V (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV')
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_of_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, m.isEmpty = true → m.get? a = none
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Semilinear maps `M →ₛₗ[f] N` identify to
morphisms `M ⟶ (ModuleCat.restrictScalars f).obj N`.  -/
ModuleCat.semilinearMapAddEquiv : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : ModuleCat R) → (N : ModuleCat S) → (↑M →ₛₗ[f] ↑N) ≃+ (M ⟶ (ModuleCat.restrictScalars f).obj N)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- Given a pair of morphisms `p`, `q` to `X` which factor through `f`, they factor through any kernel
pair of `f`.
 -/
CategoryTheory.IsKernelPair.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R X Y : C} →
      {f : X ⟶ Y} →
        {a b : R ⟶ X} →
          {S : C} →
            CategoryTheory.IsKernelPair f a b →
              (p q : S ⟶ X) →
                CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f →
                  { t // CategoryTheory.CategoryStruct.comp t a = p ∧ CategoryTheory.CategoryStruct.comp t b = q }
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeOutResponseErrorMessageOfToJson : {α : Type u_1} → [Lean.ToJson α] → CoeOut (Lean.JsonRpc.ResponseError α) Lean.JsonRpc.Message
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ],
  μ.toSignedMeasure.toMeasureOfZeroLE Set.univ ⋯ ⋯ = μ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → ∀ {t : Set M}, nhdsWithin x s = nhdsWithin x t → MDiffAt[t] f x
-- Mathlib.Data.Vector.Snoc
List.Vector.snoc_cons : ∀ {α : Type u_1} {n : ℕ} {x : α} (xs : List.Vector α n) {y : α}, (x ::ᵥ xs).snoc y = x ::ᵥ xs.snoc y
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_ofBoolListLE : ∀ {bs : List Bool} {i : ℕ},
  (BitVec.ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_succ_succ : ∀ (n k : ℕ), (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.piecewise.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s s_1 : Set α} (e_s : s = s_1)
  {inst : DecidablePred fun x => x ∈ s} [inst_1 : DecidablePred fun x => x ∈ s_1] (hs : MeasurableSet s)
  (κ κ_1 : ProbabilityTheory.Kernel α β),
  κ = κ_1 →
    ∀ (η η_1 : ProbabilityTheory.Kernel α β),
      η = η_1 → ProbabilityTheory.Kernel.piecewise hs κ η = ProbabilityTheory.Kernel.piecewise ⋯ κ_1 η_1
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_id : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A : TopRep k G),
  TopRep.Hom.hom (CategoryTheory.CategoryStruct.id A) = ContIntertwiningMap.id
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The second projection of a product is a non-unital algebra homomorphism.  -/
NonUnitalAlgHom.snd : (R : Type u) →
  [inst : Monoid R] →
    (A : Type v) →
      (B : Type w) →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : NonUnitalNonAssocSemiring B] → [inst_4 : DistribMulAction R B] → A × B →ₙₐ[R] B
-- Mathlib.RingTheory.FreeRing
instNontrivialFreeRing : ∀ (α : Type u_1), Nontrivial (FreeRing α)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorLeftObjFunctorTensorBifunctor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (X : C) →
                        CategoryTheory.Localization.Lifting
                          (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) W
                          ((CategoryTheory.MonoidalCategory.tensorLeft X).comp
                            (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε))
                          ((CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).obj
                            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X))
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTacticSeqBracketed : Lean.Elab.Tactic.Tactic
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toArray.isEmpty = m.isEmpty
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((v : β) → motive (some v)) → motive x
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.postcomp_id : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M), solution.postcomp LinearMap.id = solution
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.Grp C), (F.mapGrp.obj A).X = F.obj A.X
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  Quaternion.normSq a ≠ 0 ↔ a ≠ 0
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.coverPreserving_opensFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)
    (AlgebraicGeometry.Scheme.Hom.opensFunctor f)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_commute_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [inst_1 : Mul M],
  Commute m₁ m₂ → Commute r₁ r₂ → Commute (MonoidAlgebra.single m₁ r₁) (MonoidAlgebra.single m₂ r₂)
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal.toInductionSubgoal : Lean.Meta.CasesSubgoal → Lean.Meta.InductionSubgoal
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.monic_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.Monic 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {M : Type w'} [inst : L.Structure M] [inst_1 : Nonempty M]
  [inst_2 : M ⊨ T] {v : α → M} {φ : L.Formula α}, FirstOrder.Language.Formula.equivSentence φ ∈ T.typeOf v ↔ φ.Realize v
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiff 𝕜 n (f i)) → ContDiff 𝕜 n (∏ i ∈ t, f i)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- The composition of a continuous linear map with a continuous multilinear map is a bounded
bilinear operation.  -/
isBoundedBilinearMap_compMultilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {G : Type u_4} [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  {ι : Type u_5} {E : ι → Type u_6} [inst_5 : Fintype ι] [inst_6 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_7 : (i : ι) → NormedSpace 𝕜 (E i)], IsBoundedBilinearMap 𝕜 fun p => p.1.compContinuousMultilinearMap p.2
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.support_mono : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, H ≤ H' → H.support ⊆ H'.support
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric_nhdsWithin : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {c : α → Set α},
  IsCompact s → (∀ x ∈ s, c x ∈ nhdsWithin x s) → ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ∩ s ⊆ c y
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The equivalence `Karoubi (ChainComplex C α) ≌ ChainComplex (Karoubi C) α`.  -/
CategoryTheory.Idempotents.karoubiChainComplexEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (α : Type u_3) →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            CategoryTheory.Idempotents.Karoubi (ChainComplex C α) ≌
              ChainComplex (CategoryTheory.Idempotents.Karoubi C) α
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Diagnostics.mk.inj : ∀ {usedThmCounter triedThmCounter : Lean.PHashMap Lean.Meta.Origin ℕ} {congrThmCounter : Lean.PHashMap Lean.Name ℕ}
  {thmsWithBadKeys : Lean.PArray Lean.Meta.SimpTheorem}
  {usedThmCounter_1 triedThmCounter_1 : Lean.PHashMap Lean.Meta.Origin ℕ}
  {congrThmCounter_1 : Lean.PHashMap Lean.Name ℕ} {thmsWithBadKeys_1 : Lean.PArray Lean.Meta.SimpTheorem},
  { usedThmCounter := usedThmCounter, triedThmCounter := triedThmCounter, congrThmCounter := congrThmCounter,
        thmsWithBadKeys := thmsWithBadKeys } =
      { usedThmCounter := usedThmCounter_1, triedThmCounter := triedThmCounter_1, congrThmCounter := congrThmCounter_1,
        thmsWithBadKeys := thmsWithBadKeys_1 } →
    usedThmCounter = usedThmCounter_1 ∧
      triedThmCounter = triedThmCounter_1 ∧ congrThmCounter = congrThmCounter_1 ∧ thmsWithBadKeys = thmsWithBadKeys_1
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.ofTextEdit : Lean.Lsp.VersionedTextDocumentIdentifier → Lean.Lsp.TextEdit → Lean.Lsp.WorkspaceEdit
-- Mathlib.Order.Cover
Bool.instDecidableRelCovBy : DecidableRel fun x1 x2 => x1 ⋖ x2
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  LawfulSingleton ((a : α) × β a) (Std.ExtDHashMap α β)
-- Init.Control.State
/-- A tuple-based state monad.

Actions in `StateM σ` are functions that take an initial state and return a value paired with a
final state.
 -/
StateM : Type u → Type u → Type u
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- Coercion as a monoid hom.  -/
WithZero.coeMonoidHom : {α : Type u_1} → [inst : MulOneClass α] → α →* WithZero α
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.eq_4 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (n x : ℕ) (h_1 : (x k : ℕ) → motive 0 x k) (h_2 : (m : ℕ) → motive 1 m 0)
  (h_3 : (x : ℕ) → motive 2 x 0) (h_4 : (n x : ℕ) → motive n.succ.succ.succ x 0)
  (h_5 : (n m k : ℕ) → motive n.succ m k.succ),
  (match n.succ.succ.succ, x, 0 with
    | 0, x, k => h_1 x k
    | 1, m, 0 => h_2 m
    | 2, x, 0 => h_3 x
    | n.succ.succ.succ, x, 0 => h_4 n x
    | n.succ, m, k.succ => h_5 n m k) =
    h_4 n x
-- Mathlib.Algebra.Algebra.Prod
AlgHom.fst_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : A →ₐ[R] C), (AlgHom.fst R B C).comp (f.prod g) = f
-- Mathlib.Algebra.Star.CHSH
/-- In a noncommutative ordered \*-algebra over ℝ,
Tsirelson's bound for a CHSH tuple (A₀, A₁, B₀, B₁) is
`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2^(3/2) • 1`.

We prove this by providing an explicit sum-of-squares decomposition
of the difference.

(We could work over `ℤ[2^(1/2), 2^(-1/2)]` if we really wanted to!)
 -/
tsirelson_inequality : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : Algebra ℝ R] [IsOrderedModule ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R),
  IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.linearMap : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsBaseChange S (Algebra.linearMap R S)
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableWithinAt_abs_neg : ∀ (s : Set ℝ) {x : ℝ}, x < 0 → DifferentiableWithinAt ℝ (fun x => |x|) s x
-- Mathlib.Data.Rat.Lemmas
Rat.mul_num_den' : ∀ (q r : ℚ), (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V : (x : M') → TangentSpace I' x} {g : M' → 𝕜},
  VectorField.mpullbackWithin I I' f (g • V) s = g ∘ f • VectorField.mpullbackWithin I I' f V s
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_zero : ∀ (n : ℕ), n.ascFactorial 0 = 1
-- Mathlib.Data.Setoid.Basic
Setoid.ker_def : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α}, (Setoid.ker f) x y ↔ f x = f y
-- Mathlib.MeasureTheory.Measure.Sub
/-- The measure `μ - ν` is defined to be the least measure `τ` such that `μ ≤ τ + ν`.
It is equivalent to `(μ - ν) ⊔ 0` if `μ` and `ν` were signed measures.
Compare with `ENNReal.instSub`.
Specifically, note that if you have `α = {1,2}`, and `μ {1} = 2`, `μ {2} = 0`, and
`ν {2} = 2`, `ν {1} = 0`, then `(μ - ν) {1, 2} = 2`. However, if `μ ≤ ν`, and
`ν univ ≠ ∞`, then `(μ - ν) + ν = μ`.  -/
MeasureTheory.Measure.instSub : {α : Type u_1} → [inst : MeasurableSpace α] → Sub (MeasureTheory.Measure α)
-- Mathlib.Data.Set.Function
Set.bijOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.BijOn f ∅ ∅
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.atIdxSlow?_repeat : ∀ {α : Type w} {f : α → α} {init : α} {n : ℕ},
  Std.Iter.atIdxSlow? n (Std.Iter.repeat f init) = some (Nat.repeat f n init)
-- Mathlib.Order.Defs.Unbundled
IsStrictWeakOrder.incomp_trans : ∀ {α : Sort u_1} {lt : α → α → Prop} [self : IsStrictWeakOrder α lt] (a b c : α),
  ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft W)],
  CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂ =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.torsionOf.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  Ideal.torsionOf R M x = (LinearMap.toSpanSingleton R M x).ker
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.instDecidableRelAdjDeleteEdgesOfDecidablePredSym2MemSetOfDecidableEq : {V : Type u_1} →
  {G : SimpleGraph V} →
    {s : Set (Sym2 V)} →
      [DecidableRel G.Adj] → [DecidablePred fun x => x ∈ s] → [DecidableEq V] → DecidableRel (G.deleteEdges s).Adj
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  min a b ≤ max c d → min c d ≤ max a b → Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_append : ∀ {α : Type u} {β : Type v} (f : α → β) (s t : Stream'.Seq α),
  Stream'.Seq.map f (s.append t) = (Stream'.Seq.map f s).append (Stream'.Seq.map f t)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `x * log (1 + g x)` as `(x : ℝ) → ∞` is `t`,
where `t : ℝ` is the limit of `x * g x`.  -/
Real.tendsto_mul_log_one_add_of_tendsto : ∀ {g : ℝ → ℝ} {t : ℝ},
  Filter.Tendsto (fun x => x * g x) Filter.atTop (nhds t) →
    Filter.Tendsto (fun x => x * Real.log (1 + g x)) Filter.atTop (nhds t)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_iUnion_finite : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {η : Type u_6}
  {ιs : η → Type u_7} {f : (j : η) → ιs j → M},
  (∀ (j : η), LinearIndependent R (f j)) →
    (∀ (i : η) (t : Set η),
        t.Finite →
          i ∉ t → Disjoint (Submodule.span R (Set.range (f i))) (⨆ i ∈ t, Submodule.span R (Set.range (f i)))) →
      LinearIndependent R fun ji => f ji.fst ji.snd
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.collectDirectVarsInPattern.go : Lean.Meta.Match.Pattern → Array Lean.FVarId → Array Lean.FVarId
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `tsub_tsub_le` for an inequality.  -/
tsub_tsub_cancel_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α], a ≤ b → b - (b - a) = a