mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instVAddCommClassForall_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : VAdd M α] [inst_1 : VAdd N β],
  VAddCommClass N Mᵈᵃᵃ (α → β)
-- Mathlib.Order.OrderDual
/-- Recursor for `αᵒᵈ`.  -/
OrderDual.rec : {α : Type u_1} → {motive : αᵒᵈ → Sort u_2} → ((a : α) → motive (OrderDual.toDual a)) → (a : αᵒᵈ) → motive a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopId_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Functor.unopId C).inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.not_linearIndependent_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} [inst_3 : Fintype ι], ¬LinearIndependent R v ↔ ∃ g, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The maximum degree of all vertices (and `0` if there are no vertices).
The key properties of this are given in `exists_maximal_degree_vertex`, `degree_le_maxDegree`
and `maxDegree_le_of_forall_degree_le`.  -/
SimpleGraph.maxDegree : {V : Type u_1} → (G : SimpleGraph V) → [Fintype V] → [DecidableRel G.Adj] → ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instAddCommGroup : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Affine F} → [DecidableEq F] → AddCommGroup W.Point
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (v : ShrinkingLemma.PartialRefinement u s p) (i : ι), v.toFun i ⊆ u i
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
  N.FG ↔ ∃ n s, (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N
-- Mathlib.Order.Filter.CardinalInter
Filter.mem_ofCardinalInter : ∀ {α : Type u} {c : Cardinal.{u}} {l : Set (Set α)} (hc : 2 < c)
  (hl : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l)
  {s : Set α}, s ∈ Filter.ofCardinalInter l hc hl h_mono ↔ s ∈ l
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_neg : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R), v (-x) = v x
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMul : {α : Type u_1} → [Mul α] → Mul αᵒᵈ
-- Mathlib.Algebra.Group.Units.Basic
RightCancelMonoid.mul_ne_one : ∀ {α : Type u} [inst : RightCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
-- Mathlib.Algebra.Notation.Pi.Defs
Function.vadd_const : ∀ {ι : Type u_1} {M : Type u_7} {α : Type u_2} [inst : VAdd α M] (b : α) (a : M),
  b +ᵥ Function.const ι a = Function.const ι (b +ᵥ a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_pi_div_two_sub : ∀ (x : ℂ), Complex.cos (↑Real.pi / 2 - x) = Complex.sin x
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.mem_sup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α}
  {x : α → M}, x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  (f : G ⟶ H), f⁻¹.hom.hom = f.hom.hom⁻¹
-- Mathlib.Order.Fin.Tuple
strictMono_vecEmpty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, StrictMono ![a]
-- Lean.Meta.Closure
Lean.Meta.Closure.Context.mk : Bool → Lean.Meta.Closure.Context
-- Init.Data.SInt.Lemmas
Int16.toInt64_ofNat : ∀ {n : ℕ}, n ≤ 32767 → (OfNat.ofNat n).toInt64 = OfNat.ofNat n
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.constantCoeff_logOf : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] {f : PowerSeries A},
  PowerSeries.constantCoeff f = 1 → PowerSeries.constantCoeff f.logOf = 0
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instInfSet : {α : Type u_1} → [inst : LE α] → InfSet (LowerSet α)
-- Mathlib.Data.ENNReal.Basic
ENNReal.cinfi_ne_top : ∀ {α : Type u_1} [inst : InfSet α] (f : ENNReal → α), ⨅ x, f ↑x = ⨅ x, f ↑x
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_strictMono : StrictMono Cardinal.beth
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKeyD.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback)
  (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (fallback : α),
  x = Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 →
    x_1 = fallback →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
          fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) ≍
        h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insertIfNew k v}, (t.insertIfNew k v)[a] = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.coe_toNNReal_ae_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  (∀ᵐ (x : α) ∂μ, f x < ⊤) → (fun x => ↑(f x).toNNReal) =ᵐ[μ] f
-- Mathlib.RingTheory.PowerSeries.Catalan
PowerSeries.catalanSeries_coeff : ∀ (n : ℕ), (PowerSeries.coeff n) PowerSeries.catalanSeries = catalan n
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreId_inv_app_iso_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Core C),
  ((CategoryTheory.Functor.coreId C).inv.app X).iso.hom = CategoryTheory.CategoryStruct.id X.of
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Every nonzero element of a group with zero is invertible.  -/
CommGroupWithZero.mul_inv_cancel : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀] (a : G₀), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPathConnected_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 < r → IsPathConnected (Metric.ball x r)
-- Init.Data.List.Basic
List.length_cons : ∀ {α : Type u} {a : α} {as : List α}, (a :: as).length = as.length + 1
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instAdd : (R : Type u) → (X : Type v) → [inst : CommRing R] → Add (FreeLieAlgebra R X)
-- Init.Meta.Defs
Lean.Syntax.instBEqPreresolved.beq : Lean.Syntax.Preresolved → Lean.Syntax.Preresolved → Bool
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- Variant of the principle of isolated zeros, formulated in terms of orders: If `f` is nowhere locally
constant zero, then its zero set is discrete within its domain of meromorphicity.
 -/
