mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoIsPushout_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr'),
  CategoryTheory.CategoryStruct.comp inl' (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inl
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_fin2 : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Fin 2 → V},
  LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f], P.trW f
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A uniformly Cauchy sequence converges uniformly to its limit  -/
UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι},
  UniformCauchySeqOn F p s → (∀ x ∈ s, Filter.Tendsto (fun n => F n x) p (nhds (f x))) → TendstoUniformlyOn F f p s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : β → β}, (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G → M` satisfying the multiplicative 1-coboundary condition, produces a
1-coboundary for the representation on `Additive M` induced by the `MulDistribMulAction`.  -/
groupCohomology.coboundariesOfIsMulCoboundary₁ : {G M : Type} →
  [inst : Group G] →
    [inst_1 : CommGroup M] →
      [inst_2 : MulDistribMulAction G M] →
        {f : G → M} →
          groupCohomology.IsMulCoboundary₁ f → ↥(groupCohomology.coboundaries₁ (Rep.ofMulDistribMulAction G M))
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- `WithLp.linearEquiv` as a continuous linear equivalence.  -/
PiLp.continuousLinearEquiv : (p : ENNReal) →
  (𝕜 : Type u_1) →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [inst : Semiring 𝕜] →
          [inst_1 : (i : ι) → AddCommGroup (β i)] →
            [inst_2 : (i : ι) → Module 𝕜 (β i)] →
              [inst_3 : (i : ι) → TopologicalSpace (β i)] → PiLp p β ≃L[𝕜] (i : ι) → β i
-- Init.Data.Sum.Lemmas
Sum.comp_elim : ∀ {γ : Sort u_1} {δ : Sort u_2} {α : Type u_3} {β : Type u_4} (f : γ → δ) (g : α → γ) (h : β → γ),
  f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.instT2SpaceHomOfCarrier : ∀ {R A : CommRingCat} [inst : TopologicalSpace ↑R] [T2Space ↑R], T2Space (A ⟶ R)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_one_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (e : Topology.RelCWComplex.cell C 1),
  Topology.RelCWComplex.cellFrontier 1 e = ↑(Topology.RelCWComplex.map 1 e) '' {-1, 1}
-- Mathlib.Order.Hom.CompleteLattice
OrderIsoClass.tosInfHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [OrderIsoClass F α β], sInfHomClass F α β
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- Auxiliary definition towards the definition of the composition of morphisms
in the constructed localized category for a morphism property that has
left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasLeftCalculusOfFractions] →
        {X Y Z : C} →
          W.LeftFraction X Y → W.LeftFraction Y Z → CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Z
-- Lean.Meta.Tactic.Grind.Intro
/-- Asserts next fact in the `goal` fact queue.
Returns `true` if the queue was not empty and `false` otherwise.
 -/
Lean.Meta.Grind.Action.assertNext : Lean.Meta.Grind.Action
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The inclusion from `C` into `WithTerminal C`.  -/
CategoryTheory.WithTerminal.incl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.WithTerminal C)
-- Lean.Server.References
/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs` and collects all decls.  -/
Lean.Server.ModuleRefs.toLspModuleRefs : Lean.Server.ModuleRefs → BaseIO (Lean.Lsp.ModuleRefs × Lean.Lsp.Decls)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α) (seq : ℕ → Set β),
  Monotone seq →
    ⋃ i, seq i = Set.univ →
      ∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (nhds 1)
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Imaginary part  -/
UpperHalfPlane.im : UpperHalfPlane → ℝ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.default.injEq : ∀ (e : Lean.Expr) (source : Lean.Meta.Grind.SplitSource) (e_1 : Lean.Expr) (source_1 : Lean.Meta.Grind.SplitSource),
  (Lean.Meta.Grind.SplitInfo.default e source = Lean.Meta.Grind.SplitInfo.default e_1 source_1) =
    (e = e_1 ∧ source = source_1)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.SLAction : {R : Type u_1} → [inst : CommRing R] → [Algebra R ℝ] → MulAction (Matrix.SpecialLinearGroup (Fin 2) R) UpperHalfPlane
-- Mathlib.Data.Sum.Basic
Sum.swap_leftInverse : ∀ {α : Type u} {β : Type v}, Function.LeftInverse Sum.swap Sum.swap
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.map (self.μ.app X)) (self.μ.app X) =
    CategoryTheory.CategoryStruct.comp (self.μ.app (self.obj X)) (self.μ.app X)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_compRight : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁),
  LinearMap.BilinForm.toMatrix' (B.compRight f) = LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' f
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.utf8Decode?.go.match_1.eq_1 : ∀ (motive : Option Char → Sort u_1) (h_1 : none = none → motive none)
  (h_2 : (c : Char) → none = some c → motive (some c)),
  (match h : none with
    | none => h_1 h
    | some c => h_2 c h) =
    h_1 ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.induction_on : ∀ {α : Type u} {C : FreeGroup α → Prop} (z : FreeGroup α),
  C 1 →
    (∀ (x : α), C (FreeGroup.of x)) →
      (∀ (x : α), C (FreeGroup.of x) → C (FreeGroup.of x)⁻¹) → (∀ (x y : FreeGroup α), C x → C y → C (x * y)) → C z
