mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.LiminfLimsup
Filter.le_liminf_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.le_liminf_iff._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.le_liminf_iff._auto_3 →
      (x ≤ Filter.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a)
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.dfinsuppSum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : ι → Type u_3}
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)]
  {f : Π₀ (i : ι), β i} (g : (i : ι) → β i → R), (∀ i ∈ f.support, g i (f i) ∈ I) → f.sum g ∈ I
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J} (f : j₁ ⟶ j₂), CategoryTheory.Zigzag j₁ j₂
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- For each `n : ℕ`, `countablePartition α n` is a partition of the space in at most
`2^n` sets. Each partition is finer than the preceding one. The measurable space generated by
the union of all those partitions is the measurable space on `α`.  -/
MeasurableSpace.countablePartition : (α : Type u_3) → [inst : MeasurableSpace α] → [MeasurableSpace.CountablyGenerated α] → ℕ → Set (Set α)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A measure is called locally finite if it is finite in some neighborhood of each point.  -/
MeasureTheory.IsLocallyFiniteMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofIntClamp_of_lt : ∀ {n : ℤ}, n < 2 ^ 63 → (Int64.ofIntClamp n).toNatClampNeg = n.toNat
-- Init.Data.Nat.Lemmas
Nat.le_of_lt_add_of_dvd : ∀ {n a b : ℕ}, a < b + n → n ∣ a → n ∣ b → a ≤ b
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.homAddEquiv_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M.Hom N), ModuleCat.homAddEquiv f = f.hom
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.quotientAddGroupMk_leftQuotientEquiv : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : AddSubgroup.IsComplement S ↑H) (q : G ⧸ H),
  Quotient.mk'' ↑(hS.leftQuotientEquiv q) = q
-- Mathlib.Tactic.Linarith.Datatypes
/-- Some preprocessors need to examine the full list of hypotheses instead of working item by item.
As with `Preprocessor`, the input to a `GlobalPreprocessor` is replaced by, not added to, its
output.
 -/
Mathlib.Tactic.Linarith.GlobalPreprocessor : Type
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
CategoryTheory.Functor.mapPresheaf_map_c : ∀ {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] (F : CategoryTheory.Functor C D)
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y),
  (F.mapPresheaf.map f).c = CategoryTheory.Functor.whiskerRight f.c F
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_lineMap_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → ∀ {t : R}, 0 ≤ t → s.WSameSide ((AffineMap.lineMap x y) t) y
-- Mathlib.Order.Antichain
IsAntichain.maximal_mem_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (Maximal (fun x => x ∈ s) a ↔ a ∈ s)
-- Std.Do.WP.Monad
/-- `WP.wp` preserves `seq`.  -/
Std.Do.WPMonad.wp_seq : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : m (α → β)) (x : m α), Std.Do.wp (f <*> x) = Std.Do.wp f <*> Std.Do.wp x
-- Mathlib.Logic.Function.Defs
Function.prod_def : ∀ {ι : Sort u_3} {α : ι → Type u_1} {β : ι → Type u_2} (f : (i : ι) → α i) (g : (i : ι) → β i),
  Function.prod f g = fun i => (f i, g i)
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.le_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S}, φ.IsArithFrobAt Q → Q ≤ Ideal.comap φ Q
-- Mathlib.Computability.Partrec
Nat.Partrec.below.rfind : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} {f : ℕ →. ℕ} (a : Nat.Partrec f),
  Nat.Partrec.below a → motive f a → Nat.Partrec.below ⋯
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.liftHom_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T]
  (hx' : (Polynomial.aeval x) f = 0), (h.liftHom x hx') h.root = x
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.mem_A_of_differentiable : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {ε : ℝ},
  0 < ε →
    ∀ {x : ℝ},
      DifferentiableWithinAt ℝ f (Set.Ici x) x →
        ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, x ∈ RightDerivMeasurableAux.A f (derivWithin f (Set.Ici x) x) r ε
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getUInt16Value? : Lean.Expr → OptionT Id UInt16
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.nat_add_neg : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousAdd M] {f : ℤ → M},
  HasSum f m → HasSum (fun n => f ↑n + f (-↑n)) (m + f 0)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.singleCompEvalIsoSelf_inv_app : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (X : V), (HomologicalComplex.singleCompEvalIsoSelf V c j).inv.app X = (HomologicalComplex.singleObjXSelf c j X).inv
