mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Auxiliary definition for `final_functor`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ →
          J → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Batteries.Data.Float.Lemmas
Float.beq_self_iff : ∀ {f : Float}, (f == f) = true ↔ f ≠ Float.nan
-- Init.Data.Option.Lemmas
Option.map_id' : ∀ {α : Type u_1} {x : Option α}, Option.map (fun a => a) x = x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofAlgEquiv_symm : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃ₐ[R] B)
  (map_star : ∀ (x : A), f (star x) = star (f x)),
  (StarAlgEquiv.ofAlgEquiv f map_star).symm = StarAlgEquiv.ofAlgEquiv f.symm ⋯
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalNonAssocCommSemiring` instance along an injective function.  -/
Function.Injective.nonUnitalNonAssocCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalNonAssocCommSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : S), f (x + y) = f x + f y) →
                      (∀ (x y : S), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → NonUnitalNonAssocCommSemiring S
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C)
  (h : CategoryTheory.Limits.IsColimit sq.pushoutCocone), sq.IsPushout
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
hasFDerivAt_polarCoord_symm : ∀ (p : ℝ × ℝ), HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)}
    (PresheafOfModules.evaluation R X)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Mathlib.RingTheory.Nakayama
/-- **Nakayama's Lemma** - Statement (4) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson` for a generalisation
to the `jacobson` of any ideal  -/
Submodule.smul_le_of_le_smul_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' : Submodule R M}, N'.FG → I ≤ ⊥.jacobson → N' ≤ N ⊔ I • N' → I • N' ≤ N
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.limitsOfShape J ≤ Q.limitsOfShape J
-- Mathlib.Data.Sum.Order
WithBot.orderIsoPUnitSumLex_symm_inl : ∀ {α : Type u_1} [inst : LE α] (x : PUnit.{u_4 + 1}), WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inl x)) = ⊥
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMin'.eq_1 : ∀ {α : Type u_1} (x : α) (x_1 : Ordnode α), Ordnode.nil.splitMin' x x_1 = (x, x_1)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else' : ∀ {w : ℕ} (c : Bool) (t e : BitVec w), (e == bif c then t else e) = (!c || t == e)
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_counitIso : ∀ (α : Type u),
  (Types.monoOverEquivalenceSet α).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Data.Ordmap.Ordset
