mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the positive naturals then they are
equal.  -/
MonoidWithZeroHomClass.ext_nnrat_on_pnat : ∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ≥0 M₀]
  [MonoidWithZeroHomClass F ℚ≥0 M₀] {f g : F}, (∀ (n : ℕ), 0 < n → f ↑n = g ↑n) → f = g
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
/-- Convert a sequence of binary digits to a real number from `unitInterval`.  -/
Real.fromBinary : (ℕ → Bool) → ↑unitInterval
-- Lean.Elab.MutualDef
/-- A mapping from FVarId to Set of FVarIds.  -/
Lean.Elab.Term.MutualClosure.UsedFVarsMap : Type
-- Mathlib.GroupTheory.CoprodI
/-- The inverse of a non-empty reduced word  -/
Monoid.CoprodI.NeWord.inv : {ι : Type u_1} →
  {G : ι → Type u_4} →
    [inst : (i : ι) → Group (G i)] → {i j : ι} → Monoid.CoprodI.NeWord G i j → Monoid.CoprodI.NeWord G j i
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inlAlgHom_apply : ∀ (S : Type u_1) (R : Type u) (M : Type v) [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] (r : R),
  (TrivSqZeroExt.inlAlgHom S R M) r = TrivSqZeroExt.inl r
-- Mathlib.Algebra.Order.Hom.Units
OrderMonoidIso.val_unitsCongr_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : Preorder β] [inst_3 : Monoid β]
  (e : α ≃*o β) (a : αˣ), ↑(e.unitsCongr a) = e ↑a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.unop_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.unop.h₂ = h.h₁.unop
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusLift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η η_1 : P ⟶ Q), η = η_1 → ∀ (hQ : CategoryTheory.Presheaf.IsSheaf J Q), J.plusLift η hQ = J.plusLift η_1 hQ
-- Mathlib.NumberTheory.Bernoulli
/-- The exponential generating function for the Bernoulli numbers `bernoulli n`.  -/
bernoulliPowerSeries : (A : Type u_1) → [inst : CommRing A] → [Algebra ℚ A] → PowerSeries A
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_empty : ∀ {V : Type u_1} {G : SimpleGraph V}, G.deleteEdges ∅ = G
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_add : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.FiniteMeasure Ω), ↑(μ + ν) = ↑μ + ↑ν
-- Init.Data.Ord.Basic
Ordering.isEq_eq : Ordering.eq.isEq = true
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instMax : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Max hI.SubDPIdeal
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_α_hom : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z⟧ = (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.CategoryTheory.MorphismProperty.Descent
/-- `P` descends along `Q` if whenever `Q` holds for `X ⟶ Z`,
`P` holds for `X ×[Z] Y ⟶ X` implies `P` holds for `Y ⟶ Z`.  -/
CategoryTheory.MorphismProperty.DescendsAlong : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.BitVec.Lemmas
BitVec.zero_shiftLeft : ∀ {w : ℕ} (n : ℕ), 0#w <<< n = 0#w
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The arrow itself.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → (self : S.Arrow) → self.Y ⟶ X
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.instUniquePathRoot : {V : Type u} → [inst : Quiver V] → [inst_1 : Quiver.Arborescence V] → (b : V) → Unique (Quiver.Path (Quiver.root V) b)
-- Mathlib.Topology.ContinuousOn
Continuous.preimage_mem_nhdsSetWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → ∀ {s u s' : Set β}, u ∈ nhdsSetWithin s s' → f ⁻¹' u ∈ nhdsSetWithin (f ⁻¹' s) (f ⁻¹' s')
-- Init.Grind.Order
Lean.Grind.Order.le_eq_true_of_lt_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k₁ k₂ : ℤ},
  k₁.ble' k₂ = true → a < b + ↑k₁ → (a ≤ b + ↑k₂) = True
-- Mathlib.Algebra.Torsor.Basic
smul_eq_smul_iff_div_eq_sdiv : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] {v₁ v₂ : G} {p₁ p₂ : P},
  v₁ • p₁ = v₂ • p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂
-- Mathlib.Order.Filter.Map
Filter.bind_def : ∀ {α β : Type u_6} (f : Filter α) (m : α → Filter β), f >>= m = f.bind m
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkAtomCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (n : α) (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false),
  { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.mkAtomCached n =
    match cache.get? (Std.Sat.AIG.Decl.atom n) with
    | some hit =>
      { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst },
        ref := { gate := hit.idx, invert := false, hgate := ⋯ } }
    | none =>
      let g := decls.size;
      have cache_1 := Std.Sat.AIG.Cache.insert decls cache (Std.Sat.AIG.Decl.atom n);
      let decls_1 := decls.push (Std.Sat.AIG.Decl.atom n);
      have hdag := ⋯;
      have hzero' := ⋯;
      have hconst := ⋯;
      { aig := { decls := decls_1, cache := cache_1, hdag := hdag, hzero := hzero', hconst := hconst },
        ref := { gate := g, invert := false, hgate := ⋯ } }
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.counit_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A), CoalgebraStruct.counit (LaurentPolynomial.C a) = CoalgebraStruct.counit a
-- Mathlib.Data.Set.Function
Set.InjOn.exists_subset_injOn_subset_range_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {r : Set α},
  Set.InjOn f r → r ⊆ s → ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ Set.InjOn f u
