mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- If `fn` is `UniformIntegrable`, then the family of limits in probability of sequences of `fn` is
`UniformIntegrable`.  -/
MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {κ : Type u_4} (u : Filter κ) [u.NeBot] [u.IsCountablyGenerated]
  {fn : ι → α → β}, MeasureTheory.UniformIntegrable fn p μ → MeasureTheory.UniformIntegrable (fun f => ↑f) p μ
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.ref.sizeOf_spec : ∀ {α : Type u} {β : Type v} {σ : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (node : σ),
  sizeOf (Lean.PersistentHashMap.Entry.ref node) = 1 + sizeOf node
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj (𝟙_ D)`
is a Day convolution unit.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnit : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [inst_5 : CategoryTheory.MonoidalCategoryStruct D] →
                  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    CategoryTheory.MonoidalCategory.DayConvolutionUnit
                      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.add_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {r s : R},
  FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar (r + s)) (FreeAlgebra.Pre.ofScalar r + FreeAlgebra.Pre.ofScalar s)
-- Init.Data.List.Basic
List.Sublist.below.cons : ∀ {α : Type u_1} {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {l₁ l₂ : List α} (a : α) (a_1 : l₁.Sublist l₂),
  List.Sublist.below a_1 → motive l₁ l₂ a_1 → List.Sublist.below ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.instFinitePullback : ∀ {X₂ X₃ X₄ : SSet} [X₂.Finite] [X₃.Finite] (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄), (CategoryTheory.Limits.pullback r b).Finite
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.centralizer_univ : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Subalgebra.centralizer R Set.univ = Subalgebra.center R A
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The domination order on local subrings.
`A` dominates `B` if and only if `B ≤ A` (as subrings) and `m_A ∩ B = m_B`.
 -/
LocalSubring.instPartialOrder : {R : Type u_1} → [inst : CommRing R] → PartialOrder (LocalSubring R)
-- Mathlib.Order.Basic
PUnit.min_eq : ∀ (a b : PUnit.{u_5 + 1}), min a b = PUnit.unit
-- Init.Data.Int.Gcd
Int.eq_zero_of_gcd_eq_zero_right : ∀ {a b : ℤ}, a.gcd b = 0 → b = 0
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- The object of the fiber over `S` corresponding to a `a : 𝒳` such that `p(a) = S`.  -/
CategoryTheory.Functor.Fiber.mk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} → {S : 𝒮} → {a : 𝒳} → p.obj a = S → p.Fiber S
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
measure_Icc_lt_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α}, μ (Set.Icc a b) < ⊤
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.mk.inj : ∀ {subgoals : List Lean.Expr} {instVal instTypeBody : Lean.Expr} {subgoals_1 : List Lean.Expr}
  {instVal_1 instTypeBody_1 : Lean.Expr},
  { subgoals := subgoals, instVal := instVal, instTypeBody := instTypeBody } =
      { subgoals := subgoals_1, instVal := instVal_1, instTypeBody := instTypeBody_1 } →
    subgoals = subgoals_1 ∧ instVal = instVal_1 ∧ instTypeBody = instTypeBody_1
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure.measure_univ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsProbabilityMeasure μ],
  μ Set.univ = 1
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.uncons : {m : Type u → Type u} →
  (self : MLList.Spec✝ m) →
    {α : Type u} → [Monad m] → MLList.Spec.listM✝ self α → m (Option (α × MLList.Spec.listM✝ self α))
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsScalarTower : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X]
  {N : Type u_3} [inst_3 : SMul N X] [inst_4 : SMul M N] [inst_5 : ContinuousConstSMul N X] [IsScalarTower M N X],
  IsScalarTower M N (SeparationQuotient X)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.equivProd_symm_apply : ∀ {R : Type u_1} (a b : R) (p : R × R), (QuadraticAlgebra.equivProd a b).symm p = { re := p.1, im := p.2 }
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `secondToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₂` to `max₃ j₁ j₂ j₃`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.secondToMax₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j₁ j₂ j₃ : C) → j₂ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
-- Mathlib.Order.MinMax
min_le_of_left_le : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, b ≤ a → min b c ≤ a
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_map_out : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomotopyCategory V c} (f : C ⟶ D), (HomotopyCategory.quotient V c).map (Quot.out f) = f
-- Mathlib.Data.Finset.Range
Finset.nonempty_range_iff : ∀ {n : ℕ}, (Finset.range n).Nonempty ↔ n ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.inr_freeSumIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I J_1 : Type u),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (SheafOfModules.freeSumIso I J_1).hom =
    SheafOfModules.freeMap Sum.inr
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.evalAndSuggest : Lean.Syntax → Lean.TSyntax `tactic → ℕ → optParam Lean.Try.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_comap : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {s : NonUnitalSubsemiring S} {f : F} {x : R},
  x ∈ NonUnitalSubsemiring.comap f s ↔ f x ∈ s
-- Lean.Parser.Term
Lean.Parser.Term.explicitUniv.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.cons_isPath_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support
-- Init.Data.Array.Basic
/-- Pads `xs : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`. If `xs`
already has at least `n` elements, it is returned unmodified.

Examples:
 * `#[1, 2, 3].leftpad 5 0 = #[0, 0, 1, 2, 3]`
 * `#["red", "green", "blue"].leftpad 4 "blank" = #["blank", "red", "green", "blue"]`
 * `#["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]`
 * `#["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]`
 -/
Array.leftpad : {α : Type u} → ℕ → α → Array α → Array α
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_sub_inter_subset_union : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The congruence subgroup of `SL(2, ℤ)` of matrices whose lower left-hand entry reduces to zero
modulo `N`.  -/
CongruenceSubgroup.Gamma0 : ℕ → Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)
-- Lean.Elab.Term.TermElabM
/-- If `true`, we store in the `Expr` the `Syntax` for recursive applications (i.e., applications
of free variables tagged with `isAuxDecl`). We store the `Syntax` using `mkRecAppWithSyntax`.
We use the `Syntax` object to produce better error messages at `Structural.lean` and `WF.lean`.  -/
Lean.Elab.Term.Context.saveRecAppSyntax : Lean.Elab.Term.Context → Bool
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A complement of a CoFG submodule is FG.  -/
Submodule.CoFG.fg_of_isCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M},
  IsCompl S T → S.CoFG → T.FG
