mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.MulAction
/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`.  -/
Submonoid.isScalarTower : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass M'] [inst_1 : SMul α β] [inst_2 : SMul M' α]
  [inst_3 : SMul M' β] [IsScalarTower M' α β] (S : Submonoid M'), IsScalarTower (↥S) α β
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.ignoreIfNotExists : Lean.Lsp.DeleteFile.Options → Bool
-- Mathlib.SetTheory.Cardinal.UnivLE
univLE_iff_exists_embedding : UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
-- Mathlib.Algebra.Lie.OfAssociative
_private.Mathlib.Algebra.Lie.OfAssociative.0.termφ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.map_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.PrepathObject X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).P = F.obj P.P
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.ext_iff : ∀ {X : SSet.Truncated 1} {n : ℕ} {x y : X.Path₁ n}, x = y ↔ x.vertex = y.vertex ∧ x.arrow = y.arrow
-- Init.Data.List.Attach
List.pmap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (x_2 : ∀ a ∈ [], P a), List.pmap f [] x_2 = []
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear map is an isometry if and it preserves the inner product.  -/
LinearMap.norm_map_iff_inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {F : Type u_9}
  [inst_5 : FunLike F E E'] [LinearMapClass F 𝕜 E E'] (f : F),
  (∀ (x : E), ‖f x‖ = ‖x‖) ↔ ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y
-- Init.Data.Ord.SInt
Int64.instLawfulOrderOrd : Std.LawfulOrderOrd Int64
-- Mathlib.Combinatorics.Graph.Lattice
Graph.Compatible.edgeSet_inf : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, G.Compatible H → (G ⊓ H).edgeSet = G.edgeSet ∩ H.edgeSet
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_insert : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.insert k m p) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj : ∀ {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] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).inverse.obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_inter_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  (A ∩ x • B).card = A.convolution B⁻¹ x
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_isTorsionBySet : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Module.IsTorsionBySet R (↥(Submodule.torsionBySet R M s)) s
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.D : DyckStep
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF_def : ∀ (μ : ℝ) (v : NNReal),
  ProbabilityTheory.gaussianPDF μ v = fun x => ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x)
-- Mathlib.Topology.Order.IntermediateValue
/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly antitone (decreasing) if `f(b) ≤ f(a)`.  -/
ContinuousOn.strictAntiOn_of_injOn_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → f b ≤ f a → ContinuousOn f (Set.Icc a b) → Set.InjOn f (Set.Icc a b) → StrictAntiOn f (Set.Icc a b)
-- Mathlib.Order.Filter.Basic
Filter.Eventually.and_frequently : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∀ᶠ (x : α) in f, p x) → (∃ᶠ (x : α) in f, q x) → ∃ᶠ (x : α) in f, p x ∧ q x
-- Mathlib.Order.Hom.Lattice
/-- Natural projection homomorphism from `α × β` to `α`.  -/
LatticeHom.fst : {α : Type u_2} → {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom (α × β) α
-- Mathlib.Logic.Function.Defs
Function.dcomp_def : ∀ {ι : Sort u_3} {β : ι → Sort u_1} {φ : {i : ι} → β i → Sort u_2} (f : {i : ι} → (y : β i) → φ y) (g : (i : ι) → β i),
  f ∘' g = fun i => f (g i)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqEMatchTheoremKind.beq : Lean.Meta.Grind.EMatchTheoremKind → Lean.Meta.Grind.EMatchTheoremKind → Bool
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abelNFConv : Lean.ParserDescr
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_hom_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y),
  (z • f).hom = CategoryTheory.CategoryStruct.comp f.hom ((↑z).app Y)
-- Mathlib.Algebra.Group.PUnit
PUnit.commGroup.eq_1 : PUnit.commGroup =
  { mul := fun x x_1 => PUnit.unit, mul_assoc := PUnit.commGroup._proof_7, one := PUnit.unit,
    one_mul := PUnit.commGroup._proof_8, mul_one := PUnit.commGroup._proof_9, npow_zero := PUnit.commGroup._proof_1,
    npow_succ := PUnit.commGroup._proof_2, inv := fun x => PUnit.unit, div_eq_mul_inv := PUnit.commGroup._proof_3,
    zpow_zero' := PUnit.commGroup._proof_4, zpow_succ' := PUnit.commGroup._proof_5,
    zpow_neg' := PUnit.commGroup._proof_6, inv_mul_cancel := PUnit.commGroup._proof_10,
    mul_comm := PUnit.commGroup._proof_11 }
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.comp_epiDesc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Epi f] {T : C} (g : X ⟶ T)
  (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.epiDesc f g hg) = g
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The restriction of the trace on `L/K` restricted onto `B/A` in an AKLB setup.
See `Algebra.intTrace` instead.  -/
Algebra.intTraceAux : (A : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (B : Type u_6) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra A K] →
                    [IsFractionRing A K] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] →
                            [inst_10 : Algebra B L] →
                              [IsScalarTower A B L] →
                                [IsIntegralClosure B A L] → [FiniteDimensional K L] → [IsIntegrallyClosed A] → B →ₗ[A] A
-- Mathlib.LinearAlgebra.Determinant
/-- Specialization of `LinearEquiv.isUnit_det`  -/
LinearEquiv.isUnit_det' : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f : M ≃ₗ[A] M),
  IsUnit (LinearMap.det ↑f)
-- Mathlib.Data.Nat.Bits
Nat.div2_bit1 : ∀ (n : ℕ), (2 * n + 1).div2 = n
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The prepartition with boxes `{J ∈ π | p J}`.  -/
BoxIntegral.Prepartition.filter : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → (BoxIntegral.Box ι → Prop) → BoxIntegral.Prepartition I
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Remove and return the minimum element from the heap.  -/
Batteries.PairingHeap.deleteMin : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Option (α × Batteries.PairingHeap α le)
-- Init.Prelude
/-- A product type in which the types may be propositions, usually written `α ×' β`.

