mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRight_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} {g : b ⟶ c} {h : c ⟶ d} {η : f ⟶ f'}
  {η₁ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g}
  {η₂ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h}
  {η₃ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)}
  {η₄ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)},
  CategoryTheory.Bicategory.whiskerRight η g = η₁ →
    CategoryTheory.Bicategory.whiskerRight η₁ h = η₂ →
      CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f' g h).hom = η₃ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv η₃ = η₄ →
          CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) = η₄
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorAddUnit_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.AddMonObj.zero = CategoryTheory.AddMonObj.zero
-- Mathlib.Order.Defs.Unbundled
IsLinearOrder.toIsPartialOrder : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsLinearOrder α r], IsPartialOrder α r
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : PseudoEpimorphism α β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The `n`-sphere is the set of points in ℝⁿ⁺¹ whose norm equals `1`,
endowed with the subspace topology.  -/
TopCat.sphere : ℕ → TopCat
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- If the pairwise products of bounded continuous functions are all zero, then the norm of their
sum is the maximum of their norms.  -/
BoundedContinuousFunction.nnnorm_sum_eq_sup : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {ι : Type u_2} {f : ι → BoundedContinuousFunction α R} (s : Finset ι),
  Pairwise (Function.onFun (fun x1 x2 => x1 * x2 = 0) f) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x => ‖f x‖₊
-- Init.Data.List.Range
List.zipIdx_eq_zip_range' : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.zipIdx i = l.zip (List.range' i l.length)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.isAlgebraic_adjoin_simple_X : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (¬∃ c, f = RatFunc.C c) → IsAlgebraic (↥K⟮f⟯) RatFunc.X
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (toCoalgHom : A →ₗc[R] B) →
                      toCoalgHom.toFun 1 = 1 →
                        (∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y) → A →ₐc[R] B
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.coe_neg`. -/
AddAut.coe_inv : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), ⇑(-e) = ⇑(AddEquiv.symm e)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (x : α), TopologicalSpace.NonemptyCompacts.map f hf {x} = {f x}
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      (Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C) →
        (i : CategoryTheory.Arrow.leftFunc ⟶ Z) →
          (p : Z ⟶ CategoryTheory.Arrow.rightFunc) →
            autoParam (CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight)
                CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam →
              (∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) →
                (∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)) → W₁.FunctorialFactorizationData W₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → W'.addZ P Q * (P 2 * Q 2) = (P 0 * Q 2 - Q 0 * P 2) ^ 3
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_iInf : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_3} {f : α → β},
  Function.Injective f →
    ∀ (m : ι → MeasureTheory.OuterMeasure α),
      (MeasureTheory.OuterMeasure.map f) (⨅ i, m i) =
        (MeasureTheory.OuterMeasure.restrict (Set.range f)) (⨅ i, (MeasureTheory.OuterMeasure.map f) (m i))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tanh_sub_pi_mul_I : ∀ (z : ℂ), Complex.tanh (z - ↑Real.pi * Complex.I) = Complex.tanh z
-- Mathlib.Order.Nucleus
NucleusClass.mk : ∀ {F : Type u_2} {X : Type u_3} [inst : SemilatticeInf X] [inst_1 : FunLike F X X] [toInfHomClass : InfHomClass F X X],
  (∀ (x : X) (f : F), f (f x) ≤ f x) → (∀ (x : X) (f : F), x ≤ f x) → NucleusClass F X
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go : Lean.Meta.Grind.ENode →
  Lean.Meta.Grind.ENode →
    Lean.Meta.Grind.SolverTerms →
      Lean.Meta.Grind.SolverTerms →
        Lean.Meta.Grind.GoalM (Lean.Meta.Grind.SolverTerms × Lean.Meta.Grind.PendingSolverPropagationsData✝)
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Infinite M'] [Nontrivial R],
  Cardinal.mk (AddMonoidAlgebra R M') =
    max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inr_ A A').associator (CategoryTheory.Sum.inl_ (A ⊕ A') T) X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inlCompInrCompInverseAssociator A A' T).inv X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Sum.inl_ A' T).associator
              ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).hom
          ((CategoryTheory.Sum.inl_ A' T).whiskerLeft
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).hom)))
-- Mathlib.Data.NNReal.Defs
NNReal.iInf_empty : ∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → NNReal), ⨅ i, f i = 0
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.Iterator.curr.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.curr = String.Pos.Raw.get s i
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIrreducibleSpaceCarrierCarrierCommRingCat : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [IrreducibleSpace ↥S],
  IrreducibleSpace ↥(AlgebraicGeometry.AffineSpace n S)
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
/-- The functor `Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)` of
the Dold-Kan equivalence for additive categories.  -/
CategoryTheory.Preadditive.DoldKan.N : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
        (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₀.X₁ = CategoryTheory.Limits.kernel f
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E'4 : ADEInequality.Admissible (ADEInequality.E' 4)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCounit.eq_1 : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  L.ranCounit = { app := fun F => L.rightKanExtensionCounit F, naturality := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLiftIsKan_desc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g),
  (CategoryTheory.Bicategory.lanLiftIsKan f g).desc s = CategoryTheory.Bicategory.lanLiftDesc s
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqIRType : BEq Lean.IR.IRType
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π`, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi → x ≠ 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isSome_get?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, (Std.DHashMap.Const.get? m a).isSome = true ↔ a ∈ m
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.coe_addSubgroupMap_apply : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : ↥H),
  ↑((e.addSubgroupMap H) g) = e ↑g
