mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk_coe' : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (f : S → R) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f)
  (h₃ :
    ∀ (x y : S),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : S),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e.symm
-- Init.Data.List.Sublist
List.infix_rfl : ∀ {α : Type u_1} {l : List α}, l <:+: l
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`.  -/
hasProd_prod_of_ne_finset_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {s : Finset β}, (∀ b ∉ s, f b = 1) → ∀ [L.LeAtTop], HasProd f (∏ b ∈ s, f b) L
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum may be split into a subtraction of such sums over two subsets.  -/
Finset.weightedVSubOfPoint_sdiff_sub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
  s₂ ⊆ s →
    ∀ (w : ι → k) (p : ι → P) (b : P),
      ((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w
-- Mathlib.NumberTheory.Niven
niven_angle_div_pi_eq : ∀ {r : ℚ}, (∃ q, Real.cos (↑r * Real.pi) = ↑q) → r ∈ Set.Icc 0 1 → r ∈ {0, 1 / 3, 1 / 2, 2 / 3, 1}
-- Mathlib.Order.Sublattice
Sublattice.copy_eq : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L), L.copy s hs = L
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_map : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A : Rep.{w, u, v} k G) {X Y : Rep.{u_1, u, v} k G}
  (f : X ⟶ Y),
  A.ihom.map f =
    Rep.ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X ↑Y) (Rep.Hom.hom f).toLinearMap, isIntertwining' := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_nsmul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddMonoid β] [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] (f : F) (s : Set α) (n : ℕ), ⇑f '' (n • s) = n • ⇑f '' s
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.instZeroQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → Zero (M ⧸ p)
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns a `List` of the keys in order.  -/
Std.DTreeMap.Internal.Impl.keys : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → List α
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.instOfNatCarrierOfNatNat_1 : OfNat (↑TopCat.I) 1
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The ring topology on `MvPowerSeries` of a topological ring  -/
MvPowerSeries.WithPiTopology.instIsTopologicalRing : ∀ (σ : Type u_1) (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R],
  IsTopologicalRing (MvPowerSeries σ R)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The left homology of a short complex `S` identifies to the cokernel of the canonical
morphism `S.X₁ ⟶ kernel S.g`.  -/
CategoryTheory.ShortComplex.leftHomologyIsoCokernelLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        [inst_2 : S.HasLeftHomology] →
          [inst_3 : CategoryTheory.Limits.HasKernel S.g] →
            [inst_4 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)] →
              S.leftHomology ≅ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.Data.Seq.Computation
Computation.bind_promises : ∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β},
  s.Promises a → (f a).Promises b → (s.bind f).Promises b
-- Mathlib.Algebra.BigOperators.Fin
/-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`.  -/
finSigmaFinEquiv : {m : ℕ} → {n : Fin m → ℕ} → (i : Fin m) × Fin (n i) ≃ Fin (∑ i, n i)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instContinuousNeg : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Neg R]
  [inst_3 : Neg M] [ContinuousNeg R] [ContinuousNeg M], ContinuousNeg (TrivSqZeroExt R M)
-- Mathlib.Topology.FiberBundle.Basic
/-- For a fiber bundle `E` over `B` constructed using the `FiberPrebundle` mechanism,
continuity of a function `TotalSpace F E → X` on an open set `s` can be checked by precomposing at
each point with the pretrivialization used for the construction at that point.  -/
FiberPrebundle.continuousOn_of_comp_right : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {X : Type u_6} [inst_3 : TopologicalSpace X]
  {f : Bundle.TotalSpace F E → X} {s : Set B},
  IsOpen s →
    (∀ b ∈ s,
        ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ Set.univ)) →
      ContinuousOn f (Bundle.TotalSpace.proj ⁻¹' s)
-- Lean.Parser.Term
Lean.Parser.Term.have.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddRightCancelSemigroup M],
  Filter.Germ.instAddRightCancelSemigroup = { toAddSemigroup := Filter.Germ.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.underscore.sizeOf_spec : sizeOf Lean.Meta.Match.Example.underscore = 1
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → (l ⊓ l').HasBasis (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  DifferentiableWithinAt 𝕜 f s x → (fun x_1 => f x_1 - f x) =O[𝕜; nhdsWithin x s] fun x_1 => x_1 - x
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiff_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => (f x).ofLp i
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.isLocalRing : ∀ {ι : 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 𝒜] (𝔭 : Ideal A) [inst_6 : 𝔭.IsPrime], IsLocalRing (HomogeneousLocalization.AtPrime 𝒜 𝔭)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) ⁻¹' Set.Ioc b c = Set.Ioc (b * a) (c * a)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map.congr_simp : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f f_1 : G →* H) (e_f : f = f_1) (h : N ≤ Subgroup.comap f M),
  QuotientGroup.map N M f h = QuotientGroup.map N M f_1 ⋯
-- Init.Data.List.Nat.TakeDrop
List.length_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l₁ : List α} {l₂ : List β},
  (List.zipWith f l₁ l₂).length = min l₁.length l₂.length
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_3 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.negAddCancel with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_3 ()
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC = 1
-- Mathlib.Combinatorics.Colex
_private.Mathlib.Combinatorics.Colex.0.Finset.Colex.max_mem_aux : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Colex (Finset α)}, s ≠ t → (symmDiff (ofColex s) (ofColex t)).Nonempty
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_add_left : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] F')
  {f : MeasureTheory.SimpleFunc α F},
  MeasureTheory.SimpleFunc.setToSimpleFunc (T + T') f =
    MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T' f
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_3.splitter : (motive : (Y X : CategoryTheory.Limits.WalkingParallelPair) → (X ⟶ Y) → Sort u_1) →
  (Y X : CategoryTheory.Limits.WalkingParallelPair) →
    (f : X ⟶ Y) →
      (Unit →
          motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
            CategoryTheory.Limits.WalkingParallelPairHom.left) →
        (Unit →
            motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
              CategoryTheory.Limits.WalkingParallelPairHom.right) →
          ((x : CategoryTheory.Limits.WalkingParallelPair) →
              motive x x (CategoryTheory.Limits.WalkingParallelPairHom.id x)) →
            motive Y X f
-- Mathlib.Tactic.Attr.Register
/-- The simpset `rify_simps` is used by the tactic `rify` to move expressions from `ℕ`, `ℤ`, or
`ℚ` to `ℝ`.  -/
Parser.Attr.rify_simps : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_op_mk_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy), ed.section_.app (Opposite.op { len := 0 }) = ed.s'
-- Mathlib.Tactic.Attr.Register
/-- The simpset `mfld_simps` records several simp lemmas that are
especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it
possible to have quicker proofs (when used with `squeeze_simp` or `simp only`) while retaining
readability.

