mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.partition_eq_filter_filter.aux : ∀ {α : Type u_1} {p : α → Bool} (l : List α) {as bs : List α},
  List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not ∘ p) l)
-- Mathlib.LinearAlgebra.Goursat
Submodule.goursatFst.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (L : Submodule R (M × N)),
  L.goursatFst = Submodule.map (LinearMap.fst R M N ∘ₗ L.subtype) (LinearMap.snd R M N ∘ₗ L.subtype).ker
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instMax.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupSeminorm.instMax = { max := fun p q => { toFun := ⇑p ⊔ ⇑q, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rii_eq_mkSlice_rio_min : ∀ {α : Type u_1} {xs : Array α}, Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size
-- Init.Data.Dyadic.Basic
Dyadic.toRat_intCast : ∀ (x : ℤ), (↑x).toRat = ↑x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkLTNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.add_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ + φ').τ₁ = φ.τ₁ + φ'.τ₁
-- Init.Data.UInt.Bitwise
UInt64.toUSize_not : ∀ (a : UInt64), (~~~a).toUSize = ~~~a.toUSize
-- Mathlib.CategoryTheory.Category.TwoP
/-- **Alias** of `TwoP.of`.

---

Turns a two-pointing into a two-pointed type.  -/
TwoPointing.TwoP : {X : Type u_3} → TwoPointing X → TwoP
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_polynomialZ : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialZ = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialZ
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff : {a : Lean.Level} → {a_1 : Q(Type a)} → {a_2 : Q(«$a_1»)} → Inhabited (Mathlib.Tactic.Ring.RatCoeff a_2)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The zero module is linearly disjoint with any other submodules.  -/
Submodule.LinearDisjoint.bot_right : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  M.LinearDisjoint ⊥
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Mathlib.Topology.MetricSpace.Algebra
lipschitz_with_lipschitz_const_add : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [inst_2 : LipschitzAdd β] (p q : β × β),
  dist (p.1 + p.2) (q.1 + q.2) ≤ ↑(LipschitzAdd.C β) * dist p q
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_homologyπ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.homologyπ j) = 0
-- Mathlib.Data.Seq.Computation
Computation.results_pure : ∀ {α : Type u} (a : α), (Computation.pure a).Results a 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filter_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, Std.ExtDHashMap.filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = false
-- Mathlib.Data.Finset.Disjoint
Finset.pairwiseDisjoint_singleton_iff_injOn : ∀ {ι : Type u_1} {α : Type u_2} {s : Set ι} {f : ι → α}, (s.PairwiseDisjoint fun i => {f i}) ↔ Set.InjOn f s
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  {X Y : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)}
  (f : X ⟶ Y),
  ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.one_mem_div : ∀ {α : Type u_2} [inst : Group α] {s : Set α}, s.Nonempty → 1 ∈ s / s
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.alterKey a f l)
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- The set of functions `f : E → F` that represent continuous linear maps `f : E →SL[σ₁₂] F`
at distance `≤ r` from `f₀ : E →SL[σ₁₂] F` is closed in the topology of pointwise convergence.
This is one of the key steps in the proof of the **Banach-Alaoglu** theorem.  -/
ContinuousLinearMap.isClosed_image_coe_closedBall : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f₀ : E →SL[σ₁₂] F) (r : ℝ), IsClosed (DFunLike.coe '' Metric.closedBall f₀ r)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α},
  M.IsBase B → e ∈ B → (M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusLift_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η → γ = J.plusLift η hQ
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_bot`. -/
Set.setOf_bot : ∀ {α : Type u}, {_x | ⊥} = ∅
-- Std.Net.Addr
/-- This structure represents the address: `segments[0]:segments[1]:...`.
 -/
Std.Net.IPv6Addr.segments : Std.Net.IPv6Addr → Vector UInt16 8
-- Init.Data.List.MapIdx
List.mapFinIdx_concat : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {e : α} {f : (i : ℕ) → α → i < (l ++ [e]).length → β},
  (l ++ [e]).mapFinIdx f = (l.mapFinIdx fun i a h => f i a ⋯) ++ [f l.length e ⋯]
-- Mathlib.Algebra.Order.Group.Abs
max_one_mul_max_inv_one_eq_mabs_self : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a : G), max a 1 * max a⁻¹ 1 = |a|ₘ
-- Mathlib.NumberTheory.Height.Basic
/-- Extension for the `positivity` tactic: `Height.logHeight₁` is always nonnegative.  -/
Mathlib.Meta.Positivity.evalLogHeight₁ : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedSyntheticMVarKind : Inhabited Lean.Elab.Term.SyntheticMVarKind
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.content : Lean.VersoModuleDocs.DocFrame✝ → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_sub : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S]
  [inst_4 : Ring R] (abv : R → S) [IsAbsoluteValue abv] (a b : R), abv (a - b) = abv (b - a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_eq_lineMap : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k) (p : P1),
  (AffineMap.homothety c r) p = (AffineMap.lineMap c p) r
-- Mathlib.Algebra.Quaternion
Quaternion.coe_commute : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (a : Quaternion R), Commute (↑r) a
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        (carrier : Set X) →
          (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) →
            IsClosed carrier →
              D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
/-- **Alias** of `FiniteDimensional.of_isCompactOperator_id`.

---

If the identity operator of a Banach space over a nontrivially normed field is compact,
then the space is finite dimensional.  -/
IsCompactOperator.finiteDimensional : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E],
  IsCompactOperator id → FiniteDimensional 𝕜 E
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is `C^n` within a set at a point, with `n ≥ 1`, then it is differentiable
within this set at this point.  -/
ContDiffWithinAt.differentiableWithinAt' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → n ≠ 0 → DifferentiableWithinAt 𝕜 f (insert x s) x
-- Mathlib.Algebra.Module.ZLattice.Summable
/-- Given a basis of a (possibly not full rank) `ℤ`-lattice, there exists a `ε > 0` such that
`|b.repr x i| < n` for all `‖x‖ < n * ε` (i.e. `b.repr x i = O(x)` depending only on `b`).
This is an arbitrary choice of such an `ε`.
 -/
ZLattice.normBound : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [FiniteDimensional ℝ E] → {L : Submodule ℤ E} → [DiscreteTopology ↥L] → {ι : Type u_3} → Module.Basis ι ℤ ↥L → ℝ
-- Mathlib.Algebra.Group.Action.Pi
Pi.smul' : {ι : Type u_1} →
  {α : ι → Type u_4} → {β : ι → Type u_5} → [(i : ι) → SMul (α i) (β i)] → SMul ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomialY / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialY
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyRingedSpace.forgetToTop.map f =
    (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map (CategoryTheory.InducedCategory.homMk f.toHom)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.isOpen_iff`. -/
DeltaGeneratedSpace.isOpen_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {U : Set Y}, IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' U)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_maxD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ofHom_hom : ∀ {M N : AddMonCat} (f : M ⟶ N), AddMonCat.ofHom (AddMonCat.Hom.hom f) = f
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_equiv_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α ≃ β} (x : α →₀ M) (a : β),
  (Finsupp.mapDomain (⇑f) x) a = x (f.symm a)