-- Mathlib.Data.List.Sort
List.SortedGT.eq_of_mem_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α},
  l₁.SortedGT → l₂.SortedGT → (∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) → l₁ = l₂
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instCharP : ∀ {q : ℕ}, CharP (LucasLehmer.X q) q
-- Init.PropLemmas
exists_eq_right : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, p a ∧ a = a') ↔ p a'
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.injective_eq_monomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).PreservesMonomorphisms],
  CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.instPreorderCover : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) → (X : C) → Preorder (J.Cover X)
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} →
                (L ⊣ F) → (F ⊣ G) → (G ⊣ R) → CategoryTheory.Adjunction.Quadruple L F G R
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsReflexivePair.common_section : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g],
  ∃ s,
    CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧
      CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
-- Mathlib.Algebra.Group.End
Equiv.mulRight_one : ∀ {α : Type u_4} [inst : Group α], Equiv.mulRight 1 = 1
-- Lean.Meta.Tactic.Split
Lean.Meta.splitLocalDecl? : Lean.MVarId → Lean.FVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        h_1) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
          h_1))
-- Init.Data.Order.Factories
/-- Returns a `LawfulOrderMax α` instance given certain properties.

This lemma derives a `LawfulOrderMax α` instance from two properties involving `LE α` and `Max α`
instances.

