mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.DateFormat
/-- Full AM marker (used by `aaaa`). Typically lowercase per CLDR ("ante meridiem").
 -/
Std.Time.DateFormatSymbols.amLong : Std.Time.DateFormatSymbols → String
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits a surjective map that preserves
`1` and `*` from a `MulOneClass`. See note [reducible non-instances].  -/
Function.Surjective.mulOneClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : MulOneClass M₁] →
          (f : M₁ → M₂) → Function.Surjective f → f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → MulOneClass M₂
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.getEntry : Lean.Expr → Lean.Meta.SynthInstance.SynthM Lean.Meta.SynthInstance.TableEntry
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.preservesFiniteLimits_liftToFinset : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α)
-- Init.GrindInstances.Nat
Lean.Grind.instExistsAddOfLTNat : Lean.Grind.ExistsAddOfLT ℕ
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk.injEq : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (head : Γ) (left right : Turing.ListBlank Γ) (head_1 : Γ)
  (left_1 right_1 : Turing.ListBlank Γ),
  ({ head := head, left := left, right := right } = { head := head_1, left := left_1, right := right_1 }) =
    (head = head_1 ∧ left = left_1 ∧ right = right_1)
-- Plausible.Testable
Plausible.Testable.run : {p : Prop} → [self : Plausible.Testable p] → Plausible.Configuration → Bool → Plausible.Gen (Plausible.TestResult p)
-- Init.Data.String.Termination
String.Slice.Pos.wellFounded_lt : ∀ {s : String.Slice}, WellFounded fun p q => p < q
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_above : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, i ≤ m.castSucc → (finSuccEquiv' i) m.succ = some m
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_false_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = true → t.isEmpty = false
-- Mathlib.GroupTheory.Exponent
Monoid.pow_exponent_eq_one : ∀ {G : Type u} [inst : Monoid G] (g : G), g ^ Monoid.exponent G = 1
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan_neg : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  LieSubalgebra.lieSpan R L (-s) = LieSubalgebra.lieSpan R L s
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.left_comp_retraction_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsCoreflexivePair f g] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.commonRetraction f g) h) = h
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_apply_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) {x : β} {y : α}, e.symm x = y ↔ x = e y
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.d_toCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) [inst_2 : K.HasHomology k] {Z : C}
  (h : K.cycles k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.toCycles j k) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Order.Types.Arithmetic
OrderType.type_lex_prod : ∀ (α : Type u) (β : Type v) [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.type (Lex (α × β)) = OrderType.type β * OrderType.type α
-- Mathlib.Algebra.Group.Basic
inv_injective : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Injective Inv.inv
-- Mathlib.Analysis.Normed.Module.WeakDual
StrongDual.toWeakDual_extendRCLikeₗ_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : StrongDual ℝ F),
  StrongDual.toWeakDual (StrongDual.extendRCLikeₗ f) = WeakDual.extendRCLikeL (StrongDual.toWeakDual f)