-- Mathlib.Order.OrderIsoNat
Nat.Subtype.orderIsoOfNat.eq_1 : ∀ (s : Set ℕ) [inst : Infinite ↑s],
  Nat.Subtype.orderIsoOfNat s =
    RelIso.ofSurjective (RelEmbedding.natLT (Nat.Subtype.ofNat s) ⋯).orderEmbeddingOfLTEmbedding ⋯
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.aeval_sub : ∀ {R : Type u_1} [inst : CommRing R] {p : Polynomial R} {n : ℕ},
  p.IsMonicOfDegree n → ∀ (r : R), ((Polynomial.aeval (Polynomial.X - Polynomial.C r)) p).IsMonicOfDegree n
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsCofiltered J],
  Antitone (CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ico_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ico (a i) (b i)
-- Mathlib.Algebra.Group.Units.Hom
Units.mul_liftRight_inv : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N} {g : M → Nˣ}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), f x * ↑((Units.liftRight f g h) x)⁻¹ = 1
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionDisabled : Lean.FromJson Lean.Lsp.CodeActionDisabled
-- Mathlib.Data.Matrix.Basic
Matrix.diagonalAddMonoidHom_apply : ∀ (n : Type u_3) (α : Type u_11) [inst : DecidableEq n] [inst_1 : AddZeroClass α] (d : n → α),
  (Matrix.diagonalAddMonoidHom n α) d = Matrix.diagonal d
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv
        (CategoryTheory.Functor.whiskerRight (L.rightKanExtensionCounit F) G)) =
    L.rightKanExtensionCounit (F.comp G)
