mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.Integers
Valuation.IsTrivialOn.of_le_one : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {k : Type u_1}
  [inst_2 : Field k] [inst_3 : Algebra k R] (v : Valuation R Γ₀),
  (∀ (x : k), v ((algebraMap k R) x) ≤ 1) → Valuation.IsTrivialOn k v
-- Mathlib.Topology.Homotopy.Product
/-- The relative product of homotopies `F` and `G`,
where `F` takes `f₀` to `f₁` and `G` takes `g₀` to `g₁`  -/
ContinuousMap.HomotopyRel.prod : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            {f₀ f₁ : C(A, α)} →
              {g₀ g₁ : C(A, β)} →
                {S : Set A} → f₀.HomotopyRel f₁ S → g₀.HomotopyRel g₁ S → (f₀.prodMk g₀).HomotopyRel (f₁.prodMk g₁) S
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toMeasure_map : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (hf : AEMeasurable f ↑ν),
  ↑(ν.map hf) = MeasureTheory.Measure.map f ↑ν
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.zero_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (n : ℕ), 0 n = 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α} (h' : a ∈ m), m.get? a = some (m.get a h')
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyCell.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α)
  (f_2 :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true → c.contains = true) →
        δ),
  Std.DTreeMap.Internal.Impl.applyCell k Std.DTreeMap.Internal.Impl.leaf f_2 = f_2 Std.DTreeMap.Internal.Cell.empty ⋯
-- Mathlib.RingTheory.RingHom.Smooth
/-- Composition of smooth ring homomorphisms is smooth.  -/
RingHom.Smooth.comp : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.Smooth → g.Smooth → (g.comp f).Smooth
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The eigenvalues of the endomorphism `f`, as a subtype of `R`.  -/
Module.End.Eigenvalues : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → Type v
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerMap_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  (α : Type t) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  (CategoryTheory.Limits.FormalCoproduct.powerMap f α).f = fun i => f.f ∘ i
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskeringLeft_ε_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} E] [inst_3 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ε ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)).app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit E)
-- Mathlib.Combinatorics.Matroid.Basic
/-- The empty set isn't a base  -/
Matroid.RankPos.empty_not_isBase : ∀ {α : Type u_1} {M : Matroid α} [self : M.RankPos], ¬M.IsBase ∅
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.finite_neighborSet_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v), (p.toSubgraph.neighborSet w).Finite
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_apply_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.reflection i) (P.root j) = P.root j - P.pairing j i • P.root i
-- Mathlib.Analysis.Matrix.LDL
LDL.diagEntries.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef) (i : n),
  LDL.diagEntries hS i =
    inner 𝕜 (WithLp.toLp 2 (star (LDL.lowerInv hS i))) (WithLp.toLp 2 (S.mulVec (star (LDL.lowerInv hS i))))
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.inv.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F (-1)).hom.app X.obj₃
-- Mathlib.Algebra.Star.Module
selfAdjointPart_comp_subtype_skewAdjoint : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2], selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = 0
-- Init.Data.Float.Model.Float
Float.Model.instLE : LE Float.Model
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationRightAdjoint_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) {X Y : D} (f : X ⟶ Y) (x : C),
  ((CategoryTheory.evaluationRightAdjoint D c).map f).app x =
    CategoryTheory.Limits.Pi.lift fun g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) g) f
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAddMonoid : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddMonoid γ] → [ContinuousAdd γ] → AddMonoid (α →ₘ[μ] γ)
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_pred_iff_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  ¬IsMin a → ¬IsMin b → (Order.pred a = Order.pred b ↔ a = b)
-- Mathlib.RepresentationTheory.FDRep
FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G],
  (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).Full
