mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.center_eq_infi' : ∀ {G : Type u_1} [inst : Group G] {s : Set G},
  Subgroup.closure s = ⊤ → Subgroup.center G = ⨅ g, Subgroup.centralizer {↑g}
-- Init.Data.Float.Float32
instInhabitedFloat32 : Inhabited Float32
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.numeratorAddUnit.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (s : ↥S),
  AddOreLocalization.numeratorAddUnit s = { val := ↑s -ₒ 0, neg := 0 -ₒ s, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mem_finsupport : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) {i : ι},
  i ∈ ρ.finsupport x₀ ↔ i ∈ Function.support fun i => (ρ i) x₀
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` structure on `insert a s` when inserting a pre-existing element.  -/
Set.fintypeInsertOfMem : {α : Type u} → {a : α} → (s : Set α) → [Fintype ↑s] → a ∈ s → Fintype ↑(insert a s)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instPreorder.eq_1 : ∀ {M : Type u_2} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanOrder.instPreorder =
    { toLE := MulArchimedeanOrder.instLE, toLT := MulArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯,
      lt_iff_le_not_ge := ⋯ }
-- Lean.OriginalConstKind
/-- Checks whether the declaration was originally declared as a definition; see also
`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
 -/
Lean.wasOriginallyDefn : Lean.Environment → Lean.Name → Bool
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Set a `Bool` option in `CommandElabM`. Ideally, `CommandElabM` would have a
`MonadWithOptions` instance to this effect.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.withSetBoolOptionIn.withBoolOption : Lean.Name → Bool → Lean.Elab.Command.CommandElabM Unit → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.GroupTheory.Index
AddSubgroup.card_range_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G'),
  Nat.card ↥f.range ∣ Nat.card G
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_cpop : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVUnOp.cpop.eval = BitVec.cpop
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.Triangulated.TStructure.instHasInducedTStructureBounded : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C], t.bounded.HasInducedTStructure t
-- Lean.Parser.Types
Lean.Parser.ParserState.mkNode : Lean.Parser.ParserState → Lean.SyntaxNodeKind → ℕ → Lean.Parser.ParserState
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKey? k' =
    if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Counting.0.SimpleGraph.finsetWalkLength.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_open_ideal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R],
  IsLinearTopology R R ↔ (nhds 0).HasBasis (fun I => IsOpen ↑I) fun I => ↑I
-- Lean.Parser.Syntax
Lean.Parser.Syntax.unary.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.UInt.Bitwise
USize.toFin_not : ∀ (a : USize), (~~~a).toFin = a.toFin.rev
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm of the multiplicative identity is 1.  -/
NormOneClass.norm_one : ∀ {α : Type u_5} {inst : Norm α} {inst_1 : One α} [self : NormOneClass α], ‖1‖ = 1
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.brecOn : ∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop} {a : Set α}
  (t : MeasureTheory.generateSetAlgebra 𝒜 a),
  (∀ (a : Set α) (t : MeasureTheory.generateSetAlgebra 𝒜 a), MeasureTheory.generateSetAlgebra.below t → motive a t) →
    motive a t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The obvious projection functor from costructured arrows.  -/
CategoryTheory.CostructuredArrow.proj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (S : CategoryTheory.Functor C D) → (T : D) → CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) C
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.exists_mem_factors_of_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : α},
  a ≠ 0 → Irreducible p → p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.factors a, Associated p q
-- Mathlib.Tactic.TacticAnalysis
/-- Run the `config` against a sequence of tactics, using the `trigger` to determine which
subsequences should be `test`ed.  -/
Mathlib.TacticAnalysis.runPass : Mathlib.TacticAnalysis.ComplexConfig → Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit
-- Std.Net.Addr
Std.Net.SocketAddress.v4.inj : ∀ {addr addr_1 : Std.Net.SocketAddressV4},
  Std.Net.SocketAddress.v4 addr = Std.Net.SocketAddress.v4 addr_1 → addr = addr_1