-- Mathlib.Order.Filter.Map
Filter.mem_map' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β}, t ∈ Filter.map m f ↔ {x | m x ∈ t} ∈ f
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.equiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) (a : M),
  h.equiv.symm (f a) = (SymmetricAlgebra.ι R M) a
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid (Lex α)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits an injective map that
preserves `1` and `*` to a `MulOneClass`.  See note [reducible non-instances].  -/
Function.Injective.mulOneClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : MulOneClass M₂] →
          (f : M₁ → M₂) → Function.Injective f → f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → MulOneClass M₁
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.iInf_IicSnd_gt : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (t : ℚ) {s : Set α},
  MeasurableSet s → ∀ [MeasureTheory.IsFiniteMeasure ρ], ⨅ r, (ρ.IicSnd ↑↑r) s = (ρ.IicSnd ↑t) s
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- A subalgebra `S` of `A / R` determines a subalgebra `S.op` of the opposite ring `Aᵐᵒᵖ / R`.  -/
Subalgebra.opEquiv : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)],
  t.WF → (Std.DTreeMap.Raw.filter f t).get! k = (Option.filter (f k) (t.get? k)).get!
-- Batteries.Data.String.Lemmas
String.Pos.Raw.Valid.le_endPos : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.Valid s p → p ≤ s.rawEndPos
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.distribMulAction' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → AddMonoid (g i)} →
          [(i : I) → DistribMulAction (f i) (g i)] → DistribMulAction ((i : I) → f i) ((i : I) → g i)
-- Mathlib.Order.PiLex
Pi.le_toLex_update_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι], toLex x ≤ toLex (Function.update x i a) ↔ x i ≤ a
-- Mathlib.Logic.Equiv.Defs
/-- A family of permutations `Π a, Perm (β a)` generates a permutation `Perm (Σ a, β₁ a)`.  -/
Equiv.Perm.sigmaCongrRight : {α : Type u_1} → {β : α → Type u_2} → ((a : α) → Equiv.Perm (β a)) → Equiv.Perm ((a : α) × β a)
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.levelParams : Lean.Elab.WF.EqnInfo → List Lean.Name
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly) (c : ℕ),
  p₁.mulC p₂ c = Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ (Lean.Grind.CommRing.Poly.num 0)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.tdiv.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_1 m n
-- Init.Prelude
instMonadLiftTOfMonadLift : (m : Type u_1 → Type u_2) →
  (n : Type u_1 → Type u_3) → (o : Type u_1 → Type u_4) → [MonadLift n o] → [MonadLiftT m n] → MonadLiftT m o
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- We give a direct recursive definition of the convergents of the continued fraction
expansion of a real number `ξ`. The main reason for that is that we want to have the
convergents as rational numbers; the versions `(GenContFract.of ξ).convs` and
`(GenContFract.of ξ).convs'` always give something of the same type as `ξ`.
We can then also use dot notation `ξ.convergent n`.
Another minor reason is that this demonstrates that the proof
of Legendre's theorem does not need anything beyond this definition.
We provide a proof that this definition agrees with the other one;
see `Real.convs_eq_convergent`.
(Note that we use the fact that `1/0 = 0` here to make it work for rational `ξ`.)  -/
Real.convergent : ℝ → ℕ → ℚ
-- Mathlib.Tactic.Linter.UnusedTactic
/-- Is this a syntax kind that contains intentionally unused tactic subterms?  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.isIgnoreTacticKind : Lean.NameHashSet → Lean.SyntaxNodeKind → Bool
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddSemigrp.Hom.mk.injEq : ∀ {A B : AddSemigrp} (hom' hom'_1 : ↑A →ₙ+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_eq_iff : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) {j : ι}
  {d : ℕ} (x : f.Cell j) (s : (SSet.stdSimplex.obj { len := x.dim + 1 }).obj (Opposite.op { len := d })) (y : f.Cell j)
  (t : (SSet.stdSimplex.obj { len := y.dim + 1 }).obj (Opposite.op { len := d })),
  (CategoryTheory.ConcreteCategory.hom (x.ιSigmaStdSimplex.app (Opposite.op { len := d }))) s =
      (CategoryTheory.ConcreteCategory.hom (y.ιSigmaStdSimplex.app (Opposite.op { len := d }))) t ↔
    ∃ (h : x = y), t = cast ⋯ s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).getKeyD k fallback = fallback
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_submatrix_succ : ∀ {R : Type u_6} {n : ℕ} [inst : AddCommMonoid R] (M : Matrix (Fin n.succ) (Fin n.succ) R),
  M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- A natural transformation of functors F ⟶ F' induces a map coend F ⟶ coend F'.  -/