-- Lean.Parser.Extra
Lean.Parser.nonReservedSymbol.formatter : String → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.exists_finiteIndex_of_leftCoset_cover : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ → ∃ k ∈ s, (H k).FiniteIndex
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.grade_eq_lsingle_range : ∀ {M : Type u_1} (R : Type u_3) [inst : CommSemiring R] (m : M),
  AddMonoidAlgebra.grade R m = (AddMonoidAlgebra.lsingle m).range
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_rfl : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a p : M}, a ≡ a [PMOD p]
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_eq_top_of_isEmpty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [IsEmpty β] (f : β → α) (S : Finset β),
  S.inf f = ⊤
-- Init.Data.Order.Lemmas
Std.max_eq_if : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] {x : Max α} [Std.LawfulOrderLeftLeaningMax α] {a b : α},
  a ⊔ b = if b ≤ a then a else b
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.inv_app_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C), CategoryTheory.IsIso (α.inv.app X)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α)
  (μ : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.MutuallySingular s μ ↔ s.totalVariation.MutuallySingular μ.ennrealToMeasure
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.lift_comp_mk : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f),
  Representation.Coinvariants.lift ρ f h ∘ₗ Representation.Coinvariants.mk ρ = f
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenizeLM_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ) (p : Polynomial R), (Polynomial.homogenizeLM n) p = p.homogenize n
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncGE.toIsRelIff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncGE],
  e.IsRelIff
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_3 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.read q) =
    ∀ (s : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Λ'.Supports S (q s)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t.contains k = true → (cmp t.min! k).isLE = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α},
      (m₁.diff m₂ ⋯).getKeyD k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback else m₁.getKeyD k fallback
-- Mathlib.Analysis.Convex.Function
ConcaveOn.lt_right_of_left_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f z < f x → f y < f z
-- Lean.Server.References
/-- Gets the name of the module that contains `declName`.  -/
Lean.Server.getModuleContainingDecl? : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.Control.Functor.Multivariate
MvFunctor.LiftP_def : ∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] (P : α.Arrow (TypeVec.repeat n Prop))
  [LawfulMvFunctor F] (x : F α), MvFunctor.LiftP' P x ↔ ∃ u, MvFunctor.map (TypeVec.subtypeVal P) u = x
