mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap`
map it to the same point.
See `CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small` for a version with
less universe assumptions.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type w}
  (X : I → C) (π : (i : I) → X i ⟶ B) [inst_1 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks]
  (x : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X),
  CategoryTheory.Presieve.Arrows.Compatible P π
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.Types.productIso fun i => P.obj (Opposite.op (X i))).hom)
        x) ↔
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π)) x
-- Mathlib.LinearAlgebra.FreeAlgebra
FreeAlgebra.rank_eq : ∀ (R : Type u) (X : Type v) [inst : CommRing R] [Nontrivial R],
  Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zpow_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Group γ] [inst_4 : IsTopologicalGroup γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)),
  (f ^ z).comp g = f.comp g ^ z
-- Mathlib.Data.Num.Lemmas
Num.ofNat'_zero : Num.ofNat' 0 = 0
-- Mathlib.Data.PNat.Xgcd
/-- The reduction step does not change the product vector.  -/
PNat.XgcdType.step_v : ∀ (u : PNat.XgcdType), u.r ≠ 0 → u.step.v = u.v.swap
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card_functions_sum : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (i : ℕ),
  Cardinal.mk ((L.sum L').Functions i) =
    Cardinal.lift.{u', u} (Cardinal.mk (L.Functions i)) + Cardinal.lift.{u, u'} (Cardinal.mk (L'.Functions i))
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofList_nil : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, Std.HashMap.ofList [] = ∅
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X Y : J} (f : X ⟶ Y),
  c.toCostructuredArrow.map f = CategoryTheory.CostructuredArrow.homMk f ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.isIso_inl_iso_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {inl inr : X ⟶ P} {f : Y ⟶ X},
  CategoryTheory.IsPushout f f inl inr →
    autoParam (CategoryTheory.Epi f) CategoryTheory.IsPushout.isIso_inl_iso_of_epi._auto_1 → CategoryTheory.IsIso inl
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.CompletionAtInfty.instAlgebra : (F : Type u_1) →
  [inst : Field F] → [inst_1 : DecidableEq (RatFunc F)] → Algebra (RatFunc F) (RatFunc.CompletionAtInfty F)
-- Mathlib.Algebra.Star.Basic
StarAddMonoid.toInvolutiveStar : {R : Type u} → {inst : AddMonoid R} → [self : StarAddMonoid R] → InvolutiveStar R
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coe_eval₂AlgHom : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (g : σ → S₁), ⇑(MvPolynomial.eval₂AlgHom R g) = MvPolynomial.eval₂ (algebraMap R S₁) g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k fallback =
          Std.DHashMap.Internal.Raw₀.Const.getD m k fallback
-- Init.Sym.Lemmas
Lean.Sym.Int.le_eq_false : ∀ (a b : ℤ), decide (a ≤ b) = false → (a ≤ b) = False
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefView.default : Lean.Elab.DefView
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedImportInfo.default : Lean.Lsp.ImportInfo
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The `simp` normal form for a quadratic map is `DFunLike.coe`, not `toFun`.  -/
QuadraticMap.toFun_eq_coe : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N), Q.toFun = ⇑Q
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.prod_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β × γ → α},
  Summable f → Summable fun p => f p.swap
-- Init.Data.UInt.Lemmas
UInt64.lt_add_one : ∀ {c : UInt64}, c ≠ -1 → c < c + 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.contains'.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.contains' k l =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf => false
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.contains' k l
      | Ordering.gt => Std.DTreeMap.Internal.Impl.contains' k r
      | Ordering.eq => true
-- Mathlib.Data.Finmap
/-- There are no duplicate keys in `entries`  -/
Finmap.nodupKeys : ∀ {α : Type u} {β : α → Type v} (self : Finmap β), self.entries.NodupKeys
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A def to put an `Add` instance on a type with a `Language.ring.Structure` instance.

To be used sparingly, usually only when defining a more useful definition like,
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K`  -/
FirstOrder.Ring.addOfRingStructure : (R : Type u_2) → [FirstOrder.Language.ring.Structure R] → Add R
-- Mathlib.Analysis.Meromorphic.Order
/-- Compatibility of notions of `order` for analytic and meromorphic functions.  -/
AnalyticAt.meromorphicOrderAt_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  AnalyticAt 𝕜 f x → meromorphicOrderAt f x = ENat.map Nat.cast (analyticOrderAt f x)
-- Mathlib.Logic.Encodable.Pi
/-- When `α` is finite and all `π a` are encodable, `Π a, π a` is encodable too. Because the
encoding is not unique, we wrap it in `Trunc` to preserve computability.  -/
Encodable.fintypePi : (α : Type u_2) →
  (π : α → Type u_3) → [DecidableEq α] → [Fintype α] → [(a : α) → Encodable (π a)] → Trunc (Encodable ((a : α) → π a))
