mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffVAdd.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] {n m : WithTop ℕ∞},
  n ≤ m → ∀ [ContMDiffVAdd I I' m G M], ContMDiffVAdd I I' n G M
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [FaithfulSMul R K],
  FaithfulSMul R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Mathlib.Data.Finset.Image
/-- `s.subtype p` converts back to `s.filter p` with
`Embedding.subtype`.  -/
Finset.subtype_map : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s : Finset α},
  Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = Finset.filter p s
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_and : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.bliminf u f p ⊔ Filter.bliminf u f q ≤ Filter.bliminf u f fun x => p x ∧ q x
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.proved.sizeOf_spec : ∀ (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  sizeOf (Aesop.NormSeqResult.proved script) = 1 + sizeOf script
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice : ∀ {pat : String} {s : String.Slice},
  String.Slice.Pattern.BackwardPattern.skipSuffix? pat s =
    String.Slice.Pattern.BackwardPattern.skipSuffix? pat.toSlice s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instIsTopologicalAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F], IsTopologicalAddGroup (E →SWOT[σ] F)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfCone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.coconeUnopOfCone c).pt = Opposite.unop c.pt
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ (s : Set E), HasFTaylorSeriesUpToOn n f p s
-- Lean.Parser.Types
Lean.Parser.ParserInfo.mk : (List Lean.Parser.Token → List Lean.Parser.Token) →
  (Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) → Lean.Parser.FirstTokens → Lean.Parser.ParserInfo
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_zero_basis_Iic : (nhds 0).HasBasis (fun a => 0 < a) Set.Iic
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these
functions tends to the integral of the lower bound, then the sequence of functions converges
almost everywhere to the lower bound.  -/
MeasureTheory.tendsto_of_lintegral_tendsto_of_antitone : ∀ {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ)) →
      (∀ᵐ (a : α) ∂μ, Antitone fun i => f i a) →
        (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a) →
          ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
-- Init.Data.String.Subslice
String.Slice.subslice_endPos : ∀ {s : String.Slice} {newStart : s.Pos}, s.subslice newStart s.endPos ⋯ = s.subsliceFrom newStart
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.isGeneratedBy_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {ι : Type w'} {X : ι → Cᵒᵖ} (x : (i : ι) → F.obj (X i)),
  G.IsGeneratedBy x ↔ ⨆ i, CategoryTheory.Subfunctor.ofSection (x i) = G
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple.eq_3 : ∀ (x k : ℕ),
  List.Nat.antidiagonalTuple k.succ x =
    List.flatMap (fun ni => List.map (fun x => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2))
      (List.Nat.antidiagonal x)
-- Aesop.Tree.Data
Aesop.Goal.elim : Aesop.Goal → Aesop.GoalData Aesop.Rapp Aesop.MVarCluster
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  f.FiniteType = Algebra.FiniteType A B
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a ≠ 0 → ∀ (b c : α), (fun x => a * x) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
-- Mathlib.Topology.NhdsWithin
nhdsWithin_inter_of_mem' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
  t ∈ nhdsWithin a s → nhdsWithin a (s ∩ t) = nhdsWithin a s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.isZero_of_subsingleton : ∀ (V : SemiNormedGrp) [Subsingleton V.carrier], CategoryTheory.Limits.IsZero V
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.HasPullbacksOfInclusions C
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of colimits of shape along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.PreservesColimitsOfShape J F], CategoryTheory.Limits.PreservesColimitsOfShape J G
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.map_smul : ∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : SMul M α] [MeasurableConstSMul M α] (c : M)
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ],
  MeasureTheory.Measure.map (fun x => c • x) μ = μ
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_eq_derivFamily : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.deriv f = Ordinal.derivFamily fun x => f
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The inclusion `FibrantObject C ⥤ C`, as a localizer morphism.  -/
HomotopicalAlgebra.FibrantObject.localizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
        (HomotopicalAlgebra.weakEquivalences C)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ t.insertManyIfNewUnit l}, (t.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Tactic.Translate.Reorder
/-- Print an `ArgReorder`, representing the arguments by their index.  -/
Mathlib.Tactic.Translate.ArgReorder.toString : Mathlib.Tactic.Translate.ArgReorder → String
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instIsScalarTower_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X], IsScalarTower R (OreLocalization S M) (OreLocalization S X)
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a closed nonempty subset `s` of `Π (n : ℕ), E n`, there exists a Lipschitz retraction
onto this set, i.e., a Lipschitz map with range equal to `s`, equal to the identity on `s`.  -/
PiNat.exists_lipschitz_retraction_of_isClosed : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)}, IsClosed s → s.Nonempty → ∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ LipschitzWith 1 f
-- Init.Data.UInt.Lemmas
UInt32.ofFin_mod : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a % b) = UInt32.ofFin a % UInt32.ofFin b
-- Lean.Meta.AppBuilder
/-- Returns the application `constName xs`.
It tries to fill the implicit arguments before the last element in `xs`.