-- Std.Http.Data.Status
/-- 428 Precondition Required
 -/
Std.Http.Status.preconditionRequired : Std.Http.Status
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  I.supportSet ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_iInf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {x : M} {ι : Sort u_7} {f : ι → ConvexCone R M}, x ∈ iInf f ↔ ∀ (i : ι), x ∈ f i
-- Init.Util
panicWithPosWithDecl : {α : Sort u} → [Inhabited α] → String → String → ℕ → ℕ → String → α
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.CategoryStruct.id F).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Mathlib.ModelTheory.Basic
/-- An embedding of first-order structures is an embedding that commutes with the
interpretations of functions and relations.  -/
FirstOrder.«term_↪[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ContinuousMap.instNonUnitalCommCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] → [inst_2 : NonUnitalCommCStarAlgebra A] → NonUnitalCommCStarAlgebra C(α, A)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.isometry : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β), Isometry ⇑h
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_le_max_power_one : ∀ {a b c : Cardinal.{u_1}}, b ≤ c → a ^ b ≤ max (a ^ c) 1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (f : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.branch f q₁ q₂) x x_1 =
    bif f x then Turing.TM2.stepAux q₁ x x_1 else Turing.TM2.stepAux q₂ x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Auxiliary definition for `Over.coprod`.  -/
CategoryTheory.Over.coprodObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] →
      {A : C} → CategoryTheory.Over A → CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Over A)
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The forward direction of the equivalence between the decomposed category and the original.  -/
CategoryTheory.decomposedTo : (J : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.Functor (CategoryTheory.Decomposed J) J
-- Mathlib.Order.Interval.Set.Disjoint
iInter_Iio_of_not_bddBelow_range : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α}, ¬BddBelow (Set.range f) → ⋂ i, Set.Iio (f i) = ∅
-- Mathlib.Data.Fin.SuccPred
Fin.succ_le_or_le_castSucc : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.succ ≤ p ∨ p ≤ i.castSucc
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_eq_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁺ᵐ = a ↔ 1 ≤ a
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.flip.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.flip =
    { toLinearMap := P.flip, isPerfPair_toLinearMap := ⋯, root := P.coroot, coroot := P.root, root_coroot_two := ⋯,
      reflectionPerm := P.reflectionPerm, reflectionPerm_root := ⋯, reflectionPerm_coroot := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The obvious triangle `X₁ ⟶ X₁ ⨯ X₂ ⟶ X₂ ⟶ X₁⟦1⟧`.  -/
CategoryTheory.Pretriangulated.binaryProductTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (X₁ X₂ : C) →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] → CategoryTheory.Pretriangulated.Triangle C
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadControl n o] [inst_2 : MonadControlT m n]
  (f : ({β : Type u} → o β → m (stM m o β)) → m α),
  ⦃(Std.Do.wp (MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ ∘ x₂)).apply Q⦄ liftWith f ⦃Q⦄
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `differentiableAt_finCons` where the derivative variables are free on the RHS
instead.  -/
differentiableAt_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x
-- Mathlib.Data.EReal.Operations
EReal.instNeg : Neg EReal
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_iff_condExp_sub_nonneg : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E]
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E},
  MeasureTheory.Submartingale f ℱ μ ↔
    MeasureTheory.StronglyAdapted ℱ f ∧
      (∀ (i : ι), MeasureTheory.Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]
-- Mathlib.Topology.DenseEmbedding
/-- `i : α → β` is "dense inducing" if it has dense range and the topology on `α`
is the one induced by `i` from the topology on `β`.  -/
IsDenseInducing : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).getKeyD k fallback = m₁.getKeyD k fallback