CategoryTheory.Limits.coend.map : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.HasCoend F] →
            {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
              [inst_3 : CategoryTheory.Limits.HasCoend F'] →
                (F ⟶ F') → (CategoryTheory.Limits.coend F ⟶ CategoryTheory.Limits.coend F')
-- Init.Data.List.Nat.TakeDrop
List.findIdx?_take : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {p : α → Bool},
  List.findIdx? p (List.take i xs) = (List.findIdx? p xs).bind (Option.guard fun j => decide (j < i))
-- Mathlib.GroupTheory.OrderOfElement
powers_eq_zpowers : ∀ {G : Type u_1} [inst : Group G] [Finite G] (x : G), ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.coevaluation_comp_rightAdjointMate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (η_ Y Yᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (fᘁ)) =
    CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ)
-- Lean.Parser.Do
Lean.Parser.Term.doIdbg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iff : ∀ {R : Type u_4} {V : Type u_5} {W : Type u_6} [inst : NormedField R] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup W] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace W]
  [IsTopologicalRing R] [inst_7 : Module R V] [inst_8 : Module R W] [SeparatingDual R V]
  [inst_10 : IsTopologicalAddGroup V] [inst_11 : IsTopologicalAddGroup W] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] (f g : V ≃L[R] W), f.conjContinuousAlgEquiv = g.conjContinuousAlgEquiv ↔ ∃ α, f = α • g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_sSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (ℐ : Set (HomogeneousIdeal 𝒜)), (sSup ℐ).toIdeal = ⨆ s ∈ ℐ, s.toIdeal