-- Mathlib.Algebra.Ring.Prod
/-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`.  -/
Prod.instNonUnitalCommRing : {R : Type u_1} → {S : Type u_3} → [NonUnitalCommRing R] → [NonUnitalCommRing S] → NonUnitalCommRing (R × S)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- The inverse isometric equivalence of an isometric equivalence between two quadratic forms.  -/
QuadraticMap.IsometryEquiv.symm : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} →
                        {Q₂ : QuadraticMap R M₂ N} → Q₁.IsometryEquiv Q₂ → Q₂.IsometryEquiv Q₁
-- Mathlib.CategoryTheory.Category.Preorder
/-- A functor `X ⥤ Y` between preorder categories as an `OrderHom`.  -/
CategoryTheory.Functor.toOrderHom : {X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → CategoryTheory.Functor X Y → X →o Y
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAddAction.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.instAddAction = Function.Injective.addAction SetLike.coe ⋯ ⋯
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.bound : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ∀ {ε : ℝ},
      ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen✝ p F a ^ 2 ^ n < ε
-- Init.Data.Int.OfNat
Nat.ToInt.of_le : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → a ≤ b → a' ≤ b'
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.inner_left_rankOne_apply : ∀ {𝕜 : Type u_4} {F : Type u_6} {G : Type u_7} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : InnerProductSpace 𝕜 F] [inst_3 : SeminormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (x : F)
  (y z : G) (w : F), inner 𝕜 ((((InnerProductSpace.rankOne 𝕜) x) y) z) w = inner 𝕜 z y * inner 𝕜 x w
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.typesWith_eq_univ_of_mem_onTheory_lhomWithConstants : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : (L.withConstants α).Sentence},
  φ ∈ (L.lhomWithConstants α).onTheory T → T.typesWith φ = Set.univ
-- Mathlib.Computability.NFA
_private.Mathlib.Computability.NFA.0.NFA.Path.supp.match_1.eq_1 : ∀ {α : Type u_1} {σ : Type u_2} {M : NFA α σ} (motive : (x : List α) → (t s : σ) → M.Path s t x → Sort u_3) (s : σ)
  (h_1 : (s : σ) → motive [] s s (NFA.Path.nil s))
  (h_2 :
    (t s t_1 : σ) →
      (a : α) →
        (x : List α) →
          (a_1 : t_1 ∈ M.step s a) → (p : M.Path t_1 t x) → motive (a :: x) t s (NFA.Path.cons t_1 s t a x a_1 p)),
  (match [], s, s, NFA.Path.nil s with
    | .([]), s, .(s), NFA.Path.nil .(s) => h_1 s
    | .(a :: x), t, s, NFA.Path.cons t_1 .(s) .(t) a x a_1 p => h_2 t s t_1 a x a_1 p) =
    h_1 s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] {S : AddSubmonoid M} {f : M → N},
  (∀ (y : ↥S), IsAddUnit (f ↑y)) →
    (∀ (z : N), ∃ x, z + f ↑x.2 = f x.1) → (∀ {x y : M}, f x = f y → ∃ c, ↑c + x = ↑c + y) → S.IsLocalizationMap f
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_eq_coe_ennreal_iff : ∀ {x y : ENNReal}, ↑x = ↑y ↔ x = y
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.coe_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeftZeroExtend_eq : ∀ {w n : ℕ} {x : BitVec w}, x.shiftLeftZeroExtend n = BitVec.setWidth (w + n) x <<< n
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instLattice.eq_1 : ∀ {E : Type u_3} [inst : AddCommGroup E],
  AddGroupSeminorm.instLattice =
    { toSemilatticeSup := AddGroupSeminorm.semilatticeSup, inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.condExp_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] {i j : ℕ},
      i ≤ j →
        ∀ (a : α) {s : Set β},
          MeasurableSet s →
            (ν a)[fun x => κ.densityProcess ν j a x s | ↑(ProbabilityTheory.countableFiltration γ) i] =ᵐ[ν a] fun x =>
              κ.densityProcess ν i a x s
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_abs₃ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W a b |c| d = IsEllipticNet.atomRel W a b c d
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.generate_mem_toGrothendieck : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} {X : C}
  {R : CategoryTheory.Presieve X}, R ∈ J.coverings X → CategoryTheory.Sieve.generate R ∈ J.toGrothendieck X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- `z + star z` is the trace of `z`.  -/
QuadraticAlgebra.algebraMap_trace_eq_add_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  (algebraMap R (QuadraticAlgebra R a b)) (QuadraticAlgebra.trace z) = z + star z
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_pred : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop},
  Filter.EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.find.congr_simp : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (c c_1 : Set (ShrinkingLemma.PartialRefinement u s p)) (e_c : c = c_1) (ne : c.Nonempty) (i i_1 : ι),
  i = i_1 → ShrinkingLemma.PartialRefinement.find c ne i = ShrinkingLemma.PartialRefinement.find c_1 ⋯ i_1
-- Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
/-- Given `X : Type u`, `A : Set X`, `U : ι → Set X` and `V : ι → ι → Set X` such
that `MulticoequalizerDiagram A U V` holds, then in the category of types,
`A` is the multicoequalizer of the `U i`s along the `V i j`s.  -/
CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram : {X : Type u} →
  {ι : Type w} →
    {A : Set X} →
      {U : ι → Set X} →
        {V : ι → ι → Set X} →
          (c : CompleteLattice.MulticoequalizerDiagram A U V) →
            CategoryTheory.Limits.IsColimit (c.multicofork.map Set.functorToTypes)
-- Mathlib.Data.UInt
/-- Is this an ASCII digit character?  -/
UInt8.isASCIIDigit : UInt8 → Bool
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the
first cocone was colimiting also.
 -/
CategoryTheory.Limits.IsColimit.ofPointIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cocone F} →
            (P : CategoryTheory.Limits.IsColimit r) →
              [i : CategoryTheory.IsIso (P.desc t)] → CategoryTheory.Limits.IsColimit t
-- Mathlib.Topology.Compactification.StoneCech
stoneCech_hom_ext : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β]
  {g₁ g₂ : StoneCech α → β}, Continuous g₁ → Continuous g₂ → g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit → g₁ = g₂
-- Mathlib.Tactic.Order.CollectFacts
/-- Adds `type` to the state. It checks if the type has already been added up to
`reducible_and_instances` transparency. Returns the type that is added to the state and
definitionally equal (but may be not syntactically equal) to `type`.  -/
Mathlib.Tactic.Order.addType : {u : Lean.Level} → Q(Type u) → Mathlib.Tactic.Order.CollectFactsM Q(Type u)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
algebraMap_le_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (r : R)
  (a : A),
  (∀ x ∈ spectrum R a, r ≤ f x) →
    autoParam (ContinuousOn f (spectrum R a)) algebraMap_le_cfc._auto_1 →
      autoParam (p a) algebraMap_le_cfc._auto_3 → (algebraMap R A) r ≤ cfc f a
-- Mathlib.Data.EReal.Basic
EReal.bot_lt_coe : ∀ (x : ℝ), ⊥ < ↑x
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Divides the `i`-th row by `coef`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.divideRow : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → ℕ → ℚ → α n m
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_mk : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : MultilinearMap R (fun x => M) N)
  (h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0),
  ⇑{ toMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f
-- Std.Data.DHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.DHashMap.wf : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (self : Std.DHashMap α β), self.inner.WF
-- Mathlib.AlgebraicGeometry.Limits
/-- The sections on coproducts of schemes are the (categorical) product of the sections
on the components  -/
AlgebraicGeometry.Scheme.coprodPresheafObjIso : {X Y : AlgebraicGeometry.Scheme} →
  (U : (X ⨿ Y).Opens) →
    (X ⨿ Y).presheaf.obj (Opposite.op U) ≅
      X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⨯
        Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U))
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P Q : CategoryTheory.MorphismProperty C)
  [P.RespectsLeft Q] [P.RespectsRight Q], P.Respects Q
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.equivFunctor_symm_apply : ∀ (C D : CategoryTheory.Cat) (a : CategoryTheory.Functor ↑C ↑D),
  (CategoryTheory.Cat.Hom.equivFunctor C D).symm a = a.toCatHom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- The canonical isomorphism from the opposite of an abstract coproduct to the corresponding product
in the opposite category.
 -/
CategoryTheory.Limits.opCoproductIsoProduct' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      {Z : α → C} →
        {c : CategoryTheory.Limits.Cofan Z} →
          {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit f → (Opposite.op c.pt ≅ f.pt)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getValueCastD k (Std.Internal.List.insertList l toInsert) fallback =
      Std.Internal.List.getValueCastD k l fallback
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_le_unop_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] {S₁ S₂ : Subring Rᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The norm function determined by a rank one valuation on a field `L`.  -/
Valuation.norm : {L : Type u_1} →
  [inst : Field L] →
    {Γ₀ : Type u_2} → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation L Γ₀) → [hv : v.RankOne] → L → ℝ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If `f : M → M'` has injective differential at `x` within `s`,