This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.


Conventions for notations in identifiers:

 * The recommended spelling of `×'` in identifiers is `PProd`. -/
PProd : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Order.Bounds.Basic
bddAbove_iff_exists_ge : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] {s : Set γ} (x₀ : γ), BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addGroup : {R : Type u} → {M : Type v} → [AddGroup R] → [AddGroup M] → AddGroup (TrivSqZeroExt R M)
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- The formal derivative of a power series in one variable.
This is defined here as a function, but will be packaged as a
derivation `derivative` on `R⟦X⟧`.
 -/
PowerSeries.derivativeFun : {R : Type u_1} → [CommSemiring R] → PowerSeries R → PowerSeries R
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h : Opposite.unop (CategoryTheory.Limits.pullback f.op g.op) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f.op g.op).unop h
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given two points on a circle, twice the radius of that circle may be expressed explicitly as
the distance between those two points divided by the cosine of the angle between the chord and
the radius at one of those points.  -/
EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_radius : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₁ s.center).cos = 2 * s.radius
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.tail.darts = p.darts.tail
-- Mathlib.RepresentationTheory.Invariants
/-- `average k G` is invariant under left multiplication by elements of `G`.  -/
GroupAlgebra.mul_average_left : ∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : Invertible ↑(Fintype.card G)] (g : G),
  MonoidAlgebra.single g 1 * GroupAlgebra.average k G = GroupAlgebra.average k G
-- Mathlib.Algebra.Free
/-- If `α` is a type, then `FreeAddMagma α` is the free additive magma generated by `α`.
This is an additive magma equipped with a function `FreeAddMagma.of : α → FreeAddMagma α` which has
the following universal property: if `M` is any magma, and `f : α → M` is any function,
then this function is the composite of `FreeAddMagma.of` and a unique additive homomorphism
`FreeAddMagma.lift f : FreeAddMagma α →ₙ+ M`.

A typical element of `FreeAddMagma α` is a formal non-associative sum of
elements of `α`. For example if `x` and `y` are terms of type `α` then `x + ((y + y) + x)` is a
"typical" element of `FreeAddMagma α`.
One can think of `FreeAddMagma α` as the type of binary trees with leaves labelled by `α`.
In general, no pair of distinct elements in `FreeAddMagma α` will commute.
 -/
FreeAddMagma : Type u → Type u
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁_inter : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C}
  {p₁ : W ⟶ CategoryTheory.Limits.pullback (E.f i.1) (F.f i.2)}
  {p₂ : W ⟶ CategoryTheory.Limits.pullback (E.f j.1) (F.f j.2)},
  CategoryTheory.CategoryStruct.comp p₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)) =
      CategoryTheory.CategoryStruct.comp p₂
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)) (E.f j.1)) →
    (E.inter F).sieve₁ p₁ p₂ =
      CategoryTheory.Sieve.bind
        (E.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2)))
            (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows
        fun x f x_1 =>
        CategoryTheory.Sieve.pullback f
          (F.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.snd (E.f i.1) (F.f i.2)))
            (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.snd (E.f j.1) (F.f j.2))))
