mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk_toProd : ∀ {R : Type u_1} {A : Type u_2} (x : Unitization R A), Unitization.mk x.toProd = x
-- Mathlib.GroupTheory.Coxeter.Length
/-- **Alias** of `CoxeterSystem.exists_isReduced`. -/
CoxeterSystem.exists_reduced_word : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω
-- Init.Data.SInt.Basic
Int8.ofUInt8.sizeOf_spec : ∀ (toUInt8 : UInt8), sizeOf { toUInt8 := toUInt8 } = 1 + sizeOf toUInt8
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_toENat_eq_iInf_finset_card : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  Cardinal.toENat p.spanRank = ⨅ s, ↑(↑s).card
-- ProofWidgets.Component.Basic
ProofWidgets.Component.mk.sizeOf_spec : ∀ {Props : Type} [inst : SizeOf Props] (toModule : Lean.Widget.Module) («export» : String),
  sizeOf { toModule := toModule, «export» := «export» } = 1 + sizeOf toModule + sizeOf «export»
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.rel'.eq_1 : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)],
  LinearAlgebra.FreeProduct.rel' R A = Function.onFun (LinearAlgebra.FreeProduct.rel R A) ⇑TensorAlgebra.ofDirectSum
-- Init.Data.SInt.Lemmas
Int64.ofNat_add : ∀ (a b : ℕ), Int64.ofNat (a + b) = Int64.ofNat a + Int64.ofNat b
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.apply_diag : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] {A : Matrix V V α},
  A.IsAdjMatrix → ∀ (i : V), A i i = 0
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.IsSolvable`.

---

A group `G` is solvable if its derived series is eventually trivial. We use this definition
because it's the most convenient one to work with.  -/
IsSolvable : (G : Type u_1) → [Group G] → Prop
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_eq_two_iff`.  -/
AddSubgroup.relIndex_eq_two_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (b + a ∈ H) (b ∈ H)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instPartialOrder = PartialOrder.ofSetLike (OpenSubgroup G) G
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.darts_cycleBypass_sublist_darts : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v), w.cycleBypass.darts.Sublist w.darts
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_lt_zero : ∀ {x : ℝ}, Real.sin (Real.arctan x) < 0 ↔ x < 0
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.π_comp_eqToHom : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] {j j' : J} (hj : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.Limits.weakLimit.π F j'
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddCommMagmaQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddCommMagma M] → (c : ModuleCon S M) → AddCommMagma (ModuleCon.Quotient M c)
-- Lean.Server.CodeActions.Attr
_private.Lean.Server.CodeActions.Attr.0.Lean.CodeAction.mkHoleCodeAction.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.HoleCodeAction
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.eq_iff : ∀ {X : SSet} {x y : X.N}, x = y ↔ x.subcomplex = y.subcomplex
-- Aesop.Tree.Data
Aesop.NormalizationState.isNormal : Aesop.NormalizationState → Bool
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.mk.inj : ∀ {σ : Type} {id : ℕ} {mkInitial : IO σ} {id_1 : ℕ} {mkInitial_1 : IO σ},
  { id := id, mkInitial := mkInitial } = { id := id_1, mkInitial := mkInitial_1 } → id = id_1 ∧ mkInitial = mkInitial_1
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGT_le_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos}, s.posGT p h ≤ q ↔ p < q.offset
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.replaceTopology_eq : ∀ {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace), u.replaceTopology h = u
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply_apply_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α), (f.cycleOf x) (f x) = f (f x)
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLinAlgEquiv_symm_apply : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal)
  (a : Module.End R (WithLp p (n → R))), (Matrix.toLpLinAlgEquiv p).symm a = (Matrix.toLpLin p p).symm a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_one_iff : ∀ {c : Cardinal.{u_1}}, c < 1 ↔ c = 0
-- Mathlib.Topology.Algebra.Monoid
instContinuousMulULift : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousMul (ULift.{u, u_3} M)
-- Lean.Elab.PreDefinition.TerminationHint
/-- If `synthetic := true`, then this `termination_by` clause was
generated by `GuessLex`, and `vars` refers to *all* parameters
of the function, not just the “extra parameters”.
Cf. Lean.Elab.WF.unpackUnary
 -/