-- Init.Data.List.Nat.Basic
List.min?_getD_le_of_mem : ∀ {l : List ℕ} {a k : ℕ}, a ∈ l → l.min?.getD k ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- The symmetric Zarankiewicz function is at least twice a corresponding extremal number.  -/
SimpleGraph.two_mul_extremalNumber_le_zarankiewicz_symm : ∀ {n s t : ℕ} {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β] [Nonempty α] [Nonempty β],
  Fintype.card α = s →
    Fintype.card β = t →
      2 * SimpleGraph.extremalNumber n (completeBipartiteGraph α β) ≤ SimpleGraph.zarankiewicz n n s t
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.re_coe : ∀ (z : Complex.UnitClosedDisc), (↑z).re = z.re
-- Init.Data.Option.Attach
Option.getD_attachWith : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} {h : ∀ (x : α), o = some x → p x} {fallback : { x // p x }},
  (o.attachWith p h).getD fallback = ⟨o.getD ↑fallback, ⋯⟩
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationDesc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y)
  [inst_2 : AlgebraicGeometry.IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂),
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H)
-- Mathlib.Algebra.Group.Subgroup.Finsupp
AddSubgroup.mem_closure_range_iff_of_fintype : ∀ {M : Type u_1} [inst : AddCommGroup M] {ι : Type u_2} {f : ι → M} {x : M} [inst_1 : Fintype ι],
  x ∈ AddSubgroup.closure (Set.range f) ↔ ∃ a, x = ∑ i, a i • f i
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instUpwardEnumerable_eq : Int32.instUpwardEnumerable = HasModel.instUpwardEnumerable✝
-- Mathlib.Analysis.Analytic.Constructions
analyticOn_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F} {s : Set E},
  AnalyticOn 𝕜 (fun x => v) s
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrOn.hasLineDerivWithinAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsExtrOn f s a → HasLineDerivWithinAt ℝ f f' s a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_lhs_exact : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs₁ rhs₁ rhs₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
    Lean.Grind.AC.Seq.denote ctx lhs₁ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
      Lean.Grind.AC.Seq.denote ctx rhs₁ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.hasDerivAt_mul_log : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt (fun x => x * Real.log x) (Real.log x + 1) x
-- Mathlib.Order.Category.Frm
_private.Mathlib.Order.Category.Frm.0.Frm.Hom.mk : {X Y : Frm} → FrameHom ↑X ↑Y → X.Hom Y
-- Mathlib.NumberTheory.FunctionField
/-- `K` is a function field over `F` iff it is a finite extension of `F(t)`.  -/
functionField_iff : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] (Ft : Type u_3) [inst_2 : Field Ft]
  [inst_3 : Algebra (Polynomial F) Ft] [IsFractionRing (Polynomial F) Ft] [inst_5 : Algebra (RatFunc F) K]
  [inst_6 : Algebra Ft K] [inst_7 : Algebra (Polynomial F) K] [IsScalarTower (Polynomial F) Ft K]
  [IsScalarTower (Polynomial F) (RatFunc F) K], FunctionField F K ↔ FiniteDimensional Ft K