-- Mathlib.GroupTheory.OrderOfElement
nsmul_inj_iff_of_addOrderOf_eq_zero : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G}, addOrderOf x = 0 → ∀ {n m : ℕ}, n • x = m • x ↔ n = m
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instMonoFunctorFShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), CategoryTheory.Mono Φ.shortComplex.f
-- Mathlib.LinearAlgebra.Matrix.Unique
/-- The obvious additive isomorphism between M₁(A) and A, if A has an addition.  -/
Matrix.uniqueAddEquiv : {m : Type u_1} → {n : Type u_2} → {A : Type u_3} → [Unique m] → [Unique n] → [inst : Add A] → Matrix m n A ≃+ A
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A/R` and `B/R` are integral, such that any finite subalgebras in `A` and `B` are
linearly disjoint, then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_linearDisjoint_finite : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Algebra.IsIntegral R ↥A] [Algebra.IsIntegral R ↥B],
  (∀ (A' B' : Subalgebra R S), A' ≤ A → B' ≤ B → ∀ [Module.Finite R ↥A'] [Module.Finite R ↥B'], A'.LinearDisjoint B') →
    A.LinearDisjoint B
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_eq_coe_nnreal : ∀ {x : ℝ} (h : 0 ≤ x), ENNReal.ofReal x = ↑(NNReal.mk x h)
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_symm_apply_apply_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }) (a : α),
  ↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_top_coe : ∀ (a : ℝ), ContinuousAt (fun p => p.1 + p.2) (⊤, ↑a)
-- Lean.Meta.LazyDiscrTree
/-- Add a lazy entry to an existing trie.  -/
Lean.Meta.LazyDiscrTree.addLazyEntryToTrie : {α : Type} →
  Lean.Meta.LazyDiscrTree.TrieIndex → Lean.Meta.LazyDiscrTree.LazyEntry α → Lean.Meta.LazyDiscrTree.MatchM α Unit
-- Mathlib.Analysis.RCLike.Extend
StrongDual.re_extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (g : StrongDual ℝ F) (x : F), RCLike.re (g.extendRCLike x) = g x
-- Mathlib.Control.Traversable.Basic
/-- `traverse` plays well with `pure` of the identity monad  -/
LawfulTraversable.id_traverse : ∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {α : Type u} (x : t α),
  traverse pure x = pure x
-- Init.Data.Option.Array
Option.foldl_toArray : ∀ {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : α → β → α),
  Array.foldl f a o.toArray = o.elim a fun b => f a b
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_lt : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f : ι → α} {a : α},
  (∀ x ∈ s, f x ≤ a) → (∃ x ∈ s, f x < a) → (s.expect fun i => f i) < a
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.contDiff_arsinh : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.arsinh
-- Mathlib.Data.Fin.Tuple.Basic
/-- As a binary function, `Fin.cons` is injective.  -/
Fin.cons_injective2 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u}, Function.Injective2 Fin.cons
-- Mathlib.Data.Finset.Basic
Finset.filter_cons_of_neg : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s),
  ¬p a → Finset.filter p (Finset.cons a s ha) = Finset.filter p s
-- Mathlib.Dynamics.Transitive
/-- Let `M` be an additive monoid with a topologically transitive action on `α`. If
`U` is a nonempty open subset of `α` and `(m +ᵥ ·) ⁻¹' U ⊆ U` for all `m : M` then `U` is dense in
`α`.  -/
IsOpen.dense_of_preimage_vadd_invariant : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [AddAction.IsTopologicallyTransitive M α] {U : Set α},
  IsOpen U → U.Nonempty → (∀ (m : M), (fun x => m +ᵥ x) ⁻¹' U ⊆ U) → Dense U
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_id : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M}, Finsupp.mapDomain id v = v
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_insertMany_list : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {l : List (α × β)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).buckets).Perm
      (Std.Internal.List.insertListConst (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.getD a fallback = t_1.getD a_1 fallback_1
-- Mathlib.Data.Vector.Basic
/-- The recursive step of `scanl` splits a vector made up of a single element
`x ::ᵥ nil : Vector α 1` into a `Vector` of the provided starting value `b : β`
and the mapped `f b x : β` as the last value.
 -/
List.Vector.scanl_singleton : ∀ {α : Type u_1} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α 1),
  List.Vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ List.Vector.nil
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.ofList l) k' fallback = v
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_descCochain_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + -1 = p₂) (h₂₃ : p₂ + n = p₃),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂)
      ((CochainComplex.mappingCone.descCochain φ α β h).v p₂ p₃ h₂₃) =
    α.v p₁ p₃ ⋯
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The pushout along a mono that's preserved under pushouts is faithful.

This "preserved under pushouts" condition is automatically satisfied in abelian categories:
```
example [Abelian C] [Mono f] : (pushout f).Faithful := inferInstance
```
 -/
CategoryTheory.Under.faithful_pushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f]
  [∀ (Z : C) (g : X ⟶ Z), CategoryTheory.Mono (CategoryTheory.Limits.pushout.inl g f)],
  (CategoryTheory.Under.pushout f).Faithful
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `αₗ _ _ _` as an isomorphism of trifunctors.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso : (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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C)
                (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D) ≅
              CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D)
                (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D)
-- Init.Data.Array.Attach
Array.toList_pmap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ a ∈ xs, P a},
  (Array.pmap f xs H).toList = List.pmap f xs.toList ⋯
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_b_eq : ∀ (a b : ℕ+), b = a.gcdB' b * a.gcd b
-- Batteries.Data.UInt
UInt16.min_def : ∀ (x y : UInt16), x ⊓ y = if x ≤ y then x else y
-- Mathlib.ModelTheory.Bundled
Equiv.bundledInducedEquiv.eq_1 : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {N : Type w'} (g : M ≃ N),
  Equiv.bundledInducedEquiv L g = g.inducedStructureEquiv
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The braided monoidal category obtained from `C` by replacing its braiding
`β_ X Y : X ⊗ Y ≅ Y ⊗ X` with the inverse `(β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X`.
This corresponds to the automorphism of the braid group swapping
over-crossings and under-crossings.  -/
CategoryTheory.reverseBraiding : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).getKey? k = some k
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.mk.sizeOf_spec : ∀ {m : Type w → Type w'} {β : Type w} [inst : (a : Type w) → SizeOf (m a)] [inst_1 : SizeOf β] (α : Type w)
  (inst_2 : Std.Iterator α m β) (iterator : Std.IterM m β),
  sizeOf { α := α, inst := inst_2, iterator := iterator } = 1 + sizeOf α + sizeOf inst_2 + sizeOf iterator
-- Mathlib.Order.Lex
toColex_ofColex : ∀ {α : Type u_1} (a : Colex α), toColex (ofColex a) = a
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.prod_preimage_of_bij : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : CommMonoid β] (f : ι → κ) (s : Finset κ)
  (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β), ∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜},
  Asymptotics.IsBigOWith c l u v → 0 ≤ c → ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
-- Init.Data.SInt.Bitwise
Int64.zero_and : ∀ {a : Int64}, 0 &&& a = 0
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_setOfPred_even : schnirelmannDensity (Set.ofPred Even) = 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.isAffineMap_convexCombPair : ∀ {R : Type u_9} {M : Type u_10} [inst : PartialOrder R] [inst_1 : CommSemiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M),
  Convexity.IsAffineMap R (Convexity.convexCombPair s t hs ht h m)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