Lean.Elab.TerminationBy.synthetic : Lean.Elab.TerminationBy → Bool
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_injective : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {f : α →ₙ+ β},
  Function.Injective ⇑f → Function.Injective ⇑(WithZero.mapAddHom f)
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- If the (left) action of `C` on `D` comes from a monoidal functor
`C ⥤ (D ⥤ D)ᴹᵒᵖ`, then `curriedActionMop C D` is naturally isomorphic to that
functor.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) →
            [inst_3 : F.Monoidal] → CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D ≅ F
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.comp.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ) =
    1 + sizeOf e + sizeOf isoLift? + sizeOf f + sizeOf g + sizeOf h + sizeOf η + sizeOf θ
-- Mathlib.Analysis.Normed.Ring.Units
/-- The function `fun t ↦ inverse (x + t)` is O(1) as `t → 0`.  -/
NormedRing.inverse_add_norm : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  (fun t => Ring.inverse (↑x + t)) =O[nhds 0] fun _t => 1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
/-- A cone in the category `PresheafOfModules R` is limit if it is so after the application
of the functors `evaluation R X` for all `X`.  -/
PresheafOfModules.evaluationJointlyReflectsLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ (X : Cᵒᵖ),
                  Small.{v, max u₂ v}
                    ↑((F.comp (PresheafOfModules.evaluation R X)).comp
                          (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] →
              (c : CategoryTheory.Limits.Cone F) →
                ((X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((PresheafOfModules.evaluation R X).mapCone c)) →
                  CategoryTheory.Limits.IsLimit c
-- Mathlib.Logic.Nonempty
nonempty_subtype : ∀ {α : Sort u_3} {p : α → Prop}, Nonempty (Subtype p) ↔ ∃ a, p a
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.pullback.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f],
  CategoryTheory.Over.pullback f = CategoryTheory.Over.pullback f_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If `x : Δ[n] _⦋d⦌` and `i : Fin (d + 1)`, we may evaluate `x i : Fin (n + 1)`.  -/
SSet.stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat : (n i : ℕ) → FunLike ((SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := i })) (Fin (i + 1)) (Fin (n + 1))
-- Mathlib.Util.PrintSorries
Mathlib.PrintSorries.State.mk.inj : ∀ {visited : Lean.NameSet} {sorries : Std.HashSet Lean.Expr} {sorryMsgs : Array Lean.MessageData}
  {visited_1 : Lean.NameSet} {sorries_1 : Std.HashSet Lean.Expr} {sorryMsgs_1 : Array Lean.MessageData},
  { visited := visited, sorries := sorries, sorryMsgs := sorryMsgs } =
      { visited := visited_1, sorries := sorries_1, sorryMsgs := sorryMsgs_1 } →
    visited = visited_1 ∧ sorries = sorries_1 ∧ sorryMsgs = sorryMsgs_1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubring_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [inst_3 : Star A],
  Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubring
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.removedVersion? : Lean.ErrorExplanation.Metadata → Option String
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.nrRealPlaces_eq_zero_iff : ∀ {K : Type u_2} [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrRealPlaces K = 0 ↔ NumberField.IsTotallyComplex K
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a a_1 : List α),
  (a = [] → False) → List.MergeSort.Internal.mergeTR.go✝ le a [] a_1 = a_1.reverseAux a
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.comp_homeomorph : ∀ {X : Type u_9} {Y : Type u_10} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {M : Type u_11}
  [inst_2 : One M] {f : Y → M}, HasCompactMulSupport f → ∀ (φ : X ≃ₜ Y), HasCompactMulSupport (f ∘ ⇑φ)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.nonempty_sup_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.Nonempty],
  (P ⊔ Q).Nonempty
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The natural isomorphism `𝟭 (Sheaf J D) ≅ sheafToPresheaf J D ⋙ presheafToSheaf J D`.  -/
CategoryTheory.sheafificationNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            CategoryTheory.Functor.id (CategoryTheory.Sheaf J D) ≅
              (CategoryTheory.sheafToPresheaf J D).comp (CategoryTheory.presheafToSheaf J D)
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} [inst_7 : IntCast F] (z : ℤ), DifferentiableOn 𝕜 (↑z) s
-- Mathlib.Order.Hom.Lex
RelIso.sumLexComplRight_symm_apply : ∀ {α : Type u_1} {r : α → α → Prop} {x : α} [inst : IsTrans α r] [inst_1 : Std.Trichotomous r] [inst_2 : DecidableRel r]
  (a : { x_1 // ¬r x x_1 } ⊕ Subtype (r x)), (RelIso.sumLexComplRight r x) a = (Equiv.sumCompl (r x)) a.swap
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsAddModHomNegOfHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A] {M N : D} [inst_5 : CategoryTheory.AddModObj A M]
  [inst_6 : CategoryTheory.AddModObj A N] (f : M ≅ N) [CategoryTheory.IsAddModHom A f.hom],
  CategoryTheory.IsAddModHom A f.inv
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData}
  {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃),
  (ψ.comp ψ').φQ = CategoryTheory.CategoryStruct.comp ψ.φQ ψ'.φQ
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.hasBasis_ball : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → ∀ {x : E}, (nhds x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2
-- Batteries.Data.String.Lemmas
String.valid_toSubstring : ∀ (s : String), s.toRawSubstring.Valid
-- Mathlib.RingTheory.SimpleModule.Isotypic
OrderIso.setIsotypicComponents_apply : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsSemisimpleModule R M] (s : Set ↑(isotypicComponents R M)),
  OrderIso.setIsotypicComponents s = ⨆ c ∈ s, ⟨↑c, ⋯⟩
-- Lean.Elab.App
/-- Returns the current parameter's binder info.
Only valid if `fTypeIsForall` has returned `true`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getParamInfo : Lean.Elab.Term.ElabAppArgs.M Lean.BinderInfo
-- Mathlib.Data.List.Sort
/-- The list `List.ofFn f` is sorted with respect to `(· ≤ ·)` if and only if `f` is monotone.  -/
List.sortedLE_ofFn_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedLE ↔ Monotone f
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity.congr_simp : ∀ {α : Type u_4} {β : Type u_5} (r r_1 : α → β → Prop),
  r = r_1 →
    ∀ {inst : (a : α) → DecidablePred (r a)} [inst_1 : (a : α) → DecidablePred (r_1 a)] (s s_1 : Finset α),
      s = s_1 → ∀ (t t_1 : Finset β), t = t_1 → Rel.edgeDensity r s t = Rel.edgeDensity r_1 s_1 t_1
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry : Type
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_if : ∀ {M : Type u_2} [inst : AddCommMonoid M] {p : Prop} [inst_1 : Decidable p] {x : M}, ∑ᶠ (_ : p), x = if p then x else 0
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPoly.beq.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) →
  (x x_1 : Lean.Grind.CommRing.Poly) →
    ((a b : ℤ) → motive (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b)) →
      ((a : ℤ) →
          (a_1 : Lean.Grind.CommRing.Mon) →
            (a_2 : Lean.Grind.CommRing.Poly) →
              (b : ℤ) →
                (b_1 : Lean.Grind.CommRing.Mon) →
                  (b_2 : Lean.Grind.CommRing.Poly) →
                    motive (Lean.Grind.CommRing.Poly.add a a_1 a_2) (Lean.Grind.CommRing.Poly.add b b_1 b_2)) →
        ((x x_2 : Lean.Grind.CommRing.Poly) →
            (∀ (a b : ℤ), x = Lean.Grind.CommRing.Poly.num a → x_2 = Lean.Grind.CommRing.Poly.num b → False) →
              (∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ)
                  (b_1 : Lean.Grind.CommRing.Mon) (b_2 : Lean.Grind.CommRing.Poly),
                  x = Lean.Grind.CommRing.Poly.add a a_1 a_2 → x_2 = Lean.Grind.CommRing.Poly.add b b_1 b_2 → False) →
                motive x x_2) →
          motive x x_1
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.addFunCCAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.AttributeKind → Lean.CoreM Unit
-- Init.PropLemmas
exists_or_eq_imp : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, (q a ∨ a = a') ∧ p a) ↔ (∃ a, q a ∧ p a) ∨ p a'
-- Batteries.Data.Nat.Lemmas
Nat.recDiagAux_succ_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_left : (n : ℕ) → motive 0 n) (zero_right : (m : ℕ) → motive m 0)
  (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1)) (m n : ℕ),
  Nat.recDiagAux zero_left zero_right succ_succ (m + 1) (n + 1) =
    succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Differentiable.continuous : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F], Differentiable 𝕜 f → Continuous f
