mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.FunLike.IsApply
IsIntCastApply.intCast_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : IntCast F} {inst_2 : SMul ℤ α}
  [self : IsIntCastApply F α] (n : ℤ) (x : α), ↑n x = n • x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_inter_le_size_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.Control.EquivFunctor
/-- `map` of `f` preserves the identity morphism.  -/
EquivFunctor.map_refl' : ∀ {f : Type u₀ → Type u₁} [self : EquivFunctor f] (α : Type u₀), EquivFunctor.map (Equiv.refl α) = id
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.instInhabited : {F : Type u → Type v} → [inst : Applicative F] → Inhabited (ApplicativeTransformation F F)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n log n)`. Build a tree from an unsorted list by inserting them one at a time.  -/
List.toRBMap : {α : Type u_1} → {β : Type u_2} → List (α × β) → (cmp : α → α → Ordering) → RBTree.RBMap α β cmp
-- Mathlib.Data.Finset.Density
Finset.dens_empty : ∀ {α : Type u_2} [inst : Fintype α], ∅.dens = 0
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.theory_model_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {T : L.Theory},
  L.ElementarilyEquivalent M N → (M ⊨ T ↔ N ⊨ T)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsLocalizationQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : W.HasLeftCalculusOfFractions],
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).IsLocalization W
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodCongr_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄),
  (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
-- Mathlib.RingTheory.LaurentSeries
/-- The uniform space isomorphism between two abstract completions of `ratfunc K`  -/
LaurentSeries.comparePkg : (K : Type u_2) → [inst : Field K] → LaurentSeries.RatFuncAdicCompl K ≃ᵤ LaurentSeries K
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The sequence `spectralValue_terms p` is nonnegative.  -/
spectralValueTerms_nonneg : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R) (n : ℕ), 0 ≤ spectralValueTerms p n
-- Mathlib.Analysis.Normed.Group.Basic
NormedCommGroup.tendsto_nhds_nhds : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {x : E}
  {y : F}, Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  (Std.HashMap.filter f m)[k]! = (m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mapₗ_reindexₐ : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {B : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : Module R A] [inst_6 : Star A]
  [inst_7 : AddCommMonoid B] [inst_8 : Mul B] [inst_9 : Module R B] [inst_10 : Star B] {e : m ≃ n}
  {M : CStarMatrix m m A} (φ : A →ₗ[R] B),
  (CStarMatrix.reindexₐ R B e) ((CStarMatrix.mapₗ φ) M) = (CStarMatrix.mapₗ φ) ((CStarMatrix.reindexₐ R A e) M)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Assumption.right : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (Q ⊢ₛ R) → P ∧ Q ⊢ₛ R
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_4.eq : ∀ {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u}
  {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u}
  {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} (t : List Lean.Lsp.DocumentSymbol)
  (F_1 : (t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t)
  (F_2 : (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t)
  (F_3 : (t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t)
  (F_5 : (t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t),
  Lean.Lsp.DocumentSymbol.brecOn_4 t F_1 F_2 F_3 F_4 F_5 =
    F_5 t (Lean.Lsp.DocumentSymbol.brecOn_4.go t F_1 F_2 F_3 F_4 F_5).2
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_Bind_bind : ∀ {ps : Std.Do.PostShape} {α β : Type u} (x : Std.Do.PredTrans ps α) (f : α → Std.Do.PredTrans ps β)
  (Q : Std.Do.PostCond β ps), (x >>= f).apply Q = x.apply (fun a => (f a).apply Q, Q.2)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.dep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → M.Dep C
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.logDeriv_qParam : ∀ (h : ℝ) (z : ℂ), logDeriv (Function.Periodic.qParam h) z = 2 * ↑Real.pi * Complex.I / ↑h
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.id_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P),
  AffineIndependent k p = ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator_anti : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {U V : Submodule R (Module.Dual R M)}, U ≤ V → V.dualCoannihilator ≤ U.dualCoannihilator
-- Lean.MetavarContext
Lean.DependsOn.State.visited : Lean.DependsOn.State → Lean.ExprSet
-- Mathlib.Combinatorics.Colex
/-- Strictly monotone functions preserve the colex ordering.  -/
Finset.Colex.toColex_image_lt_toColex_image : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s t : Finset α},
  StrictMono f → (toColex (Finset.image f s) < toColex (Finset.image f t) ↔ toColex s < toColex t)
-- Std.Net.Addr
/-- Indicates whether the interface is a loopback interface.
 -/
Std.Net.InterfaceAddress.isLoopback : Std.Net.InterfaceAddress → Bool
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mem_roots_map : ∀ {R : Type u} {k : Type y} [inst : Field R] {p : Polynomial R} [inst_1 : CommRing k] [inst_2 : IsDomain k]
  {f : R →+* k} {x : k}, p ≠ 0 → (x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0)
-- Mathlib.Logic.Equiv.Embedding
/-- Embeddings from a sum type are equivalent to two separate embeddings with disjoint ranges.  -/
Equiv.sumEmbeddingEquivProdEmbeddingDisjoint : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α ⊕ β ↪ γ) ≃ { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Ioi : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.image (Fin.cast h) (Finset.Ioi i) = Finset.Ioi (Fin.cast h i)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `X ← Z → Y` is a pullback diagram over `W`, where `W` is the
coproduct of `X` and `Y`, then `Z` is initial.  -/
CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] →
        {c : CategoryTheory.Limits.BinaryCofan X Y} →
          CategoryTheory.Limits.IsColimit c →
            {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} →
              CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsInitial s.pt
-- Mathlib.Data.Nat.Periodic
Nat.periodic_gcd : ∀ (a : ℕ), Function.Periodic a.gcd a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGED k fallback = t₂.getEntryGED k fallback
-- Mathlib.ModelTheory.LanguageMap
/-- Type synonym for `N` used to equip it with an `L[[A]]`-structure where the new constants on `A`
are interpreted via the embedding `f`.  -/
FirstOrder.Language.Embedding.withConstants : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {N : Type w'} → [inst_1 : L.Structure N] → L.Embedding M N → Set M → Type w'
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.IsOver.trans' : ∀ {X Y Z S : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S} {f : X.PartialIso Y} {g : Y.PartialIso Z}
  {e : f.target = g.source},
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f →
    AlgebraicGeometry.Scheme.PartialIso.IsOver sY sZ g → AlgebraicGeometry.Scheme.PartialIso.IsOver sX sZ (f.trans' g e)
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_subset_subsingleton_mem_of_forall_separating : ∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set α → Prop) {s : Set α}
  [h : HasCountableSeparatingOn α p s], s ∈ l → (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G],
  ⊤.lowerCentralSeries (AddGroup.nilpotencyClass G) = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff!_eq_false_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = false
-- Init.Data.Ord.Basic
compareLex.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β),
  compareLex cmp₁ cmp₂ a b = (cmp₁ a b).then (cmp₂ a b)
-- Lean.Meta.Order
/-- Given CCPO instances `inst₁ : CompleteLattice α₁` and `inst₂ : CompleteLattice α₂`,
constructs an instance of the type `CompleteLattice (α₁ × α₂)`.
 -/
Lean.Meta.mkInstCompleteLatticePProd : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Abelian.Basic
/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphism
admitting a kernel such that `F` preserves this kernel and `F.map p` is an epi,
then `F.map Y` identifies to the cokernel of `F.map (kernel.ι p)`.  -/
CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : D} →
              (p : X ⟶ Y) →
                [inst_4 : CategoryTheory.Limits.HasKernel p] →
                  (F : CategoryTheory.Functor D C) →
                    [F.PreservesZeroMorphisms] →
                      [CategoryTheory.Epi (F.map p)] →
                        [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair p 0) F] →
                          CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ p ⋯))
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The prelax functor from `Cat` to `Cat` defined with `WithInitial`.  -/
CategoryTheory.WithInitial.prelaxfunctor : CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_atom : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ℕ) {e : R}, a ^ b * Nat.rawCast 1 = e → a ^ b = e + 0
-- Init.Data.Vector.Lemmas
Vector.back?_flatten : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n},
  xss.flatten.back? = Vector.findSome? (fun xs => xs.back?) xss.reverse
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_const : ∀ {b : EReal}, b ≠ ⊥ → b ≠ ⊤ → (LinearGrowth.linearGrowthInf fun x => b) = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- In a `2`-truncated simplicial set, an edge from a vertex `x₀` to `x₁` is
a `1`-simplex with prescribed `0`-dimensional faces.  -/
SSet.Truncated.Edge : {X : SSet.Truncated 2} →
  X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 }) →
    X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 }) → Type u
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
IsSimplyConnected.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), IsSimplyConnected s = SimplyConnectedSpace ↑s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateLeft : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_id : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  LinearMap.rTensor M LinearMap.id = LinearMap.id
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropSuffix?_char_eq_dropSuffix?_beq : ∀ {c : Char} {s : String.Slice}, s.dropSuffix? c = s.dropSuffix? fun x => x == c
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Constructing a continuous multilinear map from a multilinear map satisfying a boundedness
condition.  -/
MultilinearMap.mkContinuous : {𝕜 : 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 : MultilinearMap 𝕜 E G) →
                      (C : ℝ) → (∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖) → ContinuousMultilinearMap 𝕜 E G
-- Mathlib.FieldTheory.Separable
/-- In a field `F`, for any `t ∈ F` and `n > 0`, the polynomial `X ^ n - t` is separable
iff `↑n ≠ 0`. The assumption `n > 0` is needed, since for `n = 0` the polynomial `X ^ n - t`
is separable iff `t ≠ 1`.  -/
Polynomial.X_pow_sub_C_separable_iff : ∀ {F : Type u} [inst : Field F] {n : ℕ} {x : F},
  0 < n → x ≠ 0 → ((Polynomial.X ^ n - Polynomial.C x).Separable ↔ ↑n ≠ 0)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanPrepareModuleHierarchyParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.LeanPrepareModuleHierarchyParams
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- Two morphisms in `Arrow V` have the same image in `RightFreyd V` if and only if there
exists a right homotopy between them.  -/
CategoryTheory.Preadditive.RightFreyd.quotient_map_eq_iff : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f g : u ⟶ v),
  (CategoryTheory.Preadditive.RightFreyd.quotient V).map f = (CategoryTheory.Preadditive.RightFreyd.quotient V).map g ↔
    Nonempty (CategoryTheory.Arrow.RightHomotopy f g)
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of an invertible power series is `0`.  -/
PowerSeries.order_zero_of_unit : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] {f : PowerSeries R}, IsUnit f → f.order = 0
-- Mathlib.Order.Partition.Basic
Partition.bot_notMem : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Partition s), ⊥ ∉ P
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.nonneg : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (p : α × β) (x : ℝ), 0 ≤ ↑(f p) x
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.Arith.Cutsat.pp? : Lean.Meta.Grind.Goal → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- Construct a quadratic form on a product of two modules from the quadratic form on each module.
 -/
QuadraticMap.prod : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R P] → QuadraticMap R M₁ P → QuadraticMap R M₂ P → QuadraticMap R (M₁ × M₂) P
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.comp_descToInjective_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [inst_2 : CategoryTheory.Injective J]
  (hf : CategoryTheory.CategoryStruct.comp S.f f = 0) {Z : C} (h : J ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.g (CategoryTheory.CategoryStruct.comp (hS.descToInjective f hf) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.Normed.Group.Uniform
dist_div_eq_dist_mul_left : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b c : E), dist (a / b) c = dist a (c * b)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.insertIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α} {b : β},
  m.WF → (m.insertIfNew a b).WF
-- Mathlib.Order.Filter.Map
Filter.map_iInf_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β},
  Filter.map m (iInf f) ≤ ⨅ i, Filter.map m (f i)
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.add_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  AntivaryOn f g₁ s → AntivaryOn f g₂ s → AntivaryOn f (g₁ + g₂) s
-- Mathlib.Geometry.Euclidean.Triangle
/-- If `X` lies strictly between `A` and `C`, then `∠ A P X + ∠ X P C = ∠ A P C`,
with no nondegeneracy assumption on the point `P`.  -/
EuclideanGeometry.angle_add_angle_eq_of_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a c p x : P},
  Sbtw ℝ a x c → EuclideanGeometry.angle a p x + EuclideanGeometry.angle x p c = EuclideanGeometry.angle a p c
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.Homotopy.h₁ : ∀ {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g), CategoryTheory.CategoryStruct.comp SSet.ι₁ H.h = g
-- Mathlib.CategoryTheory.Shift.Basic
/-- auxiliary definition for `FullyFaithful.hasShift`  -/
CategoryTheory.Functor.FullyFaithful.hasShift.zero : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F : CategoryTheory.Functor C D} →
                F.FullyFaithful →
                  (s : A → CategoryTheory.Functor C C) →
                    ((i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) →
                      (s 0 ≅ CategoryTheory.Functor.id C)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseNatToBounded : {n m : ℕ} → Std.Internal.Parsec.String.Parser ℕ → Std.Internal.Parsec.String.Parser (Std.Time.Internal.Bounded.LE ↑n ↑m)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := true })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := true }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_2 h'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.isLongestMatchAtChain_skipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} (pos : s.Pos), String.Slice.Pattern.Model.IsLongestMatchAtChain pat pos (pos.skipWhile pat)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.toArray_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic : ∀ {ι : 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) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] (i j : ι) [IsDomain R],
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
-- Init.Data.Int.Order
Int.le_add_of_neg_add_le : ∀ {a b c : ℤ}, -b + a ≤ c → a ≤ b + c
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- We say that `R` satisfies the rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` surjective
implies `m ≤ n`.  -/
RankCondition : (R : Type u) → [Semiring R] → Prop
-- Init.Data.Array.Lemmas
Array.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (as : Array α), Array.map f as = (Array.mapM (fun x => pure (f x)) as).run
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` contains the group's 0.  -/
AddSubgroup.zero_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), 0 ∈ H
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleResponse.mk.injEq : ∀ (queryResults queryResults_1 : Array Lean.Lsp.LeanQueriedModule),
  ({ queryResults := queryResults } = { queryResults := queryResults_1 }) = (queryResults = queryResults_1)
-- Mathlib.Order.SuccPred.Tree
/-- The type representing the elements in the tree.  -/
RootedTree.α : RootedTree → Type u_2
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
complexOfReal_hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ},
  DifferentiableAt ℝ f x →
    ∀ (h₂ : (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1),
      HasDerivAt f (((fderiv ℝ f x).complexOfReal h₂) 1) x
-- Mathlib.Tactic.FunProp.FunctionData
/-- indices of `args` that contain `mainVars`  -/
Mathlib.Meta.FunProp.FunctionData.mainArgs : Mathlib.Meta.FunProp.FunctionData → Array ℕ