-- Batteries.Data.List.Lemmas
List.modify_eq_set_get : ∀ {α : Type u_1} (f : α → α) {n : ℕ} {l : List α} (h : n < l.length), l.modify n f = l.set n (f (l.get ⟨n, h⟩))
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_range_iff : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → ((Set.range f).Infinite ↔ Infinite α)
-- Mathlib.Topology.Algebra.Order.Field
eventually_nhdsGT_zero_mul_left : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {x : 𝕜},
  0 < x →
    ∀ {p : 𝕜 → Prop}, (∀ᶠ (ε : 𝕜) in nhdsWithin 0 (Set.Ioi 0), p ε) → ∀ᶠ (ε : 𝕜) in nhdsWithin 0 (Set.Ioi 0), p (x * ε)
-- Mathlib.Algebra.Lie.Nilpotent
instIsNilpotentSubtypeMemLieSubalgebraTop : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [h : LieRing.IsNilpotent L], LieRing.IsNilpotent ↥⊤
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt8.beq_eq_decide_eq : ∀ {a b : UInt8}, (a == b) = decide (a = b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t.getKey a h = (t.getKey? a).get ⋯
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongrAddEquiv_symm_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14}
  {M₁' : Type u_15} {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₁']
  [inst_3 : Semiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂'), (e₁.arrowCongrAddEquiv e₂).symm f = (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofTop_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {h : p = ⊤} (x : ↥p), (LinearEquiv.ofTop p h) x = ↑x
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ioc_add_eq_sum_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → ∑ x ∈ Finset.Ioc a b, f x + f a = ∑ x ∈ Finset.Icc a b, f x
-- Mathlib.CategoryTheory.Shift.CommShift
/-- **Alias** of `CategoryTheory.Functor.CommShift.comp_commShiftIso_hom_app`. -/
CategoryTheory.Functor.commShiftIso_comp_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [inst_3 : AddMonoid A]
  [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A]
  [inst_7 : F.CommShift A] [inst_8 : G.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (F.comp G) a).hom.app X =
    CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
      ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X))
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_cancel' : ∀ {a b : ℤ}, a ∣ b → a * (b / a) = b
-- Mathlib.Data.Finset.Card
Finset.card_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β], (Finset.image f s).card ≤ s.card
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.isStronglyProgressive : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β}
  [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β],
  MeasureTheory.IsProgressive f u → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p : P),
  (signedDist v) p =
    ((innerSL ℝ) (NormedSpace.normalize v)).toContinuousAffineMap.comp
      (ContinuousAffineMap.id ℝ P -ᵥ ContinuousAffineMap.const ℝ P p)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_ball_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} - Metric.ball 0 δ = Metric.ball x δ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.omega_succ : ∀ {n : ZFSet.{u}}, n ∈ ZFSet.omega → insert n n ∈ ZFSet.omega
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (self.naturality g).hom
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`.  -/
AffineBasis.instSMulCommClass : ∀ {ι : Type u_1} {G : Type u_3} {G' : Type u_4} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : Group G'] [inst_5 : DistribMulAction G V]
  [inst_6 : DistribMulAction G' V] [inst_7 : SMulCommClass G k V] [inst_8 : SMulCommClass G' k V]
  [SMulCommClass G G' V], SMulCommClass G G' (AffineBasis ι k V)
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is complete iff it is satisfiable and all its models are elementarily equivalent.  -/
FirstOrder.Language.Theory.IsComplete.isComplete_iff_models_elementarily_equivalent : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), L.ElementarilyEquivalent ↑M ↑N
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_hnot : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] (G' : G.Finsubgraph), ↑(￢G') = ￢↑G'
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.tsub_le_tsub_iff_left : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α}, AddLECancellable a → AddLECancellable c → c ≤ a → (a - b ≤ a - c ↔ c ≤ b)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- **Alias** of `MeasureTheory.setToFun_finsetSum`. -/
MeasureTheory.setToFun_finset_sum : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι)
  {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) →
    (MeasureTheory.setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
-- Mathlib.Algebra.Order.Ring.Abs
sq_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a : α), |a| ^ 2 = a ^ 2
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.evalSimpTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.iUnion_quotToDoubleCoset : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), ⋃ q, DoubleCoset.quotToDoubleCoset H K q = Set.univ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). The sheaf map given in `types.sheaf_hom` is natural in terms of `X`.  -/
CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ : CategoryTheory.Functor Dᵒᵖ A} →
                      {ℱ' : CategoryTheory.Sheaf K A} →
                        (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) →
                          (CategoryTheory.coyoneda.comp
                              ((CategoryTheory.Functor.whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ) ⟶
                            CategoryTheory.coyoneda.comp
                              ((CategoryTheory.Functor.whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → SemigroupWithZero (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] →
                      [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] → SemigroupWithZero (DirectLimit G f)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.contains a = m_1.contains a_1
-- Aesop.Rule.Name
Aesop.RuleName.mk.inj : ∀ {name : Lean.Name} {builder : Aesop.BuilderName} {phase : Aesop.PhaseName} {scope : Aesop.ScopeName} {hash : UInt64}
  {name_1 : Lean.Name} {builder_1 : Aesop.BuilderName} {phase_1 : Aesop.PhaseName} {scope_1 : Aesop.ScopeName}
  {hash_1 : UInt64},
  { name := name, builder := builder, phase := phase, scope := scope, hash := hash } =
      { name := name_1, builder := builder_1, phase := phase_1, scope := scope_1, hash := hash_1 } →
    name = name_1 ∧ builder = builder_1 ∧ phase = phase_1 ∧ scope = scope_1 ∧ hash = hash_1
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} (j : J) (hj : ¬IsMax j) (k : (c.attachCells j hj).ι)
  (j_1 : J) (hj_1 : ¬IsMax j_1) (k_1 : (c.attachCells j_1 hj_1).ι),
  ({ j := j, hj := hj, k := k } = { j := j_1, hj := hj_1, k := k_1 }) = (j = j_1 ∧ k ≍ k_1)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.getLevelParams : {α : Type} → [self : Lean.Meta.Grind.TheoremLike α] → α → Array Lean.Name
-- Mathlib.Algebra.CubicDiscriminant
Cubic.toPoly_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] (P : Cubic R), P.toPoly = 0 ↔ P = 0
-- Lean.Expr
Lean.mkAppB : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.disjoint_countablyGeneratedAtom : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α],
  Pairwise (Function.onFun Disjoint (MeasurableSpace.countablyGeneratedAtom α))
-- Mathlib.Topology.Algebra.Group.Basic
Filter.inv_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, (nhdsWithin a (Set.Iio a))⁻¹ = nhdsWithin a⁻¹ (Set.Ioi a⁻¹)
-- Mathlib.Topology.UniformSpace.Ascoli
/-- A version of the **Arzela-Ascoli theorem**.

Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)`. Assume that:
* `F`, viewed as a function `ι → (X →ᵤ[𝔖] α)`, is closed and inducing
* `F` is equicontinuous on each `K ∈ 𝔖`
* For all `x ∈ ⋃₀ 𝔖`, the range of `i ↦ F i x` is contained in some fixed compact subset.