-- Init.Data.SInt.Lemmas
Int64.sub_mul : ∀ {a b c : Int64}, (a - b) * c = a * c - b * c
-- Mathlib.Order.FixedPoints
OrderHom.gfp_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, (∀ b ≤ f b, b ≤ a) → OrderHom.gfp f ≤ a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLetDecl : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.LetDecl a)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- When `g` is a Lipschitz function sending `0` to `0` and `f` is in `Lp`, then `g ∘ f` is well
defined as an element of `Lp`.  -/
LipschitzWith.compLp : {α : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      {m : MeasurableSpace α} →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedAddCommGroup F] →
                {g : E → F} →
                  {c : NNReal} → LipschitzWith c g → g 0 = 0 → ↥(MeasureTheory.Lp E p μ) → ↥(MeasureTheory.Lp F p μ)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mcasesPatAlts : Lean.ParserDescr
-- Mathlib.Order.Sublocale
Nucleus.mem_toSublocale : ∀ {X : Type u_1} [inst : Order.Frame X] {n : Nucleus X} {x : X}, x ∈ n.toSublocale ↔ ∃ y, n y = x
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.range.eq_1 : ∀ (n : ℕ), Array.range n = Array.ofFn fun i => ↑i
-- Mathlib.Algebra.Group.ULift
ULift.div : {α : Type u} → [Div α] → Div (ULift.{u_1, u} α)
-- Init.Data.List.Sort.Lemmas
List.merge_of_le : ∀ {α : Type u_1} {le : α → α → Bool} {xs ys : List α},
  (∀ (a b : α), a ∈ xs → b ∈ ys → le a b = true) → xs.merge ys le = xs ++ ys
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLT? k = t₂.getEntryLT? k
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.symm_conjStarAlgEquiv : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K), e.conjStarAlgEquiv.symm = e.symm.conjStarAlgEquiv
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
-- Lean.Parser.Term
Lean.Parser.Tactic.quot : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.Prod
/-- The reversed version of **Tonelli's Theorem** (symmetric version). In this version `f` is in
curried form, which makes it easier for the elaborator to figure out `f` automatically.  -/
MeasureTheory.lintegral_lintegral_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α → β → ENNReal⦄,
  AEMeasurable (Function.uncurry f) (μ.prod ν) →
    ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : β × α), f z.2 z.1 ∂ν.prod μ