-- Mathlib.Order.SupClosed
InfClosed.biInf_mem : ∀ {α : Type u_3} [inst : CompleteLattice α] {s : Set α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  InfClosed s → t.Finite → ⊤ ∈ s → (∀ i ∈ t, f i ∈ s) → ⨅ i ∈ t, f i ∈ s
-- Lean.Compiler.IR.Basic
/-- Application. `x` must be a `pap` value.  -/
Lean.IR.Expr.ap : Lean.IR.VarId → Array Lean.IR.Arg → Lean.IR.Expr
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_induction_right : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {motive : (m : M) → m ∈ Submonoid.closure s → Prop},
  motive 1 ⋯ →
    (∀ (x : M) (hx : x ∈ Submonoid.closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯) →
      ∀ {x : M} (h : x ∈ Submonoid.closure s), motive x h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated differential within a set `s` at a point `x` is not modified if one intersects
`s` with a neighborhood of `x`.  -/
iteratedFDerivWithin_inter : ∀ {𝕜 : 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] {s u : Set E}
  {f : E → F} {x : E} {n : ℕ}, u ∈ nhds x → iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.AddOreLocalization.vadd'' : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → R → ↥S → AddOreLocalization S X → AddOreLocalization S X
-- Init.Data.List.Erase
List.exists_erase_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α},
  a ∈ l → ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt.inj : ∀ {e : Lean.Expr} {pos : Bool} {toIntThm : Lean.Expr} {lhs rhs : Int.Internal.Linear.Expr} {e_1 : Lean.Expr}
  {pos_1 : Bool} {toIntThm_1 : Lean.Expr} {lhs_1 rhs_1 : Int.Internal.Linear.Expr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt e pos toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt e_1 pos_1 toIntThm_1 lhs_1 rhs_1 →
    e = e_1 ∧ pos = pos_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A bilinear form `B` is **positive semidefinite** if it is symmetric and nonnegative.  -/
LinearMap.BilinForm.IsPosSemidef : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [LE R] → LinearMap.BilinForm R M → Prop
-- Mathlib.GroupTheory.Index
AddSubgroup.card_mul_index : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Nat.card ↥H * H.index = Nat.card G
-- Mathlib.Order.UpperLower.Closure
lowerClosure_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, ↑(lowerClosure s) = s ↔ IsLowerSet s
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.fiber_nonempty : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f), (↑a).Nonempty
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Let `f : ℝ → E` be a function which is continuous on `[a, b]` and is differentiable on `(a, b)`.
Suppose that `‖f' t‖ ≤ C` for a.e. `t ∈ (a, b)`.
Then the distance between `f a` and `f b`
is at most `C` times the measure of `x ∈ (a, b)` such that `f' x ≠ 0`.

This lemma is useful, if `f` is known to have zero derivative at most points of `[a, b]`.  -/
norm_sub_le_mul_volume_of_norm_deriv_le_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C : ℝ},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ C) →
          ‖f b - f a‖ ≤ C * MeasureTheory.volume.real {x | x ∈ Set.Ioo a b ∧ deriv f x ≠ 0}
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result.
This new task has priority `prio`.

This is a version of `BaseIO.mapTask` that ignores the result value.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
BaseIO.chainTask : {α : Type u_1} →
  Task α → (α → BaseIO Unit) → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO Unit
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The constant factor occurring in the conclusion of `eLpNorm_le_eLpNorm_fderiv_of_eq`.
It only depends on `E`, `F`, `μ` and `p`.  -/
MeasureTheory.SNormLESNormFDerivOfEqConst : (F : Type u_6) →
  [inst : NormedAddCommGroup F] →
    [inst_1 : NormedSpace ℝ F] →
      {E : Type u_7} →
        [inst_2 : NormedAddCommGroup E] →
          [inst_3 : NormedSpace ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [FiniteDimensional ℝ E] →
                  (μ : MeasureTheory.Measure E) → [μ.IsAddHaarMeasure] → [FiniteDimensional ℝ F] → ℝ → NNReal
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q Q' : l},
  Lean.Order.PartialOrder.rel P P' →
    Lean.Order.PartialOrder.rel Q Q' → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q')
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.map_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_6 : F.Braided],
  F.map (β_ X Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X))
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward_germ_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U) {Z : C} (h : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom f) x) hx)
      (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F x) h) =
    CategoryTheory.CategoryStruct.comp (F.germ ((TopologicalSpace.Opens.map f).obj U) x hx) h
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Minute.Offset
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.isNonZero_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  (-α).IsNonZero ↔ α.IsNonZero
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cocones on `F : J ⥤ Cᵒᵖ` are equivalent to cones on `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J Cᵒᵖ} → (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.leftOp
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_zero : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)], PadicInt.zmodRepr 0 = 0
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.bddAbove_range : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] {a : α} [IsDirectedOrder α]
  {u : ℕ → α}, Filter.Tendsto u Filter.atTop (nhds a) → BddAbove (Set.range u)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_surjective : Function.Surjective Real.tan
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE ISize
-- Std.Data.DTreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Const.alter : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → (Option β → Option β) → Std.DTreeMap α (fun x => β) cmp
-- Init.Grind.Offset
Lean.Grind.Nat.eq_of_le_of_le : ∀ (u v : ℕ), u ≤ v → v ≤ u → u = v
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Global sections of a sheaf of types `F` correspond to morphisms from a terminal sheaf to `F`.
We use the constant sheaf on a singleton type as a specific choice of terminal sheaf here.  -/
CategoryTheory.Sheaf.ΓObjEquivHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] →
        [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)] →
          (F : CategoryTheory.Sheaf J (Type w)) →
            (X : Type w) →
              [Unique X] →
                (CategoryTheory.Sheaf.Γ J (Type w)).obj F ≃ ((CategoryTheory.constantSheaf J (Type w)).obj X ⟶ F)
-- Mathlib.Algebra.Ring.Equiv
/-- A family of ring isomorphisms `∀ j, (R j ≃+* S j)` generates a
ring isomorphisms between `∀ j, R j` and `∀ j, S j`.

This is the `RingEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`RingEquiv.arrowCongr`.
 -/