Then `ι` is compact.  -/
ArzelaAscoli.compactSpace_of_closed_inducing' : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) →
      IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) →
        (∀ K ∈ 𝔖, EquicontinuousOn F K) → (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) → CompactSpace ι
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.IsDynNetIn.of_entourage_subset : ∀ {X : Type u_1} {T : X → X} {U V : SetRel X X} {n : ℕ} {F s : Set X},
  U ⊆ V → Dynamics.IsDynNetIn T F V n s → Dynamics.IsDynNetIn T F U n s
-- Mathlib.Algebra.Group.Prod
/-- Product of multiplicative isomorphisms; the maps come from `Equiv.prodCongr`.  -/
MulEquiv.prodCongr : {M : Type u_3} →
  {N : Type u_4} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {M' : Type u_6} →
          {N' : Type u_7} → [inst_2 : MulOneClass N'] → [inst_3 : MulOneClass M'] → M ≃* M' → N ≃* N' → M × N ≃* M' × N'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, W.Equation 0 0 ↔ W.a₆ = 0
-- Mathlib.Data.Set.Function
Set.eqOn_comm : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s ↔ Set.EqOn f₂ f₁ s
-- Mathlib.RingTheory.Discriminant
_private.Mathlib.RingTheory.Discriminant.0.Algebra.termN : Lean.ParserDescr
-- Init.Data.List.Sort.Lemmas
List.cons_merge_cons_pos : ∀ {α : Type u_1} {a b : α} (s : α → α → Bool) (l r : List α),
  s a b = true → (a :: l).merge (b :: r) s = a :: l.merge (b :: r) s
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.objEquiv_apply_symm_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [inst_2 : F.IsIso] (Y : D),
  F.obj (F.objEquiv.symm Y) = Y
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- A finpartition of a graph's vertex set is `ε`-uniform (aka `ε`-regular) iff the proportion of
its pairs of parts that are not `ε`-uniform is at most `ε`.  -/
Finpartition.IsUniform : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [Field 𝕜] →
      [LinearOrder 𝕜] →
        [inst : DecidableEq α] → {A : Finset α} → Finpartition A → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Prop