mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sober
quasiSober_iff : ∀ (α : Type u_3) [inst : TopologicalSpace α],
  QuasiSober α ↔ ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.comp_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : One γ] {g : β → γ}
  {f : α → β}, HasCompactMulSupport f → g 1 = 1 → HasCompactMulSupport (g ∘ f)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap_eq_mulRightMap : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : CommSemiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : SMulCommClass R S S] [inst_5 : IsScalarTower R S S] {M : Submodule R S}
  (N : Submodule R S) {ι : Type u_6} (m : ι → ↥M), Submodule.mulLeftMap N m = N.mulRightMap m
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.addZeroClass : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → AddZeroClass (Π₀ (i : ι), β i)
-- Lean.Elab.Do.Control
/-- The full transformer stack over the base monad.  -/
Lean.Elab.Do.EffectForwarder.liftedStack : Lean.Elab.Do.EffectForwarder → Lean.Elab.Do.ControlStack
-- Init.Data.List.Sublist
List.Sublist.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.length ≤ l₁.length → l₁ = l₂
-- Mathlib.Logic.Basic
iff_mpr_iff_true_intro : ∀ {P : Prop} (h : P), ⋯ = h
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.List.moveToFront.loop : {α : Type u_1} → [Inhabited α] → List α → ℕ → α × List α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_pos_of_pos_of_nonneg`.  -/
add_pos_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 < a → 0 ≤ b → 0 < a + b
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mkCoconeMorphism_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  (desc : (s : CategoryTheory.Limits.Cocone F) → t ⟶ s)
  (uniq : ∀ (s : CategoryTheory.Limits.Cocone F) (m : t ⟶ s), m = desc s) (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.IsColimit.mkCoconeMorphism desc uniq).desc s = (desc s).hom
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.DaylightSavingRule.mk : String →
  Std.Time.TimeZone.Offset →
    Option Std.Time.TimeZone.TransitionRule →
      Option Std.Time.TimeZone.TransitionRule → Std.Time.TimeZone.DaylightSavingRule
-- Lean.Data.Lsp.Internal
Lean.Lsp.instEmptyCollectionModuleRefs : EmptyCollection Lean.Lsp.ModuleRefs
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instStrictForwardPatternChar : ∀ {c : Char}, String.Slice.Pattern.StrictForwardPattern c
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_assoc : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ),
  (ab.trans bc).trans cd = ab.trans (bc.trans cd)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.blacklistInsertion : Lean.Environment → Lean.Name → Bool
-- Mathlib.Order.Bounded
Set.bounded_le_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Iic a)
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
/-- The ring of Witt Vectors of a perfect field of positive characteristic is a DVR.
 -/
WittVector.isDiscreteValuationRing : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [PerfectRing k p],
  IsDiscreteValuationRing (WittVector p k)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_inter : ∀ {α : Type u_1} {s t u : Set α}, s \ (t ∩ u) = s \ t ∪ s \ u
-- Mathlib.Algebra.Group.Ext
CancelCommMonoid.mk.congr_simp : ∀ {M : Type u} [toCommMonoid : CommMonoid M] [toCommMonoid_1 : CommMonoid M]
  (e_toCommMonoid : toCommMonoid = toCommMonoid_1) [toIsLeftCancelMul : IsLeftCancelMul M],
  { toCommMonoid := toCommMonoid, toIsLeftCancelMul := toIsLeftCancelMul } =
    { toCommMonoid := toCommMonoid_1, toIsLeftCancelMul := ⋯ }
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.anti_right : ∀ {α : Type u_1} {β : Type u_2} {G H K : Graph α β}, H ≤ K → K ≤ G → H.IsInducedSubgraph G → H.IsInducedSubgraph K
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.nhds_eq_comap_inf_principal : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X},
  x ∈ e.source → nhds x = Filter.comap (↑e) (nhds (↑e x)) ⊓ Filter.principal e.source
-- Mathlib.Data.Fin.Rev
Fin.succAbove_rev_right : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i.rev = (p.rev.succAbove i).rev
-- Mathlib.Data.NNRat.Defs
NNRat.coe_ne_zero : ∀ {q : ℚ≥0}, ↑q ≠ 0 ↔ q ≠ 0
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIso.mk : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} {f : K ⟶ L}
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i],
  autoParam (∀ (i : ι), QuasiIsoAt f i) QuasiIso.quasiIsoAt._autoParam → QuasiIso f
-- Mathlib.Data.Fin.Basic
Fin.one_eq_mk : ∀ {n a : ℕ} {ha : a < n + 2}, 1 = ⟨a, ha⟩ ↔ a = 1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.IsEquivalence.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam F.Faithful CategoryTheory.Functor.IsEquivalence.faithful._autoParam →
    autoParam F.Full CategoryTheory.Functor.IsEquivalence.full._autoParam →
      autoParam F.EssSurj CategoryTheory.Functor.IsEquivalence.essSurj._autoParam → F.IsEquivalence
-- Mathlib.Analysis.Convex.Function
ConvexOn.comp_strictConcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConvexOn 𝕜 (f '' s) g → StrictConcaveOn 𝕜 s f → StrictAntiOn g (f '' s) → StrictConvexOn 𝕜 s (g ∘ f)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.State.mk.injEq : ∀ (num : ℕ) (candidates : List Lean.Meta.Grind.SplitInfo) (added : Std.HashSet Lean.Meta.Grind.SplitInfo)
  (resolved : Lean.PHashSet Lean.Meta.Sym.ExprPtr) (trace : List Lean.Meta.Grind.CaseTrace)
  (lookaheads : List Lean.Meta.Grind.SplitInfo) (argPosMap : Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ))
  (argsAt : Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)) (num_1 : ℕ)
  (candidates_1 : List Lean.Meta.Grind.SplitInfo) (added_1 : Std.HashSet Lean.Meta.Grind.SplitInfo)
  (resolved_1 : Lean.PHashSet Lean.Meta.Sym.ExprPtr) (trace_1 : List Lean.Meta.Grind.CaseTrace)
  (lookaheads_1 : List Lean.Meta.Grind.SplitInfo) (argPosMap_1 : Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ))
  (argsAt_1 : Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)),
  ({ num := num, candidates := candidates, added := added, resolved := resolved, trace := trace,
        lookaheads := lookaheads, argPosMap := argPosMap, argsAt := argsAt } =
      { num := num_1, candidates := candidates_1, added := added_1, resolved := resolved_1, trace := trace_1,
        lookaheads := lookaheads_1, argPosMap := argPosMap_1, argsAt := argsAt_1 }) =
    (num = num_1 ∧
      candidates = candidates_1 ∧
        added = added_1 ∧
          resolved = resolved_1 ∧
            trace = trace_1 ∧ lookaheads = lookaheads_1 ∧ argPosMap = argPosMap_1 ∧ argsAt = argsAt_1)
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k fallback : α}, m₁.contains k = false → (m₁.inter m₂).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany_list : ∀ {α : Type u} {β : Type v} {x : Ord α} [inst : BEq α] [Std.TransOrd α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {t : Std.DTreeMap.Internal.Impl α fun x => β} (h : t.WF),
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).toListModel.Perm
    (Std.Internal.List.insertListConst t.toListModel l)
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.list : {α : Type w} → Std.Iterators.Types.ListIterator α → List α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_apply_of_contains_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  (h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true),
  (f k (t.get k ⋯)).isSome = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.neq_of_mem_ofStabilizer : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (a : α)
  {x : ↥(SubMulAction.ofStabilizer G a)}, ↑x ≠ a
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_add : ∀ {w i : ℕ}, i < w → ∀ (x y : BitVec w), (x + y).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ BitVec.carry i x y false))
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
FormalMultilinearSeries.compAlongOrderedFinpartition_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) (v : Fin n → E),
  (q.compAlongOrderedFinpartition p c) v = (q c.length) (c.applyOrderedFinpartition (fun m => p (c.partSize m)) v)
-- Init.Core
/-- The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.

It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
 -/
PSum : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_apply_le_apply_prod : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [AddLeftMono β] (s : Finset ι) {f : ι → α} (g : α → β),
  0 ≤ g 1 → (∀ (a b : α), g a + g b ≤ g (a * b)) → ∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x)
-- Mathlib.Order.Sublocale
Sublocale.inf_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {a b : X}, a ∈ S → b ∈ S → a ⊓ b ∈ S
-- Mathlib.Analysis.Complex.Basic
Complex.conjCAE_apply : ∀ (z : ℂ), Complex.conjCAE z = (starRingEnd ℂ) z
-- Init.Grind.AC
Lean.Grind.AC.Expr.brecOn.go : {motive : Lean.Grind.AC.Expr → Sort u} →
  (t : Lean.Grind.AC.Expr) →
    ((t : Lean.Grind.AC.Expr) → Lean.Grind.AC.Expr.below t → motive t) → motive t ×' Lean.Grind.AC.Expr.below t
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The set of program positions. We make extensive use of inductive types here to let us describe
"subroutines"; for example `clear p k q` is a program that clears stack `k`, then does `q` where
`q` is another label. In order to prevent this from resulting in an infinite number of distinct
accessible states, we are careful to be non-recursive (although loops are okay). See the section
documentation for a description of all the programs.  -/
Turing.PartrecToTM2.Λ' : Type
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f g : MeasureTheory.SimpleFunc α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coconeUnopOfConeEquiv =
    {
      functor :=
        { obj := fun c => CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      inverse :=
        { obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c),
          map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ),
      counitIso :=
        CategoryTheory.Iso.refl
          ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c),
                map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun c => CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c),
              map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }),
      functor_unitIso_comp := ⋯ }
-- Lean.Level
Lean.mkLevelSucc : Lean.Level → Lean.Level
-- Init.Core
ne_self_iff_false : ∀ {α : Sort u_1} (a : α), a ≠ a ↔ False
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic' n R` is different from `0`.  -/
Polynomial.cyclotomic'_ne_zero : ∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' n R ≠ 0
-- Mathlib.Geometry.Euclidean.Volume.Measure
instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_5}
  [inst_3 : AddGroup α] [inst_4 : AddAction α X] [IsIsometricVAdd α X] (d : ℕ),
  MeasureTheory.VAddInvariantMeasure α X (MeasureTheory.Measure.euclideanHausdorffMeasure d)
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddCommGroup.nhds_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (x : E),
  (nhds x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y - x‖ < ε}