The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
Std.LawfulOrderMax.of_max_le_iff : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α],
  autoParam (∀ (a b c : α), a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c) Std.LawfulOrderMax.of_max_le_iff._auto_1 →
    autoParam (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) Std.LawfulOrderMax.of_max_le_iff._auto_3 → Std.LawfulOrderMax α
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.mk.sizeOf_spec : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] (toMulHom : R →ₙ* S) (nonneg' : ∀ (x : R), 0 ≤ toMulHom.toFun x)
  (eq_zero' : ∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0)
  (add_le' : ∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y),
  sizeOf { toMulHom := toMulHom, nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' } = 1 + sizeOf toMulHom
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of a polynomial is smaller than its degree.  -/
Polynomial.natSepDegree_le_natDegree : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree ≤ f.natDegree
-- Init.Data.Rat.Lemmas
Rat.instLawfulIdentityHAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Data.Finsupp.Basic
Int.cast_finsupp_sum : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : AddCommGroupWithOne R]
  (g : α → M → ℤ), ↑(f.sum g) = f.sum fun a b => ↑(g a b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.sinh` is real analytic.  -/
Real.analyticAt_sinh : ∀ {x : ℝ}, AnalyticAt ℝ Real.sinh x
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A version of the layer cake formula for bounded continuous functions which have finite integral:
`∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt`.  -/
MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral : ∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  (f : BoundedContinuousFunction α ℝ) (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] ⇑f →
    MeasureTheory.HasFiniteIntegral (⇑f) μ → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a | t ≤ f a}
-- Std.Sat.AIG.Lemmas
/-- If an index contains a `Decl.atom` we know how to denote it.
 -/
Std.Sat.AIG.denote_idx_atom : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} {assign : α → Bool} {invert : Bool} {a : α}
  {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size},
  aig.decls[start] = Std.Sat.AIG.Decl.atom a →
    ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = (assign a ^^ invert)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
/-- `support a` for `a : FreeAbelianGroup X` is the finite set of `x : X`
that occur in the formal sum `a`.  -/
FreeAbelianGroup.support : {X : Type u_1} → FreeAbelianGroup X → Finset X
-- Mathlib.Order.Filter.Pointwise
Filter.mem_neg : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α} {s : Set α}, s ∈ -f ↔ Neg.neg ⁻¹' s ∈ f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α},
      k ∉ m → l.contains k = false → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey? k = none
-- Init.Core
/-- Quotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.
 -/
Quotient : {α : Sort u} → Setoid α → Sort u
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.ge : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V → V ≤ Uᗮ
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
primitiveRoots.eq_1 : ∀ (k : ℕ) (R : Type u_7) [inst : CommRing R] [inst_1 : IsDomain R],
  primitiveRoots k R = {ζ ∈ (Polynomial.nthRoots k 1).toFinset | IsPrimitiveRoot ζ k}
-- Init.Data.UInt.Lemmas
UInt64.lt_or_le : ∀ (a b : UInt64), a < b ∨ b ≤ a
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.map_pointwise_vadd : ∀ {k : Type u_2} {V₁ : Type u_5} {P₁ : Type u_6} {V₂ : Type u_7} {P₂ : Type u_8} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁),
  AffineSubspace.map f (v +ᵥ s) = f.linear v +ᵥ AffineSubspace.map f s
-- Mathlib.CategoryTheory.Filtered.Connected
CategoryTheory.IsFilteredOrEmpty.isPreconnected : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C],
  CategoryTheory.IsPreconnected C
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_sub : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (y1 y2 : HomogeneousLocalization 𝒜 x), (y1 - y2).val = y1.val - y2.val
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (U : N) (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P =
    (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).toPresheafFiber (p.obj U)
      (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.id (p.obj U))) P
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Init.Data.Int.Pow
Int.pow_pos : ∀ {n : ℤ} {m : ℕ}, 0 < n → 0 < n ^ m
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.subtype : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (p : X → Prop), IsUltrametricDist (Subtype p)
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is monotone if `a ≤ b` implies `f a ≤ f b`.  -/
Monotone : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Init.Data.String.Lemmas.StringOrder
String.le_antisymm : ∀ {a b : String}, a ≤ b → b ≤ a → a = b
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Iic_eq_of_Icc_zero_eq : ∀ {n : ℕ} {s : Finset ℕ}, Finset.Icc 0 n = s → Finset.Iic n = s
-- Mathlib.Condensed.Solid
/-- The predicate on condensed `R`-modules describing the property of being solid.

TODO: This is not the correct definition of solid `R`-modules for a general `R`. The correct one is
as follows: Use this to define solid modules over a finite type `ℤ`-algebra `R`. In particular this
gives a definition of solid modules over `ℤ[X]` (polynomials in one variable). Then a solid
`R`-module over a general ring `R` is the condition that for every `r ∈ R` and every ring
homomorphism `ℤ[X] → R` such that `X` maps to `r`, the underlying `ℤ[X]`-module is solid.
 -/
CondensedMod.IsSolid : (R : Type (u + 1)) → [inst : Ring R] → CondensedMod R → Prop
-- Lean.Structure
Lean.instInhabitedStructureParentInfo : Inhabited Lean.StructureParentInfo
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Given a.e. strongly measurable functions `f` and `g`, `edist f g` is measurable.

Note that this lemma proves a.e. measurability, **not** a.e. strong measurability.
This is an intentional decision: for functions taking values in ℝ≥0∞,
a.e. measurability is much more useful than a.e. strong measurability.  -/
MeasureTheory.AEStronglyMeasurable.edist : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : PseudoMetricSpace β]
  {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → AEMeasurable (fun a => edist (f a) (g a)) μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, k ∈ Std.ExtDHashMap.ofList l ↔ (List.map Sigma.fst l).contains k = true
-- Init.Data.BitVec.Lemmas
BitVec.fill_toFin : ∀ {w : ℕ} {v : Bool}, (BitVec.fill w v).toFin = if v = true then (BitVec.allOnes w).toFin else Fin.ofNat (2 ^ w) 0
-- Mathlib.LinearAlgebra.Lagrange
/-- This defines the nodal weight for a given set of node indexes and node mapping function `v`.  -/
Lagrange.nodalWeight : {F : Type u_1} → [Field F] → {ι : Type u_2} → [DecidableEq ι] → Finset ι → (ι → F) → ι → F
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- A version of `Matrix.toLin' A` that produces linear equivalences.  -/
Matrix.SpecialLinearGroup.toLin' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Matrix.SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R
-- Init.ShareCommon
ShareCommon.instNonemptyStateFactory : Nonempty ShareCommon.StateFactory
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₃ =
    CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.left φ)
-- Mathlib.Combinatorics.Derangements.Basic
/-- If `α` is equivalent to `β`, then `derangements α` is equivalent to `derangements β`.  -/
Equiv.derangementsCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → ↑(derangements α) ≃ ↑(derangements β)
-- Std.Do.SPred.Laws
_private.Std.Do.SPred.Laws.0.Std.Do.SPred.entails.match_1.splitter : (motive : (σs : List (Type u_1)) → Std.Do.SPred σs → Std.Do.SPred σs → Sort u_2) →
  (σs : List (Type u_1)) →
    (P Q : Std.Do.SPred σs) →
      ((P Q : Std.Do.SPred []) → motive [] P Q) →
        ((σ : Type u_1) → (tail : List (Type u_1)) → (P Q : Std.Do.SPred (σ :: tail)) → motive (σ :: tail) P Q) →
          motive σs P Q
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k k' fallback : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKeyD k' fallback = k
-- Std.Do.Triple.SpecLemmas
modifyThe.eq_1 : ∀ (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m] (f : σ → σ),
  modifyThe σ f = MonadStateOf.modifyGet fun s => (PUnit.unit, f s)
-- Mathlib.CategoryTheory.Square
/-- the left morphism  -/
CategoryTheory.Square.f₁₃ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Square C) → self.X₁ ⟶ self.X₃
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.star_mono : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A], Monotone star
-- Mathlib.Order.Sublocale
Sublocale.instPartialOrder : {X : Type u_1} → [inst : Order.Frame X] → PartialOrder (Sublocale X)
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
cases we have a computable `floor` function.  -/
Archimedean.floorRing : (R : Type u_5) → [inst : Ring R] → [inst_1 : LinearOrder R] → [IsStrictOrderedRing R] → [Archimedean R] → FloorRing R