it is `MDifferentiable` at `x` within `s`.  -/
mdifferentiableWithinAt_of_mfderivWithin_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  Function.Injective ⇑(mfderiv[s] f x) → MDiffAt[s] f x
-- Lean.Expr
Lean.reflBoolFalse : Lean.Expr
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If a vector space is `FiniteDimensional`, `Basis.ofVectorSpace` is indexed by
a finite type.  -/
FiniteDimensional.instFintypeElemOfVectorSpaceIndex : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → Fintype ↑(Module.Basis.ofVectorSpaceIndex K V)
-- Std.Time.DateTime
/-- Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week
and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
The week-based year may differ from the calendar year for dates near the start or end of the year.
 -/
Std.Time.DateTime.weekYear : Std.Time.DateTime →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.DateTime.weekOfYear._proof_1) →
      Std.Time.Year.Offset
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.mem_iInf : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_3} {S : ι → AddSubsemigroup M} {x : M}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Algebra.Homology.ExactSequence
/-- the composition of two consecutive arrows is zero  -/
CategoryTheory.ComposableArrows.IsComplex.zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.IsComplex →
    ∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.IsComplex._auto_1),
      CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0
-- Mathlib.Analysis.Real.Spectrum
coe_mem_spectrum_real_of_nonneg : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : PartialOrder A] [inst_2 : Algebra ℝ A] [NonnegSpectrumClass ℝ A] {a : A}
  {x : NNReal}, autoParam (0 ≤ a) coe_mem_spectrum_real_of_nonneg._auto_1 → (↑x ∈ spectrum ℝ a ↔ x ∈ spectrum NNReal a)
-- Mathlib.Data.PFun
/-- The monad `map` function, pointwise `Part.map`  -/
PFun.map : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (β → γ) → (α →. β) → α →. γ
-- Init.Data.UInt.Lemmas
UInt16.mul_zero : ∀ {a : UInt16}, a * 0 = 0
-- Mathlib.Algebra.Lie.Subalgebra
Submodule.exists_lieSubalgebra_coe_eq_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (p : Submodule R L),
  (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_map_toDual`. -/
List.SortedGT.of_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, l.SortedGT → (List.map (⇑OrderDual.toDual) l).SortedLT