-- Lean.Widget.Commands
Lean.Widget.eraseWidgetSpec : Lean.ParserDescr
-- Mathlib.Order.CompleteLattice.Basic
iInf_ite : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p] (f g : ι → α),
  (⨅ i, if p i then f i else g i) = (⨅ i, ⨅ (_ : p i), f i) ⊓ ⨅ i, ⨅ (_ : ¬p i), g i
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is cofiltered or empty, and we have a functor `L : C ⥤ D` with a right adjoint,
then `D` is cofiltered or empty.
 -/
CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (h : L ⊣ R), CategoryTheory.IsCofilteredOrEmpty D
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.neg with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_7 a
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.homologyπ_extendHomologyIso_inv_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C}
  (h : (K.extend e).homology j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ j)
      (CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv h) =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv
      (CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j') h)
-- Mathlib.Probability.Distributions.Geometric
/-- The pmf of the geometric distribution depending on its success probability.  -/
ProbabilityTheory.geometricPMFReal : ℝ → ℕ → ℝ
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
continuousAt_jacobiTheta₂ : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → ContinuousAt (fun p => jacobiTheta₂ p.1 p.2) (z, τ)
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk' : {B : Type u_1} → {E : B → Type u_3} → (F : Type u_4) → (x : B) → E x → Bundle.TotalSpace F E
-- Mathlib.Algebra.Homology.HomologicalComplex
ComplexShape.down.congr_simp : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α],
  ComplexShape.down α = ComplexShape.down α
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.hasStrictFDerivAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (g'inv : G →L[𝕜] E),
  φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G →
    φ.leftDeriv ∘SL g'inv = 0 → HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
-- Batteries.Data.Array.Scan
/-- **Alias** of `Array.back?_scanl`. -/
Array.back_scanl? : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  (Array.scanl f init as).back? = some (Array.foldl f init as)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk.injEq : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (toLinearMap : L →ₗ[R] M) (leibniz' : ∀ (a b : L), toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆)
  (toLinearMap_1 : L →ₗ[R] M)
  (leibniz'_1 : ∀ (a b : L), toLinearMap_1 ⁅a, b⁆ = ⁅a, toLinearMap_1 b⁆ - ⁅b, toLinearMap_1 a⁆),
  ({ toLinearMap := toLinearMap, leibniz' := leibniz' } = { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instNeg : {R : Type u_3} → {A : Type u_4} → [Neg R] → [Neg A] → Neg (Unitization R A)
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_iff_isChain`. -/
List.SortedGE.isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE → List.IsChain (fun x1 x2 => x1 ≥ x2) l
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.fvar.injEq : ∀ (a : Lean.FVarId) (a_1 : ℕ) (a_2 : Lean.FVarId) (a_3 : ℕ),
  (Lean.Meta.LazyDiscrTree.Key.fvar a a_1 = Lean.Meta.LazyDiscrTree.Key.fvar a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.instHasColimitDiscreteWalkingPairCompPairEval : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.pair K L).comp (HomologicalComplex.eval C c i))
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferConstType : Lean.Name → List Lean.Level → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Convex.Hull
convexHull.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], convexHull 𝕜 = ClosureOperator.ofCompletePred (Convex 𝕜) ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.fst_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (CategoryTheory.SemiCartesianMonoidalCategory.fst R S) =
    CategoryTheory.Limits.pullback.fst R.hom S.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `s` is a limit fork over `f` and `g`, then a morphism `k : W ⟶ X` satisfying
`k ≫ f = k ≫ g` induces a morphism `l : W ⟶ s.pt` such that `l ≫ fork.ι s = k`.  -/
CategoryTheory.Limits.Fork.IsLimit.lift' : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s : CategoryTheory.Limits.Fork f g} →
          CategoryTheory.Limits.IsLimit s →
            {W : C} →
              (k : W ⟶ X) →
                CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
                  { l // CategoryTheory.CategoryStruct.comp l s.ι = k }
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R} {k : ℕ},
  Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g)) h
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The proposition that a projective point representative `(x, y, z)` on a Weierstrass curve `W` is
nonsingular.

In other words, either `W_X(x, y, z) ≠ 0`, `W_Y(x, y, z) ≠ 0`, or `W_Z(x, y, z) ≠ 0`.

Note that this definition is only mathematically accurate for fields.  -/
WeierstrassCurve.Projective.Nonsingular : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → Prop
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The fan on `i ↦ S ⊗[R] P i` given by `∀ i, S ⊗[R] P i`  -/
CommRingCat.Under.tensorProductFan' : {R : CommRingCat} →
  (S : CommRingCat) →
    [inst : Algebra ↑R ↑S] →
      {ι : Type u} →
        (P : ι → CategoryTheory.Under R) →
          CategoryTheory.Limits.Fan fun i => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {k : α}, t.contains k = true ↔ k ∈ t