MeromorphicAt.MeromorphicOn.codiscreteWithin_setOfPred_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  MeromorphicOn f U → (∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) → ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).get? k = if t₂.contains k = true then t₁.get? k else none
-- Init.Data.Vector.Attach
Vector.attachWith_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {P : α → Prop} {H : ∀ x ∈ Vector.mk xs h, P x},
  (Vector.mk xs h).attachWith P H = Vector.mk (xs.attachWith P ⋯) ⋯
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series of a subgroup `S` of `G`, computed in the ambient group `G`.
This is the iterated commutator `⁅⁅⋯⁅S, S⁆, S⁆⋯, S⁆`, a subgroup of `G`. The lower central series
of `G` itself is the case `S = ⊤`.  -/
Subgroup.lowerCentralSeries : {G : Type u_1} → [inst : Group G] → Subgroup G → ℕ → Subgroup G
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.u_bot : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (gi : GaloisCoinsertion l u), u ⊥ = ⊥
-- Std.Http.Data.URI.Encoding
Std.Http.URI.all_of_all_of_imp : ∀ {p q : UInt8 → Bool} {b : ByteArray},
  b.data.all p = true → (∀ (c : UInt8), p c = true → q c = true) → b.data.all q = true
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- A sigma-algebra $\mathcal{A}$ and a family of random variables $(X_1, ..., X_p)$ are independent
if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$  -/
indep_comap_pi_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] [Finite S],
  m ≤ mΩ →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
              ∫ (ω : Ω) in A, f fun x => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X x ω ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap (fun ω s => X s ω) MeasurableSpace.pi) P
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_one : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : One M], sInf 1 = 1
-- Mathlib.Algebra.Lie.Graded
/-- A class that ensures a bracket product preserves an additive grading.  -/
SetLike.GradedBracket : {ι : Type u_1} → {σ : Type u_2} → {L : Type u_4} → [SetLike σ L] → [Bracket L L] → [Add ι] → (ι → σ) → Prop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.modifyKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : β k → β k)
  (l : List ((a : α) × β a)),
  Std.Internal.List.modifyKey k f l =
    match Std.Internal.List.getValueCast? k l with
    | none => l
    | some v => Std.Internal.List.replaceEntry k (f v) l
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList.eq_def : ∀ (x : ℕ),
  x.primeFactorsList =
    match x with
    | 0 => []
    | 1 => []
    | k.succ.succ =>
      have m := (k + 2).minFac;
      m :: ((k + 2) / m).primeFactorsList
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ici : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ici ↑x = Set.Ici x
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_mul : ∀ {α : Type u_2} [inst : SeminormedAddCommGroup α] [inst_1 : Mul α] [NormMulClass α] (a b : α), ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊
-- Lean.Meta.Tactic.Simp.Types
/-- If `inDSimp := true`, then `simp` is in `dsimp` mode, and only applying
transformations that preserve definitional equality.
 -/
Lean.Meta.Simp.Context.inDSimp : Lean.Meta.Simp.Context → Bool
-- Mathlib.Control.Traversable.Equiv
Equiv.id_traverse : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t] {α : Type u}
  (x : t' α), Equiv.traverse eqv pure x = pure x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAddZeroClass.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitAddZeroClass F = { zero := Zero.zero, add := Add.add, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Topology.EMetricSpace.Weak
instWeakEMetricSpaceWithTop.eq_1 : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α] [m : WeakEMetricSpace α],
  instWeakEMetricSpaceWithTop =
    { toWeakPseudoEMetricSpace := instWeakPseudoEMetricSpaceWithTop, eq_of_edist_eq_zero := ⋯ }
-- Lean.Meta.Basic
/-- Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
 -/