Ordset.instEmptyCollection : {α : Type u_1} → [inst : Preorder α] → EmptyCollection (Ordset α)
-- Lean.Data.Json.Basic
Lean.Json.instCoeInt : Coe ℤ Lean.Json
-- Mathlib.Analysis.Normed.Group.Basic
ofReal_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ
-- Mathlib.Dynamics.Flow
/-- The identity map as a constant flow.  -/
Flow.id : (τ : Type u_1) →
  (α : Type u_2) → [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddZero τ] → Flow τ α
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_mul_div : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → a = a * b * (1 / b)
-- Init.Data.List.MapIdx
List.mapIdx.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (as : List α), List.mapIdx f as = List.mapIdx.go f as #[]
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α} {fallback : β a}, m.getD a fallback = Std.DHashMap.Internal.Raw₀.getD ⟨m, ⋯⟩ a fallback
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Encodable.decodeSum.match_1.splitter : (motive : Bool → ℕ → Sort u_1) →
  (x : Bool) →
    (x_1 : ℕ) → ((m : ℕ) → motive false m) → ((x : Bool) → (m : ℕ) → (x = false → False) → motive x m) → motive x x_1
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_filterₘ : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  (Std.DHashMap.Internal.toListModel (↑(m.filterₘ f)).buckets).Perm
    (List.filter (fun p => f p.fst p.snd) (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_iff_of_not_isMax' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax b → (Order.succ a ≤ b ↔ a < b)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] {W : C}
  (i j : CategoryTheory.Limits.multicoequalizer I ⟶ W),
  (∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j) →
    i = j
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.one_le_cosh : ∀ (x : ℝ), 1 ≤ Real.cosh x
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_eq_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance X Y μ = ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.orderIsoOfIso_apply : ∀ {α β : PartOrdEmb} (e : α ≅ β) (a : ↑α),
  (PartOrdEmb.orderIsoOfIso e) a = (CategoryTheory.ConcreteCategory.hom e.hom) a
-- Mathlib.Algebra.Order.Module.Defs
MulPosMono.toSMulPosMono : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [MulPosMono α], SMulPosMono α α
-- Mathlib.Data.TypeVec
/-- `RelLast α r x y` says that `p` the last elements of `x y : α.append1 β` are related by `r` and
all the other elements are equal.  -/
TypeVec.RelLast : {n : ℕ} → (α : TypeVec.{u} n) → {β γ : Type u} → (β → γ → Prop) → ⦃i : Fin2 (n + 1)⦄ → (α ::: β) i → (α ::: γ) i → Prop
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.comap_ne_bot`. -/
Ideal.IsIntegralClosure.comap_ne_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, I ≠ ⊥ → Ideal.comap (algebraMap R A) I ≠ ⊥
-- Init.Data.Fin.Lemmas
Fin.reverseInduction.go.eq_def : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1))
  (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x : motive ⟨j, h⟩),
  Fin.reverseInduction.go cast i j h h2 x =
    if hi : ↑i = j then _root_.cast ⋯ x
    else
      match j, h, h2, x, hi with
      | 0, h, h2, x, hi => ⋯.elim
      | j.succ, h, h2, x, hi => Fin.reverseInduction.go cast i j ⋯ ⋯ (cast ⟨j, ⋯⟩ x)
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.finInsepDegree_le_of_left_le : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {E₁ E₂ : IntermediateField F K},
  E₁ ≤ E₂ → ∀ [Module.Finite (↥E₁) K], Field.finInsepDegree (↥E₂) K ≤ Field.finInsepDegree (↥E₁) K
-- Init.PropLemmas
peirce' : ∀ {a : Prop}, (∀ (b : Prop), (a → b) → a) → a
-- Std.Http.Data.Chunk
/-- Attempts to create an `ExtensionValue` from a `String`, returning `none` if the string contains
characters that cannot be encoded as an HTTP quoted-string.
 -/
Std.Http.Chunk.ExtensionValue.ofString? : String → Option Std.Http.Chunk.ExtensionValue
-- Mathlib.Order.Bounds.Basic
OrderBot.lowerBounds_univ : ∀ {γ : Type u_3} [inst : PartialOrder γ] [inst_1 : OrderBot γ], lowerBounds Set.univ = {⊥}
-- Std.Async.Process
/-- Represents resource usage statistics for a process or thread.
All time values are in milliseconds.
 -/
Std.IO.Process.ResourceUsageStats : Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
rel_act_of_rel_of_rel_act : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] [IsTrans N r] (m : M)
  {a b c : N}, r a b → r c (μ m a) → r c (μ m b)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), {x} - Metric.ball y δ = Metric.ball (x - y) δ
-- Mathlib.Order.Category.HeytAlg
HeytAlg.mk : (carrier : Type u_1) → [str : HeytingAlgebra carrier] → HeytAlg
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_mul_le_right : ∀ {R : Type u} [inst : CommSemiring R] (f g : R), PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen g
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.SpecMap_iff : ∀ {R S : CommRingCat} {φ : R ⟶ S},
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_lcm_mul_left_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), lcm m n ∣ lcm m (k * n)
-- Mathlib.Order.Filter.Basic
Filter.union_mem_sup : ∀ {α : Type u} {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s ∪ t ∈ f ⊔ g
-- Mathlib.Data.List.Infix
List.take_isPrefix_take : ∀ {α : Type u_1} {l : List α} {m n : ℕ}, List.take m l <+: List.take n l ↔ m ≤ n ∨ l.length ≤ n
-- Mathlib.Topology.LocallyFinsupp
/-- If `V` is a subset of `U`, then functions with locally finite support within `U` restrict to
functions with locally finite support within `V`, by setting their values to zero outside of `V`.
 -/
Function.locallyFinsuppWithin.restrict : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : Zero Y] → {V : Set X} → Function.locallyFinsuppWithin U Y → V ⊆ U → Function.locallyFinsuppWithin V Y
-- Mathlib.Analysis.Complex.AbsMax
/-- If `f` is differentiable on the open unit ball `{z : ℂ | ‖z‖ < 1}`, and `‖f‖` attains a maximum
in this open ball, then `f` is constant.  -/
Complex.eq_const_of_exists_max : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {b : ℝ},
  DifferentiableOn ℂ f (Metric.ball 0 b) →
    ∀ {v : E},
      v ∈ Metric.ball 0 b →
        IsMaxOn (norm ∘ f) (Metric.ball 0 b) v → Set.EqOn f (Function.const E (f v)) (Metric.ball 0 b)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.image_mem_edgeSet_image : ∀ {α : Type u_1} {β : Type u_2} {e : Set α} {H : Hypergraph α} {f : α → β}, e ∈ H.edgeSet → f '' e ∈ (H.image f).edgeSet
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
Profinite.NobelingProof.GoodProducts.P0 : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I], Profinite.NobelingProof.P I 0
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_equivSentence_symm_con : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {α : Type u'} [inst_1 : (L.withConstants α).Structure M]
  [(L.lhomWithConstants α).IsExpansionOn M] (φ : (L.withConstants α).Sentence),
  ((FirstOrder.Language.Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ M ⊨ φ
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.triangleRotation_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.triangleRotation C).inverse = CategoryTheory.Pretriangulated.invRotate C
-- Lean.Data.Json.Basic
Lean.Json.num : Lean.JsonNumber → Lean.Json
-- Mathlib.Order.Category.Frm
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
Frm.Hom.Simps.hom : (X Y : Frm) → X.Hom Y → FrameHom ↑X ↑Y
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasEigenvalue.pow : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasEigenvalue μ → ∀ (n : ℕ), (f ^ n).HasEigenvalue (μ ^ n)
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_mul : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀),
  (Function.support fun x => f x * g x) = Function.support f ∩ Function.support g
-- Mathlib.RingTheory.IdealFilter.Topology
IdealFilter.ringFilterBasis_sets : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} [inst_1 : F.IsUniform],
  IdealFilter.ringFilterBasis.sets = {x | ∃ I ∈ F, ↑I = x}
-- Mathlib.Order.CompleteLatticeIntervals
subset_sInf_emptyset : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : InfSet α] [inst_2 : Inhabited ↑s], sInf ∅ = default
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_div_lt : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R}, p ≠ 0 → 0 < q.degree → (p / q).degree < p.degree
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk.injEq : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂] (toLinearMap : M →ₛₗ[σ] M₂)
  (cont : autoParam (Continuous toLinearMap.toFun) ContinuousLinearMap.cont._autoParam) (toLinearMap_1 : M →ₛₗ[σ] M₂)
  (cont_1 : autoParam (Continuous toLinearMap_1.toFun) ContinuousLinearMap.cont._autoParam),
  ({ toLinearMap := toLinearMap, cont := cont } = { toLinearMap := toLinearMap_1, cont := cont_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_sub_eq_left_of_lt : ∀ {R : Type u} {n : ℕ} [inst : Ring R] {p q : Polynomial R}, q.natDegree < n → (p - q).coeff n = p.coeff n
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Coercion of an `OpenPartialHomeomorph` to function.
Note that an `OpenPartialHomeomorph` is not `DFunLike`.  -/
OpenPartialHomeomorph.instCoeFunForall : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → CoeFun (OpenPartialHomeomorph X Y) fun x => X → Y
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
separatingDual_iff_injective : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalRing R] [inst_5 : Module R V],
  SeparatingDual R V ↔ Function.Injective ⇑(ContinuousLinearMap.coeLM R).flip
-- Init.Data.List.Count
List.IsPrefix.count_le : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} (a : α), l₁ <+: l₂ → List.count a l₁ ≤ List.count a l₂
-- Mathlib.Topology.Algebra.Module.LocallyConvex
locallyConvexSpace_iff_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E],
  LocallyConvexSpace 𝕜 E ↔ (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ Convex 𝕜 s) id
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t₁ \ t₂).getKey! k = if k ∈ t₂ then default else t₁.getKey! k
-- Mathlib.Algebra.Quaternion
Quaternion.imI_equivProd_symm_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : R × R × R × R),
  ((Quaternion.equivProd R).symm a).imI = a.2.1
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cocone `c : Cocone (F ⋙ forget)`
of the underlying cocone of types, this is a cocone for `F` whose point is
`c.pt` with the supremum of the coinduced topologies by the maps `c.ι.app j`.  -/
TopCat.coconeOfCoconeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat)) → CategoryTheory.Limits.Cocone F
-- Std.Time.DateTime
Std.Time.DateTime.instHSubDuration : HSub Std.Time.DateTime Std.Time.DateTime Std.Time.Duration
-- Mathlib.Algebra.Algebra.Basic
/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
invertible when `algebraMap R A r` is.  -/
Invertible.algebraMapOfInvertibleAlgebraMap : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (f : A →ₗ[R] B) → f 1 = 1 → {r : R} → Invertible ((algebraMap R A) r) → Invertible ((algebraMap R B) r)
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedAlgebra.mem_support_iff : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜]
  [inst_6 : DecidableEq A] (r : A) (i : ι),
  i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (GradedAlgebra.proj 𝒜 i) r ≠ 0
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.map_π_apply' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F' G' : CategoryTheory.Functor J (Type v)} (α : F' ⟶ G')
  (j : J) (x : CategoryTheory.Limits.limit F'),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π G' j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limMap α)) x) =
    (CategoryTheory.ConcreteCategory.hom (α.app j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A structure giving a chosen left adjoint of a 1-morphism `right`.  -/
CategoryTheory.Bicategory.LeftAdjoint : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (b ⟶ a) → Type (max v₁ w₁)
-- Mathlib.Algebra.Field.Defs
NNRat.smul_def : ∀ {K : Type u_1} [inst : DivisionSemiring K] (q : ℚ≥0) (a : K), q • a = ↑q * a
-- Mathlib.Analysis.Calculus.TangentCone.Basic
AccPt.of_mem_tangentConeAt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space E] {y : E},
  y ∈ tangentConeAt 𝕜 s x → y ≠ 0 → AccPt x (Filter.principal s)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_bot : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.zeroLocus 𝒜 ↑⊥ = Set.univ
-- Init.Data.String.Bootstrap
String.Internal.drop : String → ℕ → String
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {c : ℝ} {f : ↥(MeasureTheory.Lp E p μ)}
  {g : ↥(MeasureTheory.Lp F p μ)}, (∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖) → ‖f‖ ≤ c * ‖g‖
-- Mathlib.Algebra.Exact.Basic
Function.Exact.iff_of_ladder_linearEquiv : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {P : Type u_6} {P' : Type u_7}
  [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid N'] [inst_5 : AddCommMonoid P] [inst_6 : AddCommMonoid P'] [inst_7 : Module R M]
  [inst_8 : Module R M'] [inst_9 : Module R N] [inst_10 : Module R N'] [inst_11 : Module R P] [inst_12 : Module R P']
  {f₁₂ : M →ₗ[R] N} {f₂₃ : N →ₗ[R] P} {g₁₂ : M' →ₗ[R] N'} {g₂₃ : N' →ₗ[R] P'} {e₁ : M ≃ₗ[R] M'} {e₂ : N ≃ₗ[R] N'}
  {e₃ : P ≃ₗ[R] P'},
  g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂ → g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃ → (Function.Exact ⇑g₁₂ ⇑g₂₃ ↔ Function.Exact ⇑f₁₂ ⇑f₂₃)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : AlgebraicGeometry.PresheafedSpace C)
  {f : X ⟶ ↑Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (Y.ofRestrict hf)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.toIsHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [self : p.IsCartesian f φ],
  p.IsHomLift f φ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instPartialOrder = PartialOrder.ofSetLike (Subsemigroup M) M
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.map_condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D)
  [G.PreservesZeroMorphisms],
  CategoryTheory.CategoryStruct.comp (G.map f) (G.map (CategoryTheory.Limits.Cofork.π c)) = 0
-- Mathlib.Analysis.Convex.Function
ConcaveOn.comp : ∀ {𝕜 : 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 : β → α}, ConcaveOn 𝕜 (f '' s) g → ConcaveOn 𝕜 s f → MonotoneOn g (f '' s) → ConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
List.prod_toFinset : ∀ {ι : Type u_1} {M : Type u_5} [inst : DecidableEq ι] [inst_1 : CommMonoid M] (f : ι → M) {l : List ι},
  l.Nodup → l.toFinset.prod f = (List.map f l).prod
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.getSyntheticMVarDecl? : Lean.MVarId → Lean.Elab.TermElabM (Option Lean.Elab.Term.SyntheticMVarDecl)