-- Mathlib.Order.Sublattice
Sublattice.le_pi : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {s : Set κ} {L : (i : κ) → Sublattice (π i)}
  {M : Sublattice ((i : κ) → π i)}, M ≤ Sublattice.pi s L ↔ ∀ i ∈ s, M ≤ Sublattice.comap (Pi.evalLatticeHom i) (L i)
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_uInt64Size : ∀ (a b : Fin UInt64.size), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Mathlib.Order.Concept
Concept.swap_lt_swap_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.swap < d.swap ↔ d < c
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the forward direction of `LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

---

`range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → f.range ∈ Module.End.invtSubmodule T → f ∘ₗ T ∘ₗ f = T ∘ₗ f
-- Std.Time.Notation
/-- Defines a syntax for time-only values. The string should represent a time, either in 24-hour or
12-hour format.

Example:
`time("15:00:00")` or `time("03:00:00 PM")`
 -/
Std.Time.«termTime(_)» : Lean.ParserDescr
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_zero_iff : ∀ {d : ℤ}, d < 0 → ∀ (z : ℤ√d), z.norm = 0 ↔ z = 0
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.singleRuleTac.injEq : ∀ (decl decl_1 : Lean.Name),
  (Aesop.RuleTacDescr.singleRuleTac decl = Aesop.RuleTacDescr.singleRuleTac decl_1) = (decl = decl_1)
-- Mathlib.Algebra.Module.Submodule.Defs
SubmoduleClass.module : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : SetLike S M] → [inst_4 : AddSubmonoidClass S M] → [SMulMemClass S R M] → (s : S) → Module R ↥s
-- Mathlib.Algebra.Homology.DifferentialObject
/-- The category of differential graded objects in `V` is equivalent
to the category of homological complexes in `V`.
 -/