Lean.Meta.Config.zetaDelta : Lean.Meta.Config → Bool
-- Mathlib.Topology.LocallyFinite
LocallyFinite.option_elim' : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → ∀ (s : Set X), LocallyFinite (Option.elim' s f)
-- Mathlib.Data.List.Cycle
/-- The length of the `s : Cycle α`, which is the number of elements, counting duplicates.  -/
Cycle.length : {α : Type u_1} → Cycle α → ℕ
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddMonoid.enorm_add_le : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedAddMonoid E] (x y : E), ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (a : αᵒᵈ), (CompleteLatticeHom.dual f) a = OrderDual.toDual (f (OrderDual.ofDual a))
-- Mathlib.Order.Filter.Pointwise
Filter.smul_tendsto_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : GroupWithZero γ] [inst_1 : MulAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, c ≠ 0 → (Filter.Tendsto (c • m) f (c • g) ↔ Filter.Tendsto m f g)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.le_expGrowthSup_comp : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  Monotone u →
    (LinearGrowth.linearGrowthInf fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup (u ∘ v)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus : ∀ {R : CommRingCat} (s : Set ↑R),
  (AlgebraicGeometry.Spec R).zeroLocus
      (⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) '' s) =
    PrimeSpectrum.zeroLocus s
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- If `C` has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
taking the colimit of the diagram formed by the coproducts of finite sets over the indexing type.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] →
          (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) → CategoryTheory.Limits.ColimitCocone F
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
/-- The triangle `triangleOfSES` attached to a short exact sequence `S` of cochain
complexes is isomorphic to the standard distinguished triangle associated to
the morphism `S.f`.  -/
DerivedCategory.triangleOfSESIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} →
          (hS : S.ShortExact) →
            DerivedCategory.triangleOfSES hS ≅
              DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.sInf_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s : Set M.Submodule) (X : Cᵒᵖ), (sInf s).obj X = ⨅ N ∈ s, N.obj X
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_submatrix_submatrix : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} {p' : Type u_18} (f : α → β → γ) (A : Matrix l m α)
  (B : Matrix n p β) (r : l' → l) (c : m' → m) (r' : n' → n) (c' : p' → p),
  Matrix.kroneckerMap f (A.submatrix r c) (B.submatrix r' c') =
    (Matrix.kroneckerMap f A B).submatrix (Prod.map r r') (Prod.map c c')
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.containsThenInsertIfNew a b).2).buckets).Perm
        (Std.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α},
      Std.DHashMap.Raw.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Raw.Const.get? m a
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.eulerPoint.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.eulerPoint i = (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) +ᵥ s.mongePoint
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.smul_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {R : Type u_5} [inst_3 : SMulZeroClass R β] [inst_4 : ContinuousConstSMul R β] (r : R)
  (f : CompactlySupportedContinuousMap α β) (x : α), (r • f) x = r • f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey! k =
        if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else default
-- Mathlib.Topology.ContinuousMap.Star
/-- The functorial map taking `f : C(X, Y)` to `C(Y, A) →⋆ₐ[𝕜] C(X, A)` given by pre-composition
with the continuous function `f`. See `ContinuousMap.compMonoidHom'` and
`ContinuousMap.compAddMonoidHom'`, `ContinuousMap.compRightAlgHom` for bundlings of
pre-composition into a `MonoidHom`, an `AddMonoidHom` and an `AlgHom`, respectively, under
suitable assumptions on `A`.  -/
ContinuousMap.compStarAlgHom' : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (𝕜 : Type u_4) →
          [inst_2 : CommSemiring 𝕜] →
            (A : Type u_5) →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : Semiring A] →
                  [inst_5 : IsTopologicalSemiring A] →
                    [inst_6 : Star A] →
                      [inst_7 : ContinuousStar A] → [inst_8 : Algebra 𝕜 A] → C(X, Y) → C(Y, A) →⋆ₐ[𝕜] C(X, A)
-- Mathlib.Topology.Continuous
/-- A version of `Continuous.tendsto` that allows one to specify a simpler form of the limit.
E.g., one can write `continuous_exp.tendsto' 0 1 exp_zero`.  -/
Continuous.tendsto' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (x : X) (y : Y), f x = y → Filter.Tendsto f (nhds x) (nhds y)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mapRelations_mapGenerators : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  CategoryTheory.CategoryStruct.comp (P.mapRelations F η) (P.mapGenerators F η) = 0
-- Mathlib.Combinatorics.Configuration
/-- If a nondegenerate configuration has a unique point on any two lines, and if `|P| = |L|`,
then there is a unique line through any two points.  -/
Configuration.HasPoints.hasLines : {P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      [Configuration.HasPoints P L] →
        [inst_2 : Fintype P] → [inst_3 : Fintype L] → Fintype.card P = Fintype.card L → Configuration.HasLines P L
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.brecOn : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop} {n : ℕ} {a : List.Vector ℕ n → ℕ}
  (t : Nat.Primrec' a),
  (∀ {n : ℕ} (a : List.Vector ℕ n → ℕ) (t : Nat.Primrec' a), Nat.Primrec'.below t → motive a t) → motive a t
-- Qq.AssertInstancesCommute
Qq.Impl.termAssertInstancesCommuteDummy : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
        (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).hom)
-- Init.Data.UInt.Lemmas
UInt8.le_antisymm_iff : ∀ {a b : UInt8}, a = b ↔ a ≤ b ∧ b ≤ a
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_eq_eraseIdx.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (i : ℕ) (h_1 : Unit → motive none) (h_2 : (i : ℕ) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.getSymbols : {α : Type} → [self : Lean.Meta.Grind.TheoremLike α] → α → List Lean.HeadIndex