-- Init.Tactics
/-- Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
`BitVec` goals already.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvNormalizeMacro : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_lt_top : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f : Ω → ENNReal},
  ∫⁻ (x : Ω), f x ∂P ≠ ⊤ → ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x < ⊤
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- This prevents `toVal v x` being printed as `{ ofAbs := x }` by `delabStructureInstance`.  -/
WithVal.delabToVal : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.ofLocalizationPrime : RingHom.OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Std.Data.DTreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.DTreeMap.Const.mergeWith : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      (α → β → β → β) →
        Std.DTreeMap α (fun x => β) cmp → Std.DTreeMap α (fun x => β) cmp → Std.DTreeMap α (fun x => β) cmp
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.cast_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ g₀ g₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X), (F.cast h₀ h₁) a = F a
-- Mathlib.LinearAlgebra.Matrix.PosDef
QuadraticForm.posDef_of_toMatrix' : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)},
  Q.toMatrix'.PosDef → QuadraticMap.PosDef Q
-- Mathlib.Topology.Order.LeftRight
continuousAt_iff_continuous_left'_right' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β}, ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iio a) a ∧ ContinuousWithinAt f (Set.Ioi a) a
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.pretrivialization_mem_atlas : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (x : B),
  self.pretrivializationAt x ∈ self.pretrivializationAtlas
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderOptionT : {m : Type u_1 → Type u_2} →
  {α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.PartialOrder (m α)] → Lean.Order.PartialOrder (OptionT m α)