-- Mathlib.Order.UpperLower.Fibration
Relation.Fibration.isLowerSet_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LE α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f → ∀ {s : Set α}, IsLowerSet s → IsLowerSet (f '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoProduct_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  (CategoryTheory.Limits.biproduct.isoProduct f).inv =
    CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π f)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_comp_sumElim : ∀ {m n : ℕ} {α : Sort u_1} {xs : Fin m → α} {ys : Fin n → α},
  Fin.append xs ys ∘ Sum.elim (Fin.castAdd n) (Fin.natAdd m) = Sum.elim xs ys
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.stronglyMeasurable_llr : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  MeasureTheory.StronglyMeasurable (MeasureTheory.llr μ ν)
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_of_infinite' : ∀ (R M : Type u) [inst : Semiring R] [Nonempty M] [Infinite R],
  Cardinal.mk (AddMonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.instFullHomotopyCategoryMapHomotopyCategoryOfFaithful : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Full] [F.Faithful] [inst_6 : F.Additive],
  (F.mapHomotopyCategory c).Full
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM_indicatorConstLp : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α}
  [inst_3 : CompleteSpace F'] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F'),
  (MeasureTheory.condExpL1CLM F' hm μ) (MeasureTheory.indicatorConstLp 1 hs hμs x) =
    (MeasureTheory.condExpInd F' hm μ s) x
-- Lean.Parser.Command
Lean.Parser.Command.public : Lean.Parser.Parser
-- Mathlib.Order.MinMax
min_lt_min : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, c < a → d < b → min c d < min a b
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Equivalence.stdRefl`. -/
Equivalence.reflexive : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → Std.Refl r
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ)
  (ll rr : List ((a : α) × β a)) (size : ℕ) (k' : α) (v' : β k') (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hm_2 :
    Std.DTreeMap.Internal.Impl.contains' k l = true →
      Std.DTreeMap.Internal.Impl.contains' k (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) = true),
  Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) hm_2 rr =
    match h : k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll l_1 ⋯ (⟨k', v'⟩ :: r.toListModel ++ rr)
    | Ordering.eq => f (ll ++ l_1.toListModel) (Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯) ⋯ (r.toListModel ++ rr)
    | Ordering.gt => Std.DTreeMap.Internal.Impl.applyPartition.go k l f (ll ++ l_1.toListModel ++ [⟨k', v'⟩]) r ⋯ rr
-- Mathlib.Analysis.Convex.Cone.Dual
/-- Any set is a subset of its double dual cone.  -/
ProperCone.subset_dual_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] {s : Set M}, s ⊆ ↑(ProperCone.dual p.flip ↑(ProperCone.dual p s))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max w v₁))) (X : C)
  (e : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ≅ F) {X_1 : C},
  ((CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso F X).symm e).homEquiv =
    Equiv.ulift.symm.trans (equivEquivIso.symm (e.app X_1))
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
/-- The same oracle as `CertificateOracle.simplexAlgorithmSparse`, but uses dense matrices. Works faster
on dense states.
 -/
Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmDense : Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_2 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ x =
    Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret x).succ
-- Mathlib.Logic.Equiv.Set
Equiv.preimage_subset : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set β), ⇑e ⁻¹' s ⊆ ⇑e ⁻¹' t ↔ s ⊆ t
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.instHasLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F],
  L.HasLeftKanExtension F
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Rcc α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.retract_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g) {Z_1 : C} (h_1 : (CategoryTheory.Arrow.mk f).left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.r) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) h_1
-- Mathlib.Order.SymmDiff
sup_inf_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⊓ bihimp a b = a ⊓ b
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.Quotient.commGroup : {G : Type u_5} → [inst : CommGroup G] → (N : Subgroup G) → CommGroup (G ⧸ N)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.equivSum_symm_apply : ∀ {n : ℕ} (x : ZMod n ⊕ ZMod n),
  DihedralGroup.equivSum.symm x =
    match x with
    | Sum.inl j => DihedralGroup.r j
    | Sum.inr j => DihedralGroup.sr j
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveAt.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] (γ : ℝ → M)
  (v : (x : M) → TangentSpace I x) (t₀ : ℝ),
  IsMIntegralCurveAt γ v t₀ = ∀ᶠ (t : ℝ) in nhds t₀, HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
-- Mathlib.Algebra.BigOperators.Fin
/-- The sum of `g i j` over `i j : Fin (n + 1)`, `i ≠ j`,
is equal to the sum of `g i j + g j i` over `i < j`.

This lemma is useful for some proofs about differential forms.
In this application, the function has the signature `f : Fin (n + 1) → Fin n → M`,
where `f i j` means `g i (Fin.succAbove i j)` in the informal statements.

Similarly, the sum of `g i j + g j i` over `i < j`
is written as `f (Fin.castSucc i) j + f (Fin.succ j) i` over `i j : Fin n`, `j ≥ i`.
 -/
Fin.sum_sum_eq_sum_triangle_add : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → Fin n → M),
  ∑ i, ∑ j, f i j = ∑ i, ∑ j ≥ i, (f i.castSucc j + f j.succ i)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.id : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (self : CategoryTheory.Limits.DiagramOfCocones F) (j : J),
  (self.map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (self.obj j).pt
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t).getKey! k = t.getKey! k
-- Batteries.Data.List.Basic
/-- **Alias** of `List.findIdxsValues`.

---

Returns the elements of `l` that satisfy `p` together with their indexes in
`l` added to an optional parameter `start`. The returned list is ordered by index.
We have `l.findIdxsValues p s = (l.findIdxs p s).zip (l.filter p)`.
 -/
List.indexsValues : {α : Type u_1} → (α → Bool) → List α → optParam ℕ 0 → List (ℕ × α)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_id : ∀ {M : CommMonCat}, CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = MonoidHom.id ↑M
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.commonIntTangents_union_commonExtTangents : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s₁ s₂ : EuclideanGeometry.Sphere P),
  s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂ = s₁.commonTangents s₂