HomologicalComplex.dgoEquivHomologicalComplex : {β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V) ≌
              HomologicalComplex V (ComplexShape.up' b)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsCongr_symm : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f g : R →+* S} (e : f = g),
  (ModuleCat.restrictScalarsCongr e).symm = ModuleCat.restrictScalarsCongr ⋯
-- Batteries.Recycling.RBTree.Basic
/-- A nil node is balanced with black-height 0, and it is considered black.  -/
RBTree.RBNode.Balanced.nil : ∀ {α : Type u_1}, RBTree.RBNode.nil.Balanced RBTree.RBColor.black 0
-- Mathlib.Combinatorics.Colex
Finset.Colex.instOrderBot : {α : Type u_1} → [inst : PartialOrder α] → OrderBot (Colex (Finset α))
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.toList_split_intercalate : ∀ {c : Char} {l : List String},
  (∀ s ∈ l, c ∉ s.toList) →
    List.map (fun x => x.copy) (((String.singleton c).intercalate l).split c).toList = if l = [] then [""] else l
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_subtype_inj : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {K L : Subgroup ↥H},
  Subgroup.map H.subtype K = Subgroup.map H.subtype L ↔ K = L
-- Mathlib.Data.TypeVec
TypeVec.const_iff_true : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {i : Fin2 n} {x : α i} {p : Prop}, TypeVec.ofRepeat (TypeVec.const p α i x) ↔ p
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterM m α → Sort u_3) →
      (it : Std.IterM m α) →
        (Unit → motive { internalState := { list := [] } }) →
          ((x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }) → motive it
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_transvection' : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : CommRing R]
  [inst_2 : DecidableEq m] {i j : m},
  b j ≤ b i → ∀ (c : R), (Matrix.transvection i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)
-- Std.Do.SPred.Laws
Std.Do.SPred.forall_intro : ∀ {σs : List (Type u)} {α : Sort u_1} {P : Std.Do.SPred σs} {Ψ : α → Std.Do.SPred σs},
  (∀ (a : α), P ⊢ₛ Ψ a) → P ⊢ₛ ∀ a, Ψ a
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).right = X.right
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.function.inj : ∀ {thm thm_1 : Mathlib.Meta.FunProp.FunctionTheorem},
  Mathlib.Meta.FunProp.Theorem.function thm = Mathlib.Meta.FunProp.Theorem.function thm_1 → thm = thm_1
-- Init.SizeOf
Decidable.isFalse.congr_simp : ∀ {p : Prop} (h : ¬p), isFalse h = isFalse h
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
AddHom.copy : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → (f' : M → N) → f' = ⇑f → M →ₙ+ N
-- Mathlib.NumberTheory.SumTwoSquares
instDecidableExistsNatEqHAddHPowOfNat_mathlib : {n : ℕ} → Decidable (∃ x y, n = x ^ 2 + y ^ 2)
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_isSpecial : ∀ (u : PNat.XgcdType), u.flip.IsSpecial ↔ u.IsSpecial
-- Mathlib.Data.FinEnum
FinEnum.instFintype : {α : Type u} → [FinEnum α] → Fintype α
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Cylinder.LeftHomotopy.weakEquivalence_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder X)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities] {f₀ f₁ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁),
  HomotopicalAlgebra.WeakEquivalence f₀ ↔ HomotopicalAlgebra.WeakEquivalence f₁