RingEquiv.piCongrRight : {ι : Type u_7} →
  {R : ι → Type u_8} →
    {S : ι → Type u_9} →
      [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] →
        [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)] →
          ((i : ι) → R i ≃+* S i) → ((i : ι) → R i) ≃+* ((i : ι) → S i)
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the fractional parts of the stream are nonnegative.  -/
GenContFract.IntFractPair.nth_stream_fr_nonneg : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.f_iUnion : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (i : ℕ), m.IsCaratheodory (s i)) → Pairwise (Function.onFun Disjoint s) → m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `a` and `b` are topologically nilpotent, then `a + b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.add : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsLinearTopology R R] {a b : R},
  IsTopologicallyNilpotent a → IsTopologicallyNilpotent b → IsTopologicallyNilpotent (a + b)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) (i : Fin (m + 1)),
  (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm
-- Mathlib.Data.Num.Lemmas
PosNum.add_to_nat : ∀ (m n : PosNum), ↑(m + n) = ↑m + ↑n
-- Lean.Meta.Sym.Pattern
/-- Returns true if `u` is `max v ?m` (or variant). That is, we solve `max v ?m =?= v` as `?m := v`.
This is an approximation. For example, we ignore the solution `?m := 0`.

**Note**: The same approximation is used at LevelDefEq.lean
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryApproxSelfMax : Lean.Level → Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffWithinAt.fst : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'} {s : Set N} {x : N},
  ContMDiffWithinAt J (I.prod I') n f s x → ContMDiffWithinAt J I n (fun x => (f x).1) s x
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_toNat_eq_rank : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] (A : Matrix m n R),
  Cardinal.toNat A.cRank = A.rank
-- Lean.DocString.Types
Lean.Doc.Inline.emph.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (content : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Inline.emph content) = 1 + sizeOf content
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_ne_zero : ∀ {x : ℝ}, ↑x ≠ 0 ↔ x ≠ 0
-- Mathlib.Tactic.Ring.Basic
/-- `ExProd BaseType sα e` stores the structure of a normalized monomial expression `e`.
A monomial here is a product of powers of `ExBase` expressions, terminated by a (nonzero) constant
coefficient. The data of the constant coefficient is stored in the `BaseType`.  -/
Mathlib.Tactic.Ring.ExProd : {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.instIsBotZeroClass : ∀ {α : Type u} [inst : Zero α] [inst_1 : LE α] [IsBotZeroClass α], IsBotZeroClass (WithTop α)
-- Lean.Data.PPContext
Lean.PPContext.mk.inj : ∀ {env : Lean.Environment} {mctx : Lean.MetavarContext} {lctx : Lean.LocalContext} {opts : Lean.Options}
  {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl} {env_1 : Lean.Environment} {mctx_1 : Lean.MetavarContext}
  {lctx_1 : Lean.LocalContext} {opts_1 : Lean.Options} {currNamespace_1 : Lean.Name} {openDecls_1 : List Lean.OpenDecl},
  { env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := currNamespace, openDecls := openDecls } =
      { env := env_1, mctx := mctx_1, lctx := lctx_1, opts := opts_1, currNamespace := currNamespace_1,
        openDecls := openDecls_1 } →
    env = env_1 ∧
      mctx = mctx_1 ∧ lctx = lctx_1 ∧ opts = opts_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1
-- Mathlib.RingTheory.Ideal.NatInt
Nat.mem_maximalIdeal_iff : ∀ {n : ℕ}, n ∈ IsLocalRing.maximalIdeal ℕ ↔ n ≠ 1
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_isBasis_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {I X : Set α},
  (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.IsLimit.isIso_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (hc : CategoryTheory.Limits.IsLimit c),
  f = 0 → CategoryTheory.IsIso (CategoryTheory.Limits.Fork.ι c)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_comp_cycle' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  {P : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [Module.Free R M] [Module.Finite R M] [Module.Free R P] [Module.Finite R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
  (h : P →ₗ[R] M), (LinearMap.trace R P) ((g ∘ₗ f) ∘ₗ h) = (LinearMap.trace R M) ((h ∘ₗ g) ∘ₗ f)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C_diag : ∀ (n : ℕ) (i : Fin n), CartanMatrix.C n i i = 2
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_single : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, b ≠ 0 → (fun₀ | i => b).support = {i}
-- Mathlib.Data.Nat.Fib.Basic
Nat.isStrongDvdSequence_fib : Nat.IsStrongDvdSequence Nat.fib
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circle average of a function `f` on the unit sphere equals the circle average of the function
`z ↦ f z⁻¹`.
 -/
Real.circleAverage_zero_one_congr_inv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E},
  Real.circleAverage (fun x => f x⁻¹) 0 1 = Real.circleAverage f 0 1
-- Mathlib.Computability.Primrec.List
Primrec.vector_tail : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.tail