The typical use case is the following, in a file on manifolds:
If `simp [foo, bar]` is slow, replace it with `squeeze_simp [foo, bar, mfld_simps]` and paste
its output. The list of lemmas should be reasonable (contrary to the output of
`squeeze_simp [foo, bar]` which might contain tens of lemmas), and the outcome should be quick
enough.
 -/
Parser.Attr.mfld_simps : Lean.ParserDescr
-- Mathlib.Data.Finsupp.Basic
Finsupp.uncurry_apply_pair : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α →₀ β →₀ M) (a : α) (b : β),
  f.uncurry (a, b) = (f a) b
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization map of a submodule.  -/
Submodule.toLocalized : {R : Type u_1} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (p : Submonoid R) → (M' : Submodule R M) → ↥M' →ₗ[R] ↥(Submodule.localized p M')
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.Functor.mapProjectiveResolution_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v_1, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject D] [inst_5 : CategoryTheory.Preadditive D]
  [inst_6 : CategoryTheory.CategoryWithHomology D] (F : CategoryTheory.Functor C D) [inst_7 : F.Additive]
  [inst_8 : F.PreservesProjectiveObjects] [inst_9 : F.PreservesHomology] {Z : C}
  (P : CategoryTheory.ProjectiveResolution Z),
  (F.mapProjectiveResolution P).π =
    CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map P.π)
      ((HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.down ℕ) 0).hom.app Z)
-- Mathlib.Combinatorics.Graph.Delete
/-- **Alias** of `Graph.restrict_edgeSet_sdiff_eq_deleteEdges`. -/
Graph.restrict_edgeSet_diff_eq_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), G.restrict (G.edgeSet \ F) = G.deleteEdges F
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_one : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α], Matrix.adjugate 1 = 1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mrange_eq : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : AddMonoid.Coprod M N →+ P),
  AddMonoidHom.mrange f =
    AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inl) ⊔ AddMonoidHom.mrange (f.comp AddMonoid.Coprod.inr)
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod_eq_add_fmod_right : ∀ {m n k : ℤ} (i : ℤ), m.fmod n = k.fmod n → (m + i).fmod n = (k + i).fmod n
-- Mathlib.Order.Bounds.Basic
bddBelow_empty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], BddBelow ∅
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toNondegComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  s.toNondegComplex.f n =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (s.toKaroubiNondegComplexIsoN₁.inv.f.f n)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.lam.sizeOf_spec : ∀ (thm : Mathlib.Meta.FunProp.LambdaTheorem), sizeOf (Mathlib.Meta.FunProp.Theorem.lam thm) = 1 + sizeOf thm
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction equals the `vectorSpan`.  -/
AffineSubspace.direction_eq_vectorSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P), s.direction = vectorSpan k ↑s
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.div_mem_div : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (s t : NonemptyInterval α)
  (a b : α), a ∈ s → b ∈ t → a / b ∈ s / t
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_of_infinitesimal_inv : ∀ {x : ℝ*}, x ≠ 0 → x⁻¹.Infinitesimal → x.Infinite
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (a : F.ColimitType), hc.equiv a = F.descColimitType c a
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.mk.sizeOf_spec : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A} [inst_2 : SizeOf A]
  [inst_3 : SizeOf C] (F : CategoryTheory.Functor A C) (π : F.comp ι ⟶ CategoryTheory.Functor.id A)
  (epi_π_app :
    autoParam (∀ (X : A), CategoryTheory.Epi (π.app X)) CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam),
  sizeOf { F := F, π := π, epi_π_app := epi_π_app } = 1 + sizeOf F + sizeOf π
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₂ y₁ y₂ : F},
  ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃ →
    W.slope x₂ x₂ y₁ y₂ = (3 * x₂ ^ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃))