Remark:
``mkAppM `arbitrary #[α]`` returns `@arbitrary.{u} α` without synthesizing
the implicit argument occurring after `α`.
Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]``,
returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
 -/
Lean.Meta.mkAppM : Lean.Name → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofHom_comp : ∀ {X Y Z : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : AddGroup Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalAddGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y]
  [inst_10 : AddGroup Z] [inst_11 : TopologicalSpace Z] [inst_12 : IsTopologicalAddGroup Z] [inst_13 : CompactSpace Z]
  [inst_14 : TotallyDisconnectedSpace Z] (f : X →ₜ+ Y) (g : Y →ₜ+ Z),
  ProfiniteAddGrp.ofHom (g.comp f) =
    CategoryTheory.CategoryStruct.comp (ProfiniteAddGrp.ofHom f) (ProfiniteAddGrp.ofHom g)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.delta_lt_false : ∀ {a b : ℕ}, Ordnode.delta * a < b → Ordnode.delta * b < a → False
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- A complex-valued real-bilinear map on an oriented real inner product space of dimension 2. Its
real part is the inner product and its imaginary part is `Orientation.areaForm`.

On `ℂ` with the standard orientation, `kahler w z = conj w * z`; see `Complex.kahler`.  -/
Orientation.kahler : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →ₗ[ℝ] E →ₗ[ℝ] ℂ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₂_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (i : E.I₀),
  (CategoryTheory.PreZeroHypercover.pullback₂ f E).X i = CategoryTheory.Limits.pullback (E.f i) f
-- Std.Time.Format.Basic
Std.Time.FormatPart.modifier.inj : ∀ {modifier modifier_1 : Std.Time.Modifier},
  Std.Time.FormatPart.modifier modifier = Std.Time.FormatPart.modifier modifier_1 → modifier = modifier_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEval.toMkEvalWhiskerLeft : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkEval m] → Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algebraMap_eq_inl : ∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⇑(algebraMap R (Unitization R A)) = Unitization.inl
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.isoShift_inv_naturality_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n : M) {X Y : C} (f : X ⟶ Y) {Z : A}
  (h : F.obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shift n).map f)
      (CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app X)
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) h)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
_private.Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare.0.ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable_real : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {s : Set (↑unitInterval × ↑unitInterval)}
  {t : Set E} {ω : E → E →L[ℝ] F} {dω : E → E →L[ℝ] E →L[ℝ] F} (φ : (↑γ₁).Homotopy ↑γ₂),
  s.Countable →
    (∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) →
      (∀ a_1 ∈ Set.Ioo 0 1,
          ∀ b_1 ∈ Set.Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))) →
        ContinuousOn ω (closure t) →
          (∀ a_1 ∈ Set.Ioo 0 1,
              ∀ b_1 ∈ Set.Ioo 0 1,
                (a_1, b_1) ∉ s →
                  ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
                    ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u) →
            ContDiffOn ℝ 2 (fun xy => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1) →
              ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x =
                ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Antitone fun x => Set.Iic (f x)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
DifferentiableWithinAtProp.eq_1 : ∀ {𝕜 : 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) {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (f : H → H') (s : Set H) (x : H),
  DifferentiableWithinAtProp I I' f s x =
    DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.mk.injEq : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (toFun : X → X → R)
  (refl' : ∀ (x : X), toFun x x = 0) (symm' : ∀ (x y : X), toFun x y = toFun y x)
  (triangle' : ∀ (x y z : X), toFun x z ≤ toFun x y + toFun y z) (toFun_1 : X → X → R)
  (refl'_1 : ∀ (x : X), toFun_1 x x = 0) (symm'_1 : ∀ (x y : X), toFun_1 x y = toFun_1 y x)
  (triangle'_1 : ∀ (x y z : X), toFun_1 x z ≤ toFun_1 x y + toFun_1 y z),
  ({ toFun := toFun, refl' := refl', symm' := symm', triangle' := triangle' } =
      { toFun := toFun_1, refl' := refl'_1, symm' := symm'_1, triangle' := triangle'_1 }) =
    (toFun = toFun_1)
-- Mathlib.AlgebraicTopology.MooreComplex
/-- The (normalized) Moore complex of a simplicial object `X` in an abelian category `C`.

The `n`-th object is intersection of
the kernels of `X.δ i : X.obj n ⟶ X.obj (n-1)`, for `i = 1, ..., n`.

The differentials are induced from `X.δ 0`,
which maps each of these intersections of kernels to the next.
 -/
AlgebraicTopology.normalizedMooreComplex : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)
-- Mathlib.Analysis.Convex.Side
AffineEquiv.sOppSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [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] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P'), (AffineSubspace.map (↑f) s).SOppSide (f x) (f y) ↔ s.SOppSide x y
-- Std.Data.ExtTreeSet.Basic
/-- Support for the `for` loop construct in `do` blocks. The iteration happens in ascending
order.
 -/
Std.ExtTreeSet.forIn : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [inst : Monad m] →
          [LawfulMonad m] → [Std.TransCmp cmp] → (α → δ → m (ForInStep δ)) → δ → Std.ExtTreeSet α cmp → m δ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_of_length_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ}, w.length ≤ i → w.getVert i = v
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X_1 Y : C₁} (f : X_1 ⟶ Y)
  (X_2 : C₂) (X_3 : C₃),
  ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).map f).app X_2).app X_3 = X.map (((F.map f).app X_2).app X_3)
-- Mathlib.Topology.VectorBundle.Constructions
VectorBundle.pullback : ∀ (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : TopologicalSpace B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] {K : Type u_7} [inst_8 : FunLike K B' B]
  [inst_9 : ContinuousMapClass K B' B] [inst_10 : (x : B) → TopologicalSpace (E x)] [inst_11 : FiberBundle F E]
  [VectorBundle 𝕜 F E] (f : K), VectorBundle 𝕜 F (⇑f *ᵖ E)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.pOpcycles_extendOpcyclesIso_inv : ∀ {ι : 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'],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.extendOpcyclesIso e hj').inv =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv ((K.extend e).pOpcycles j')
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keys_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ},
  (Std.TreeMap.map f t).keys = t.keys
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_cons_eq_if : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs acc : List α},
  List.splitOnPPrepend p (x :: xs) acc =
    if p x = true then acc.reverse :: List.splitOnP p xs else List.splitOnPPrepend p xs (x :: acc)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂),
  CategoryTheory.CategoryStruct.comp self.f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ self.f₁
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  {l : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l] g →
    ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)
-- Mathlib.Data.Seq.Computation
Computation.notMem_empty : ∀ {α : Type u} (a : α), a ∉ Computation.empty α
-- Mathlib.NumberTheory.NumberField.Basic
/-- The algebra homomorphism `(𝓞 K) →ₐ[𝓞 k] (𝓞 L)` given by restricting an algebra homomorphism
`f : K →ₐ[k] L` to `𝓞 K`.  -/
NumberField.RingOfIntegers.mapAlgHom : {k : Type u_3} →
  {K : Type u_4} →
    {L : Type u_5} →
      {F : Type u_6} →
        [inst : Field k] →
          [inst_1 : Field K] →
            [inst_2 : Field L] →
              [inst_3 : Algebra k K] →
                [inst_4 : Algebra k L] →
                  [inst_5 : FunLike F K L] →
                    [AlgHomClass F k K L] →
                      F → NumberField.RingOfIntegers K →ₐ[NumberField.RingOfIntegers k] NumberField.RingOfIntegers L
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (c : CategoryTheory.Limits.Cocone F) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre F E)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F c) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.desc (E.comp F) (CategoryTheory.Limits.Cocone.whisker E c)) h
-- Batteries.Data.HashMap.Basic
/-- Variant of `ofList` which accepts a function that combines values of duplicated keys.
```
ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}
```
 -/
Std.HashMap.ofListWith : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → (β → β → β) → Std.HashMap α β
-- Mathlib.Data.PFun
/-- If advancing one step from `a` leads to `b : β`, then `f.fix a = b`  -/
PFun.fix_stop : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a : α}, Sum.inl b ∈ f a → b ∈ f.fix a
-- Mathlib.Order.BooleanAlgebra.Basic
compl_bijective : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Bijective compl
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKey?ₘ_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.getKey?ₘ k = Std.Internal.List.getKey? k t.toListModel
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `Finset.Nonempty.card_pow_mono` for a version that works for zero powers.  -/
Finset.card_pow_mono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelMonoid α] {s : Finset α} {m n : ℕ},
  m ≠ 0 → m ≤ n → (s ^ m).card ≤ (s ^ n).card
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.r_iff : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (a a_1 : ℕ × K),
  PerfectClosure.R K p a a_1 ↔ ∃ n x, a = (n, x) ∧ a_1 = (n + 1, (frobenius K p) x)
-- Mathlib.Topology.Compactification.StoneCech
stoneCechUnit.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α), stoneCechUnit x = T2Quotient.mk (preStoneCechUnit x)