-- Mathlib.Topology.Path
Path.mul.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : ContinuousMul X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂), γ₁.mul γ₂ = (γ₁.prod γ₂).map ⋯
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.mk.inj : ∀ {hyps : Array Lean.Widget.InteractiveHypothesisBundle} {type : Lean.Widget.CodeWithInfos}
  {ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo} {hyps_1 : Array Lean.Widget.InteractiveHypothesisBundle}
  {type_1 : Lean.Widget.CodeWithInfos} {ctx_1 : Lean.Server.WithRpcRef Lean.Elab.ContextInfo},
  { hyps := hyps, type := type, ctx := ctx } = { hyps := hyps_1, type := type_1, ctx := ctx_1 } →
    hyps = hyps_1 ∧ type = type_1 ∧ ctx = ctx_1
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_neg : ∀ (a : UInt16), (-a).toUInt32 = -a.toUInt32 % 65536
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a : α) (property : [a].length = 1),
  List.MergeSort.Internal.mergeSortTR₂.run✝ le ⟨[a], property⟩ = [a]
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_lineMap_lineMap : ∀ {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 q : P) (c₁ c₂ : ℝ),
  ((signedDist v) ((AffineMap.lineMap p q) c₁)) ((AffineMap.lineMap p q) c₂) = (c₂ - c₁) * ((signedDist v) p) q
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `x` is not an isolated point of `X`, then `x : OnePoint X` is not an isolated point
of `OnePoint X`.  -/
OnePoint.nhdsNE_coe_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) [h : (nhdsWithin x {x}ᶜ).NeBot], (nhdsWithin ↑x {↑x}ᶜ).NeBot
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Iio_eq_Iio_iSup : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R}, ⋃ i, Set.Iio (f i) = Set.Iio (⨆ i, f i)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The map `((Xᵢ ×[Z] Y) ×[X] Xⱼ) ×[Xᵢ ×[Z] Y] ((Xᵢ ×[Z] Y) ×[X] Xₖ)` ⟶
`((Xⱼ ×[Z] Y) ×[X] Xₖ) ×[Xⱼ ×[Z] Y] ((Xⱼ ×[Z] Y) ×[X] Xᵢ)` needed for gluing  -/
AlgebraicGeometry.Scheme.Pullback.t' : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (i j k : 𝒰.I₀) →
            CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
                (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ⟶
              CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
                (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i)
-- Mathlib.Data.List.Infix
List.concat_get_prefix : ∀ {α : Type u_1} {x y : List α}, x <+: y → ∀ (hl : x.length < y.length), x ++ [y.get ⟨x.length, hl⟩] <+: y
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_prodMk_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (f₀ : F), ContDiff 𝕜 n fun e => (e, f₀)
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
homothety_inv_two : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : CharZero k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] (a b : P), (AffineMap.homothety a 2⁻¹) b = midpoint k a b
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instIsInducedInjectiveObjectFibrantObjectInverseImageQuasiIsoMapCochainComplexPlusιWeakEquivalencesFibrantObjectLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (CochainComplex.Plus.fibrantObjectLocalizerMorphism C).IsInduced
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : β → β}, k' ∈ t.modify k f ↔ k' ∈ t
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.forget.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.MonObj A],
  CategoryTheory.Mod.forget A = { obj := fun A_1 => A_1.X, map := fun {X Y} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_toLinAlgEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (M : Matrix n n R),
  (LinearMap.toMatrixAlgEquiv v₁) ((Matrix.toLinAlgEquiv v₁) M) = M
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `0 : R` equals 0.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  v.intValuationDef 0 = 0
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend_homRestrict : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {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'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e), e.liftExtend (e.homRestrict ψ) ⋯ = ψ
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is co-Cartesian if for all
morphisms `φ' : a ⟶ b'`, also lying over `f`, there exists a unique morphism `χ : b ⟶ b'` lifting
`𝟙 S` such that `φ' = φ ≫ χ`.  -/
CategoryTheory.Functor.IsCocartesian : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        CategoryTheory.Functor 𝒳 𝒮 → {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (s : ContMDiffSection I F (↑⊤) V),
  MDiff fun x => ⟨x, s x⟩
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `findLe`.  -/
Ordnode.findLeAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → α → α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} (h : m.WF) {hc : k' ∈ m.modify k f},
  (m.modify k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_sInf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (S : Set (NonUnitalSubring R)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.factorial_eq_mul_doubleFactorial : ∀ (n : ℕ), (n + 1).factorial = (n + 1).doubleFactorial * n.doubleFactorial
-- Mathlib.Order.Heyting.Basic
GeneralizedHeytingAlgebra.toHImp : {α : Type u_4} → [self : GeneralizedHeytingAlgebra α] → HImp α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `c₄` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.c₄ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_getElem_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.keysArray[0]
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_linearMap : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [IsNoetherian R M] [Module.Finite R N], IsNoetherian R (N →ₗ[R] M)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- This class assumes that the map `β × γ → β` given by `(x, y) ↦ x ^ y` is measurable.  -/
MeasurablePow : (β : Type u_2) → (γ : Type u_3) → [MeasurableSpace β] → [MeasurableSpace γ] → [Pow β γ] → Prop
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_eq_def' : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.normSq z = ‖z‖ ^ 2