-- Init.Data.Iterators.Basic
/-- Carries out a step of iteration.
 -/
Std.Iterator.step : {α : Type w} →
  {m : Type w → Type w'} →
    {β : outParam (Type w)} →
      [self : Std.Iterator α m β] →
        (it : Std.IterM m β) → m (Std.Shrink (Std.PlausibleIterStep (Std.Iterator.IsPlausibleStep it)))
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a more convenient formulation to show that a `CokernelCofork` constructed using
`CokernelCofork.ofπ` is a limit cone.
 -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {Z : C} →
            (g : Y ⟶ Z) →
              (eq : CategoryTheory.CategoryStruct.comp f g = 0) →
                (desc : {Z' : C} → (g' : Y ⟶ Z') → CategoryTheory.CategoryStruct.comp f g' = 0 → (Z ⟶ Z')) →
                  (∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0),
                      CategoryTheory.CategoryStruct.comp g (desc g' eq') = g') →
                    (∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0) (m : Z ⟶ Z'),
                        CategoryTheory.CategoryStruct.comp g m = g' → m = desc g' eq') →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g eq)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_div_const_iff : ∀ {α : Type u} {G : Type u_1} [inst : GroupWithZero G] [inst_1 : TopologicalSpace G] [ContinuousDiv G] {b : G},
  b ≠ 0 →
    ∀ {c : G} {f : α → G} {l : Filter α},
      Filter.Tendsto (fun x => f x / b) l (nhds (c / b)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Order.Filter.Map
Filter.map_le_iff_le_comap : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {m : α → β}, Filter.map m f ≤ g ↔ f ≤ Filter.comap m g
-- Lean.Parser.Command
Lean.Parser.Command.initialize : Lean.Parser.Parser
-- Mathlib.Logic.Function.Defs
/-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates
`g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation
from `β` to `α`.  -/
Function.onFun : {α : Sort u₁} → {β : Sort u₂} → {φ : Sort u₃} → (β → β → φ) → (α → β) → α → α → φ
-- Mathlib.NumberTheory.Divisors
Nat.mem_divisorsAntidiagonalList : ∀ {n : ℕ} {a : ℕ × ℕ}, a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_id_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} {f : Z ⟶ X},
  CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id Z) f f (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
/-- The tensor product of two presheaves of modules.  -/
PresheafOfModules.Monoidal.tensorObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)) →
        PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)) →
          PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))
-- Mathlib.Order.Hom.Basic
/-- If the images by an order embedding of two elements are codisjoint,
then they are themselves codisjoint.  -/
Codisjoint.of_orderEmbedding : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ↪o β) [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] {a₁ a₂ : α}, Codisjoint (f a₁) (f a₂) → Codisjoint a₁ a₂
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.Ordering.Compares.match_1.eq_3 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.gt, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_3 a b
-- Std.Data.DTreeMap.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.DTreeMap.values : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → List β
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Discrimination tree trie. See `RefinedDiscrTree`.

A `Trie` will normally have exactly one of the following
- nonempty `values`
- nonempty `stars`, `labelledStars` and/or `children`
- nonempty `pending`
But defining it as a structure that can have all at the same time turns out to be easier.
 -/
Lean.Meta.RefinedDiscrTree.Trie : Type → Type
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.monoOfLE_comp_assoc : ∀ {X : SSet} [inst : X.Nonsingular] {x y z : X.N} (h : x ≤ y) (h' : y ≤ z) {Z : SimplexCategory}
  (h_1 : { len := z.dim } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.N.monoOfLE h) (CategoryTheory.CategoryStruct.comp (SSet.N.monoOfLE h') h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.N.monoOfLE ⋯) h_1
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- The forgetful functor from R-algebras to rings preserves all limits.
 -/
AlgCat.forget₂Ring_preservesLimitsOfSize : ∀ {R : Type u} [inst : CommRing R] [UnivLE.{v, w}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1}
    (CategoryTheory.forget₂ (AlgCat R) RingCat)
-- Mathlib.Data.Nat.Nth
Nat.nth_of_forall_not : ∀ {p : ℕ → Prop} {n : ℕ}, (∀ n' ≥ n, ¬p n') → Nat.nth p n = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w<b`.
See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices.  -/
csSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
  s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b