-- Mathlib.Algebra.Group.NatPowAssoc
/-- A mixin for power-associative multiplication.  -/
NatPowAssoc : (M : Type u_2) → [MulOneClass M] → [Pow M ℕ] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
/-- Given `X : SSet`, this is the (colimit) cocone consisting of
the inclusions of the monogenous subcomplexes of `X`. (Note: a monogenous
subcomplex of `X` is generated by a unique nondegenerate simplex `x : X.N`.)  -/
SSet.coconeN : (X : SSet) → CategoryTheory.Limits.Cocone X.functorN
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filterMap : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ}
  {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b =>
          match f b with
          | some c => g d c
          | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.Iter.foldM g init (Std.Iter.filterMap f it) ⦃Q⦄
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKeyD fallback = t₂.maxKeyD fallback
-- Mathlib.Topology.Category.TopCat.Yoneda
/-- The universe polymorphic Yoneda presheaf on `TopCat` preserves finite products.  -/
ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf' : ∀ (Y : Type w') [inst : TopologicalSpace Y],
  CategoryTheory.Limits.PreservesFiniteProducts (ContinuousMap.yonedaPresheaf' Y)
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a bijective map which maps zero to zero,
`j : M ≃+ M'` is a group isomorphism, such that the scalar multiplications on `M` and `M'` are
compatible, then the rank of `M / R` is equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearEquiv.lift_rank_eq`.  -/
lift_rank_eq_of_equiv_equiv : ∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] (i : R → R')
  (j : M ≃+ M'),
  Function.Bijective i →
    (∀ (r : R) (m : M), j (r • m) = i r • j m) →
      Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R' M')
-- Mathlib.Order.BoundedOrder.Basic
top_notMem_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {s : Set α}, ⊤ ∉ s ↔ ∀ x ∈ s, x < ⊤
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instInhabited : Inhabited UniformSpaceCat
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_finsetSup' : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousSup β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty)
  (f : ι → CompactlySupportedContinuousMap α β), ⇑(s.sup' H f) = s.sup' H fun i => ⇑(f i)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.forget₂AddCommGroup_reflectsLimit : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J]
  (F : CategoryTheory.Functor J (ModuleCat R)),
  CategoryTheory.Limits.ReflectsLimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.exists_dual_map_eq_bot_of_lt_top : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
  p < ⊤ → Module.Projective R (M ⧸ p) → ∃ f, f ≠ 0 ∧ Submodule.map f p = ⊥
-- Init.Data.Vector.Count
Vector.count_le_count_map : ∀ {α : Type u_2} [inst : BEq α] [LawfulBEq α] {β : Type u_1} {n : ℕ} [inst_2 : BEq β] [LawfulBEq β] {xs : Vector α n}
  {f : α → β} {x : α}, Vector.count x xs ≤ Vector.count (f x) (Vector.map f xs)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Cofork f g),
  s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.CategoryStruct.comp f s.π
-- Mathlib.Analysis.Seminorm
Seminorm.ball_mem_nhds : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, Continuous ⇑p → ∀ {r : ℝ}, 0 < r → p.ball 0 r ∈ nhds 0
-- Init.Data.Nat.Basic
Nat.le_of_not_gt : ∀ {a b : ℕ}, ¬b > a → b ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker : ∀ {S : CategoryTheory.ShortComplex Ab}, S.Exact ↔ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.leadingCoeff = p.coeff p.natDegree
-- Mathlib.NumberTheory.WellApproximable
approxOrderOf.smul_eq_of_mul_dvd : ∀ {A : Type u_1} [inst : SeminormedCommGroup A] {a : A} {n : ℕ} (δ : ℝ),
  0 < n → orderOf a ^ 2 ∣ n → a • approxOrderOf A n δ = approxOrderOf A n δ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.exists_inclusion_eq_of_eventually : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖)
  {x : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕},
  (∀ᶠ (i : ι) in 𝓖, x i ∈ A i) → ∃ x', RestrictedProduct.inclusion R A h x' = x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Restricting to `S₁` then mapping through the restriction of `f` to `S₁ →ᵃ[k] S₂` is the same
as mapping through unrestricted `f`, then restricting to `S₂`.  -/
Affine.Simplex.restrict_map_restrict : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f)
  (S₁ : AffineSubspace k P) (S₂ : AffineSubspace k P₂) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁)
  (hfS : AffineSubspace.map f S₁ ≤ S₂), (s.restrict S₁ hS₁).map (f.restrict hfS) ⋯ = (s.map f hf).restrict S₂ ⋯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsLittleOIsBigO : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      {G' : Type u_8} →
        [inst : Norm E] →
          [inst_1 : Norm F] →
            [inst_2 : SeminormedAddCommGroup G'] →
              {l : Filter α} → Trans (fun x1 x2 => x1 =o[l] x2) (fun x1 x2 => x1 =O[l] x2) fun x1 x2 => x1 =o[l] x2
-- Mathlib.RingTheory.Binomial
BinomialRing.mk : {R : Type u_1} →
  [inst : AddCommMonoid R] →
    [inst_1 : Pow R ℕ] →
      [toIsAddTorsionFree : IsAddTorsionFree R] →
        (multichoose : R → ℕ → R) →
          (∀ (r : R) (n : ℕ), n.factorial • multichoose r n = (ascPochhammer ℕ n).smeval r) → BinomialRing R
-- Mathlib.Tactic.NormNum.BigOperators
/-- This represents the result of trying to determine whether the given expression
`s : Q(Finset $α)` is either empty or consists of an element inserted into a strict subset.  -/
Mathlib.Meta.Finset.ProveEmptyOrConsResult : {u : Lean.Level} → {α : Q(Type u)} → Q(Finset «$α») → Type
-- Mathlib.Topology.Spectral.Hom
/-- Reinterpret a `SpectralMap` as a `ContinuousMap`.  -/
SpectralMap.toContinuousMap : {α : Type u_2} →
  {β : Type u_3} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → SpectralMap α β → C(α, β)
-- Mathlib.Topology.CantorBendixson
/-- Once `sᵈ[a]` is a fixed point of `relDerivSet`, the perfect kernel equals `sᵈ[a]`.  -/
CantorBendixson.perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPoints : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {a : Ordinal.{u}},
  CantorBendixson.iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet →
    CantorBendixson.perfectKernel s = CantorBendixson.iteratedDerivedSet s a
-- Mathlib.Logic.Equiv.Prod
Equiv.coe_sigmaUnique : ∀ {α : Type u_10} {β : α → Type u_9} [inst : (a : α) → Unique (β a)], ⇑(Equiv.sigmaUnique α β) = Sigma.fst
-- Mathlib.Topology.MetricSpace.Algebra
lipschitzWith_lipschitz_const_mul_edist : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [_i : LipschitzMul β],
  LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.instIsRightAdjointOverForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C],
  (CategoryTheory.MonoOver.forget X).IsRightAdjoint
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isExtTangent_iff_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_filter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α},
  (↑m).WF →
    ((Std.DHashMap.Internal.Raw₀.filter f m).contains k = true ↔
      ∃ (h' : m.contains k = true), f (m.getKey k h') (Std.DHashMap.Internal.Raw₀.Const.get m k h') = true)
-- Mathlib.Topology.LocallyFinsupp
/-- A function `X → Y`  -/
Function.locallyFinsuppWithin.toFun : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : Zero Y] → Function.locallyFinsuppWithin U Y → X → Y
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instValuativeRel : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → ValuativeRel (WithVal v)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.inline : Lean.Compiler.InlineAttributeKind
-- Mathlib.Order.BoundedOrder.Basic
ne_bot_of_gt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, b < a → a ≠ ⊥
-- Lean.Elab.InfoTree.Main
/-- Resets the trees state `t₀`, runs `x` to produce a new trees state `t₁` and sets the state to be
`t₀ ++ (InfoTree.context (PartialContextInfo.autoImplicitCtx Γ) <$> t₁)` where `Γ` is the set of
auto-implicits provided by `MonadAutoImplicits m`.
 -/
Lean.Elab.withSaveAutoImplicitInfoContext : {m : Type → Type} →
  [Monad m] → [Lean.Elab.MonadInfoTree m] → {α : Type} → [MonadFinally m] → [Lean.Elab.MonadAutoImplicits m] → m α → m α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (typeName : Lean.Name) (resultType : Lean.Expr) (discr : Lean.FVarId)
  (alts : Array (Lean.Compiler.LCNF.Alt pu)),
  sizeOf (Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts) =
    1 + sizeOf typeName + sizeOf resultType + sizeOf discr + sizeOf alts
-- Std.Async.Timer
/-- If:
- `s` is still running this stops `s` without completing any remaining `Async` computations that were created
  through `wait`. Note that if another `Async` computation is binding on any of these it will hang
  forever without further intervention.
- `s` is not yet or not anymore running this is a no-op.
 -/
Std.Async.Sleep.stop : Std.Async.Sleep → IO Unit
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_one`. -/
MonoidAlgebra.support_one : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : One G] [NeZero 1], (MonoidAlgebra.coeff 1).support = 1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builderOption.inj : ∀ {o o_1 : Aesop.Frontend.BuilderOption},
  Aesop.Frontend.Feature.builderOption o = Aesop.Frontend.Feature.builderOption o_1 → o = o_1
-- Mathlib.Order.Booleanisation
Booleanisation.lift_inf_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a ⊓ Booleanisation.lift b = Booleanisation.lift (a ⊓ b)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_sub_one : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A ^ (n - 1) = A ^ n * A⁻¹
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.embDomain_succ_smul_powers : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R},
  0 < x.orderTop →
    (x • HahnSeries.SummableFamily.powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } =
      HahnSeries.SummableFamily.powers x - HahnSeries.SummableFamily.ofFinsupp fun₀ | 0 => 1
-- Mathlib.Data.Fin.SuccPred
Fin.lt_pred_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0), j < i.pred hi ↔ j.succ < i
-- Mathlib.Analysis.Meromorphic.Basic
/-- Meromorphy of a function on all of 𝕜.  -/
Meromorphic : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → Prop