lintegral_fderiv_lineMap_eq_edist : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y : E},
  ∫⁻ (t : ℝ) in Set.Icc 0 1, ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Set.Icc 0 1) t) 1‖ₑ = edist x y
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toNNReal_measureReal_eq_coeFn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω),
  ((↑ν).real s).toNNReal = ν s
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Variant of the previous result with the variable expressed as `y` instead of `x + y`.  -/
HasFiniteFPowerSeriesOnBall.eq_partialSum' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → ∀ y ∈ Metric.eball x r, ∀ (m : ℕ), n ≤ m → f y = p.partialSum m (y - x)
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (↑M →ₗ[R] ↑N) → M.Hom N
-- Lean.Elab.Tactic.Simp
/-- The result of elaborating a single `simp` argument
 -/
Lean.Elab.Tactic.ElabSimpArgResult : Type
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Subgroup.isPretransitive_of_stabilizer_lt : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {G : Subgroup M},
  MulAction.stabilizer M s < G →
    (∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ MulAction.stabilizer M s, g • a = b) → MulAction.IsPretransitive (↥G) α
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- The derivative of an antitone function is nonpositive.  -/
Antitone.deriv_nonpos : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜}, Antitone g → deriv g x ≤ 0
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α),
  Array.findSomeRevM? f as = Array.findSomeRevM?.find✝ f as as.size ⋯
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- `basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩` if and only if `J ≤ K` and `e ≤ d`.  -/
MvPowerSeries.LinearTopology.basis_le_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ},
  K ≠ ⊤ →
    (MvPowerSeries.LinearTopology.basis σ R (J, d) ≤ MvPowerSeries.LinearTopology.basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.instCreatesFiniteProductsOfCreatesFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteProducts F
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ico : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ a₁ → b₁ ≤ b₂ → Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_sub : ∀ {R : Type u} {M : Type v} [inst : Sub R] [inst_1 : Sub M] (x₁ x₂ : TrivSqZeroExt R M), (x₁ - x₂).fst = x₁.fst - x₂.fst
-- Mathlib.RingTheory.Valuation.Quotient
/-- The quotient valuation on `R / J` has support `(supp v) / J` if `J ⊆ supp v`.  -/
Valuation.supp_quot : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {J : Ideal R} (hJ : J ≤ v.supp), (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Ric.isEmpty.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (x : Std.Ric α), x.isEmpty = false
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_closure : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (m : M)
  (s : Set A), m • AddSubmonoid.closure s = AddSubmonoid.closure (m • s)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.continuous_inner : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A]
  [inst_3 : SMul A E] [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℂ E] [inst_6 : CStarModule A E],
  Continuous fun x => inner A x.1 x.2
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_iSup : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S] {ι : Sort u_3} (K : ι → Ideal R), Ideal.map f (iSup K) = ⨆ i, Ideal.map f (K i)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instMulAction : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid R] →
      [inst_1 : MulAction R ENNReal] → [IsScalarTower R ENNReal ENNReal] → MulAction R (MeasureTheory.OuterMeasure α)
-- Mathlib.Algebra.LinearRecurrence
/-- The characteristic polynomial of `E` is
`X ^ E.order - ∑ i : Fin E.order, (E.coeffs i) * X ^ i`.  -/
LinearRecurrence.charPoly : {R : Type u_1} → [inst : CommRing R] → LinearRecurrence R → Polynomial R
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCoeMonCat : Coe GrpCat MonCat
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_left_left : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime (x * y) z ↔ IsCoprime y z
-- Mathlib.Analysis.Normed.Group.Basic
dist_sum_sum_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedAddCommGroup E] (s : Finset ι) (f a : ι → E),
  dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.h₀ : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g), CategoryTheory.CategoryStruct.comp SSet.ι₀ self.h = f.map
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.mk : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                {pres₂ : Module.Presentation A M₂} →
                  {f : M₁ →ₗ[A] M₂} →
                    {ι : Type w₁} →
                      {g₁ : ι → M₁} →
                        (lift : ι → pres₂.G →₀ A) → (∀ (i : ι), pres₂.π (lift i) = f (g₁ i)) → pres₂.CokernelData f g₁
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder αᵐᵒᵖ
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instAntisymmRel_std : ∀ {l : Sort u_1} [inst : Lean.Order.CompleteLattice l], Std.Antisymm fun x1 x2 => Lean.Order.PartialOrder.rel x1 x2
-- Mathlib.Order.ScottContinuity
ScottContinuous.const : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (x : β), ScottContinuous (Function.const α x)
-- Mathlib.Data.ENat.Basic
ENat.natCast_lt_add_one_iff : ∀ {m : ℕ} {n : ℕ∞}, ↑m < n + 1 ↔ ↑m ≤ n
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_eq_weight_one : ∀ {σ : Type u_1} {R : Type u_5} [inst : Semiring R], Finsupp.degree = Finsupp.weight fun x => 1