-- Aesop.Frontend.Command
_private.Aesop.Frontend.Command.0.Aesop.Frontend.Parser.evalStatsReport?.unsafe_impl_2 : Lean.Name → Lean.CoreM (Option Aesop.StatsReport)
-- Batteries.Linter.UnreachableTactic
/-- Accumulates the set of tactic syntaxes that should be evaluated at least once.  -/
Batteries.Linter.UnreachableTactic.getTactics : Lean.NameHashSet → (Lean.SyntaxNodeKind → Bool) → Lean.Syntax → Batteries.Linter.UnreachableTactic.M Unit
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_top_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.Nondegenerate → B.orthogonal ⊤ = ⊥
-- Mathlib.Algebra.Ring.Subring.Basic
/-- If all elements of `s : Set R` commute pairwise, then `closure s` is a commutative ring.  -/
Subring.closureCommRingOfComm : {R : Type u_1} → [inst : Ring R] → {s : Set R} → (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → CommRing ↥(Subring.closure s)
-- Init.Control.Reader
ReaderT.tryFinally : {m : Type u_1 → Type u_2} → {ρ : Type u_1} → [MonadFinally m] → MonadFinally (ReaderT ρ m)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendIso_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X : C} (f : s.pt ≅ X),
  (s.extendIso f).inv.hom = f.inv
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapActionComp_inv : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [inst_2 : Monoid G] {T : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} T] (F : CategoryTheory.Functor V W) (F' : CategoryTheory.Functor W T),
  (CategoryTheory.Functor.mapActionComp G F F').inv =
    { app := fun X => CategoryTheory.CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := ⋯ }
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.isSome_iff : ∀ {ι : Type u_1} {I : WithBot (BoxIntegral.Box ι)}, Option.isSome I = true ↔ (↑I).Nonempty
-- Mathlib.Analysis.Convex.Between
affineSegment_image : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] (f : P →ᵃ[R] P') (x y : P),
  ⇑f '' affineSegment R x y = affineSegment R (f x) (f y)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.degree_U_of_ne_neg_one : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℤ),
  n ≠ -1 → (Polynomial.Chebyshev.U R n).degree = ↑((n + 1).natAbs - 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow.injEq : ∀ (ka : ℤ) (ca? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (kb : ℕ)
  (cb? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (ka_1 : ℤ) (ca?_1 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (kb_1 : ℕ) (cb?_1 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow ka ca? kb cb? =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow ka_1 ca?_1 kb_1 cb?_1) =
    (ka = ka_1 ∧ ca? = ca?_1 ∧ kb = kb_1 ∧ cb? = cb?_1)
-- Mathlib.Data.Finset.Sym
Finset.sym2_nonempty : ∀ {α : Type u_1} {s : Finset α}, s.sym2.Nonempty ↔ s.Nonempty
-- Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
/-- Fundamental theorem of calculus for set integrals, `nhdsWithin` version: if `μ` is a locally
finite measure, `f` is continuous on a measurable set `t`, and `a ∈ t`, then `∫ x in (s i), f x ∂μ =
μ (s i) • f a + o(μ (s i))` at `li` provided that `s i` tends to `(𝓝[t] a).smallSets` along `li`.
Since `μ (s i)` is an `ℝ≥0∞` number, we use `μ.real (s i)` in the actual statement.

Often there is a good formula for `μ.real (s i)`, so the formalization can take an optional
argument `m` with this formula and a proof of `(fun i => μ.real (s i)) =ᶠ[li] m`. Without these
arguments, `m i = μ.real (s i)` is used in the output.  -/
ContinuousOn.integral_sub_linear_isLittleO_ae : ∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopologyEither X E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X}
  {t : Set X} {f : X → E},
  ContinuousOn f t →
    x ∈ t →
      MeasurableSet t →
        ∀ {s : ι → Set X} {li : Filter ι},
          Filter.Tendsto s li (nhdsWithin x t).smallSets →
            ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
              autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousOn.integral_sub_linear_isLittleO_ae._auto_1 →
                (fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
-- Mathlib.Order.Heyting.Basic
GeneralizedCoheytingAlgebra.toDistribLattice : {α : Type u_2} → [GeneralizedCoheytingAlgebra α] → DistribLattice α
-- Mathlib.Algebra.Group.Defs
npowRec.eq_2 : ∀ {M : Type u_1} [inst : One M] [inst_1 : Mul M] (x : M) (n : ℕ), npowRec n.succ x = npowRec n x * x
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.regularEpiOfPreserves_isColimit : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.EffectiveEpi f]
  (F : CategoryTheory.Functor C D) [inst_3 : F.PreservesEffectiveEpis]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Functor.regularEpiOfPreserves f F c hc).isColimit =
    CategoryTheory.isColimitCoforkOfEffectiveEpi (F.map f)
      (CategoryTheory.Limits.PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
      ((CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
          (CategoryTheory.Limits.cospanIsoMk
            (CategoryTheory.Iso.refl
              (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.one))
            (CategoryTheory.Iso.refl
              (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.left))
            (CategoryTheory.Iso.refl
              (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.right))
            ⋯ ⋯)
          (F.mapCone c) (CategoryTheory.Limits.PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
          (CategoryTheory.Limits.Cone.ext
            (CategoryTheory.Iso.refl
              ((CategoryTheory.Limits.Cone.postcompose
                      (CategoryTheory.Limits.cospanIsoMk
                          (CategoryTheory.Iso.refl
                            (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.one))
                          (CategoryTheory.Iso.refl
                            (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.left))
                          (CategoryTheory.Iso.refl
                            (((CategoryTheory.Limits.cospan f f).comp F).obj CategoryTheory.Limits.WalkingCospan.right))
                          ⋯ ⋯).hom).obj
                  (F.mapCone c)).pt)
            ⋯))
        (CategoryTheory.Limits.isLimitOfPreserves F hc))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.get k ⋯ = v
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.upperSemicontinuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {f : α → γ}, Continuous f → UpperSemicontinuous f
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_apply : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian)
  (i : Fin p.support.length), hp.supportGetEquiv i = p.support[↑i]