-- Init.Data.String.Subslice
/-- The byte position of the end of the subslice.  -/
String.Slice.Subslice.endExclusive : {s : String.Slice} → s.Subslice → s.Pos
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.mk.inj : ∀ {μ : YoungDiagram} {entry : ℕ → ℕ → ℕ} {row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2}
  {col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j}
  {zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0} {entry_1 : ℕ → ℕ → ℕ}
  {row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2}
  {col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j}
  {zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0},
  { entry := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' } =
      { entry := entry_1, row_weak' := row_weak'_1, col_strict' := col_strict'_1, zeros' := zeros'_1 } →
    entry = entry_1
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.codRestrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s),
  f.codRestrict s h = { toFun := fun n => ⟨f n, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Interval.Finset.Defs
Prod.instLocallyFiniteOrderTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [LocallyFiniteOrderTop α] → [LocallyFiniteOrderTop β] → [DecidableLE (α × β)] → LocallyFiniteOrderTop (α × β)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.add_subset : ∀ {M : Type u_3} [inst : AddMonoid M] {s t : Set M} {S : AddSubmonoid M}, s ⊆ ↑S → t ⊆ ↑S → s + t ⊆ ↑S
-- Mathlib.Analysis.Convex.Jensen
StrictConvexOn.map_sum_lt_iff_of_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_inv_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} {f f' : x ⟶ y} {g g' : y ⟶ z} {h h' : z ⟶ t}
  (ef : f = f') (eg : g = g') (eh : h = h'),
  (CategoryTheory.Bicategory.associator f g h).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g' h').inv
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.norm_setToFun_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hf : MeasureTheory.Integrable f μ),
  0 ≤ C → ‖MeasureTheory.setToFun μ T hT f‖ ≤ C * ‖MeasureTheory.Integrable.toL1 f hf‖
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `zero_apply`. -/
ContinuousLinearMap.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.bounds_nonempty : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G}, ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.instCoeSubtypeMemSubringInteger : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → {v : Valuation A Γ} → [hv : v.IsRankOneDiscrete] → Coe v.Uniformizer ↥v.integer
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.algebraMap_eq_zero_iff : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : R),
  (algebraMap R (ExteriorAlgebra R M)) x = 0 ↔ x = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union!_equiv_congr_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁.union! m₃).Equiv (m₂.union! m₃)