-- Std.Data.String.ToInt
String.toInt?_toSlice : ∀ {s : String}, s.toSlice.toInt? = s.toInt?
-- Std.Data.Iterators.Combinators.Monadic.StepSize
/-- Produces an iterator that emits one value of `it`, then drops `n - 1` elements, then emits another
value, and so on. In other words, it emits every `n`-th value of `it`, starting with the first one.

If `n = 0`, the iterator behaves like for `n = 1`: It emits all values of `it`.


**Marble diagram:**

```
it               ---1----2----3---4----5
it.stepSize 2    ---1---------3--------5
```

**Availability:**

This operation is currently only available for iterators implementing `IteratorAccess`,
such as `PRange.iter` range iterators.

**Termination properties:**

* `Finite` instance: only if the base iterator `it` is finite
* `Productive` instance: always
 -/
Std.IterM.stepSize : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] → [Std.IteratorAccess α m] → [Monad m] → Std.IterM m β → ℕ → Std.IterM m β
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_roc : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_roc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLE = true)) t.toList
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- zero-smoothness on a set is equivalent to continuity on this set.  -/
contMDiffOn_zero_iff : ∀ {𝕜 : 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 : M → M'} {s : Set M},
  ContMDiffOn I I' 0 f s ↔ ContinuousOn f s
-- Mathlib.Data.Nat.Init
/-- Batteries has a home-baked development of the algebraic and order-theoretic theory of `ℕ` and `ℤ`
which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness
libraries in mathlib (naturals and integers show up as indices/offsets in lists, cardinality in
finsets, powers in groups, ...).

Less basic uses of `ℕ` and `ℤ` should however use the typeclass-mediated development.

The relevant files are:
* `Mathlib/Data/Nat/Basic.lean` for the continuation of the home-baked development on `ℕ`
* `Mathlib/Data/Int/Init.lean` for the continuation of the home-baked development on `ℤ`
* `Mathlib/Algebra/Group/Nat/Defs.lean` for the monoid instances on `ℕ`
* `Mathlib/Algebra/Group/Int/Defs.lean` for the group instance on `ℤ`
* `Mathlib/Algebra/Ring/Nat.lean` for the semiring instance on `ℕ`
* `Mathlib/Algebra/Ring/Int/Defs.lean` for the ring instance on `ℤ`
* `Mathlib/Algebra/Order/Group/Nat.lean` for the ordered monoid instance on `ℕ`
* `Mathlib/Algebra/Order/Group/Int.lean` for the ordered group instance on `ℤ`
* `Mathlib/Algebra/Order/Ring/Nat.lean` for the ordered semiring instance on `ℕ`
* `Mathlib/Algebra/Order/Ring/Int.lean` for the ordered ring instance on `ℤ`
 -/
LibraryNote.foundational_algebra_order_theory : Batteries.Util.LibraryNote