mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Filter
Filter.tendsto_nhds_atTop : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : PartialOrder X] [OrderTopology X] [NoMaxOrder X],
  Filter.Tendsto nhds Filter.atTop (nhds Filter.atTop)
-- Mathlib.Algebra.Group.Commute.Basic
Commute.zpow_zpow_self : ∀ {G : Type u_1} [inst : Group G] (a : G) (m n : ℤ), Commute (a ^ m) (a ^ n)
-- Batteries.Data.PairingHeap
/-- An empty heap is no more than one tree.  -/
Batteries.PairingHeapImp.Heap.NoSibling.nil : ∀ {α : Type u_1}, Batteries.PairingHeapImp.Heap.nil.NoSibling
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (k, v) ∈ t.toList ↔ t.getKey? k = some k ∧ t[k]? = some v
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together. Stated by permuting the entries of `f`.  -/
Antivary.sum_smul_lt_sum_comp_perm_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → (∑ i, f i • g i < ∑ i, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g)
-- Lean.PrettyPrinter.Formatter
/-- Registers a formatter for a parser.

`@[formatter k]` registers a declaration of type `Lean.PrettyPrinter.Formatter` to be used for
formatting syntax of kind `k`.
 -/
Lean.PrettyPrinter.formatterAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter
-- Init.Data.UInt.Lemmas
USize.mod_zero : ∀ {a : USize}, a % 0 = a
-- Mathlib.SetTheory.ZFC.Basic
/-- `{x ∈ a | p x}` is the set of elements in `a` satisfying `p`  -/
ZFSet.sep : (ZFSet.{u_1} → Prop) → ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.Data.Nat.Log
Nat.log_one_left : ∀ (n : ℕ), Nat.log 1 n = 0
-- Mathlib.Analysis.Normed.Group.Quotient
/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m * s‖ < ‖mk' S m‖ + ε`.  -/
QuotientGroup.exists_norm_mul_lt : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] (S : Subgroup M) (m : M) {ε : ℝ},
  0 < ε → ∃ s ∈ S, ‖m * s‖ < ‖(QuotientGroup.mk' S) m‖ + ε
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.instEssSurjObjPostOfFull : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Full] [F.EssSurj], (CategoryTheory.Under.post F).EssSurj
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} 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} {H : Type u'} {inst_6 : CategoryTheory.Category.{v', u'} H}
  {inst_7 : CategoryTheory.Preadditive H} [self : t.Heart H],
  (CategoryTheory.Triangulated.TStructure.Heart.ι t).essImage = t.heart
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_shiftRight : ∀ {i j : ℕ} (x : ℕ), (x >>> i).testBit j = x.testBit (i + j)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiInf_eq_of_not_forall : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {p : ι → Prop} {f : Subtype p → α},
  (¬∀ (i : ι), p i) → ⨅ i, ⨅ (h : p i), f ⟨i, h⟩ = min (iInf f) (sInf ∅)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_iff_prime_pow_dvd_dvd : ∀ (n d : ℕ), d ∣ n ↔ ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ d → p ^ k ∣ n
-- Mathlib.Topology.Order
dense_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] {s : Set α}, Dense s ↔ s = Set.univ
-- Mathlib.Order.Bounds.Basic
bddBelow_def : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s ↔ ∃ x, ∀ y ∈ s, x ≤ y
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientAddEquivOfEq_mk : ∀ {G : Type u} [inst : AddGroup G] {M N : AddSubgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N) (x : G),
  (QuotientAddGroup.quotientAddEquivOfEq h) ↑x = ↑x
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- If `P : InjectiveResolution X` and `F` is an additive functor, this is
the canonical morphism from `F.obj X` to the cycles in degree `0` of
`(F.mapHomologicalComplex _).obj P.cocomplex`.  -/
CategoryTheory.InjectiveResolution.toRightDerivedZero' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Abelian D] →
            {X : C} →
              (P : CategoryTheory.InjectiveResolution X) →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.Additive] →
                    F.obj X ⟶ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).cycles 0
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.instCartesianMonoidalCategoryOpposite : {R : Type u} → [inst : CommRing R] → CategoryTheory.CartesianMonoidalCategory (CommAlgCat R)ᵒᵖ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ) =
    1 + sizeOf e + sizeOf isoLift? + sizeOf f₁ + sizeOf g₁ + sizeOf f₂ + sizeOf g₂ + sizeOf η + sizeOf θ
-- Mathlib.Order.Atoms
GaloisInsertion.isCoatom_of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) {b : β}, IsCoatom (u b) → IsCoatom b
-- Std.Http.Data.Method
Std.Http.Method.baselineControl.sizeOf_spec : sizeOf Std.Http.Method.baselineControl = 1
-- Lean.Level
Lean.PLevelSet : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        (m₁.diff! m₂).getD k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback else m₁.getD k fallback
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.integrable_vectorMeasure_prodMk_left : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.VectorMeasure X E}
  {ν : MeasureTheory.VectorMeasure Y F} [MeasureTheory.IsFiniteMeasure μ.variation] {s : Set (X × Y)},
  MeasurableSet s → μ.Integrable fun x => ν (Prod.mk x ⁻¹' s)
-- Lean.Meta.Tactic.CasesOnStuckLHS
/-- Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
apply `cases xMajor`.  -/
Lean.Meta.casesOnStuckLHS : Lean.MVarId → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet_iff_iIndepSets_singleton : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ι → Set Ω},
  (∀ (i : ι), MeasurableSet (f i)) →
    (ProbabilityTheory.Kernel.iIndepSet f κ μ ↔ ProbabilityTheory.Kernel.iIndepSets (fun i => {f i}) κ μ)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.opOp.eq_1 : ∀ (M : Type u_3) [inst : Mul M],
  MulEquiv.opOp M = { toEquiv := MulOpposite.opEquiv.trans MulOpposite.opEquiv, map_mul' := ⋯ }
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.mk.injEq : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (inner inner_1 : Std.IterM m β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_union_of_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.center_eq_univ_iff_radius_eq_ediam : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.center = Set.univ ↔ G.radius = G.ediam
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- If `C` is a braided CCC with pushouts and an initial object, then `(⊥_ C ⟶ 𝟙_ C) □ X ≅ X`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          [inst_4 : CategoryTheory.Limits.HasInitial C] →
            [CategoryTheory.BraidedCategory C] →
              (X : CategoryTheory.Arrow C) →
                (CategoryTheory.Arrow.mk
                      (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) □
                    X) ≅
                  X
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.IsKProjective.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K : CochainComplex C ℤ},
  (∀ {L : CochainComplex C ℤ} (f : K ⟶ L), HomologicalComplex.Acyclic L → Nonempty (Homotopy f 0)) → K.IsKProjective
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey! ∈ t
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Derivative under integral of `x ↦ ∫ F x a` at a given point `x₀ : ℝ`, assuming
`F x₀` is integrable, `x ↦ F x a` is differentiable on an interval around `x₀` for ae `a`
(with interval radius independent of `a`) with derivative uniformly bounded by an integrable
function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasDerivAt_integral_of_dominated_loc_of_deriv_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] {bound : α → ℝ}
  {F : 𝕜 → α → E} {x₀ : 𝕜} {s : Set 𝕜},
  s ∈ nhds x₀ →
    (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        ∀ {F' : 𝕜 → α → E},
          MeasureTheory.AEStronglyMeasurable (F' x₀) μ →
            (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a) →
              MeasureTheory.Integrable bound μ →
                (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x => F x a) (F' x a) x) →
                  MeasureTheory.Integrable (F' x₀) μ ∧
                    HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
-- Init.Data.BitVec.Lemmas
BitVec.slt.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.slt y = decide (x.toInt < y.toInt)
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to unit length.  -/
norm_smul_inv_norm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E},
  x ≠ 0 → ‖(↑‖x‖)⁻¹ • x‖ = 1
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff.eq_def : ∀ (p : Int.Internal.Linear.Poly) (x : Int.Internal.Linear.Var),
  p.coeff x =
    match p with
    | Int.Internal.Linear.Poly.add a y p => bif x == y then a else p.coeff x
    | Int.Internal.Linear.Poly.num k => 0
-- Mathlib.Algebra.Homology.Localization
/-- The homology functor on `HomologicalComplexUpToQuasiIso C c` is induced by
the homology functor on `HomotopyCategory C c`.  -/
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Preadditive C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              [inst_4 : c.QFactorsThroughHomotopy C] →
                (i : ι) →
                  HomologicalComplexUpToQuasiIso.Qh.comp (HomologicalComplexUpToQuasiIso.homologyFunctor C c i) ≅
                    HomotopyCategory.homologyFunctor C c i
-- Mathlib.Topology.Defs.Induced
Topology.IsClosedEmbedding.toIsEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → Topology.IsEmbedding f
-- Batteries.Recycling.RBTree.Basic
/-- Returns the root of the tree, if any.  -/
RBTree.RBNode.root? : {α : Type u_1} → RBTree.RBNode α → Option α
-- Mathlib.RingTheory.Henselian
/-- [Stacks Tag 06RR](https://stacks.math.columbia.edu/tag/06RR) -/
IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub : ∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R] {f : Polynomial R} {a b : R},
  Polynomial.eval a f = 0 →
    Polynomial.eval b f = 0 → ¬IsUnit (a - b) → IsUnit (Polynomial.eval a (Polynomial.derivative f)) → a = b
-- Mathlib.Data.EReal.Basic
EReal.coe_eq_one : ∀ {x : ℝ}, ↑x = 1 ↔ x = 1
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.triviallyComplete : Lean.Meta.Match.Problem → Bool
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.isValidAtom : String → Bool
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.tensorQuotientTensorEquiv_symm_tmul : ∀ {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing R']
  [inst_2 : CommRing R''] [inst_3 : CommRing S] [inst_4 : Algebra R R'] [inst_5 : Algebra R R'']
  [inst_6 : Algebra R' R''] [inst_7 : IsScalarTower R R' R''] [inst_8 : Algebra R S] (e : TensorProduct R R' S)
  (a : R'') (b : S),
  (Algebra.tensorQuotientTensorEquiv R'' e).symm
      ((Ideal.Quotient.mk (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e})) (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (1 ⊗ₜ[R] b)
-- Init.Grind.AC
Lean.Grind.AC.superpose_tail_idempotent_cert : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Lindelöf if and only if
for every family of closed sets whose intersection avoids `s`,
there exists a countable subfamily whose intersection avoids `s`.  -/
isLindelof_iff_countable_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s ↔
    ∀ {ι : Type u} (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
-- Lean.Meta.Tactic.Grind.Types
/-- Beta-reduction.  -/
Lean.Meta.Grind.SplitSource.beta : Lean.Expr → Lean.Meta.Grind.SplitSource
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  a ∉ t → t.get! a = default
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_rocIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound upperBound : α},
  (Std.DTreeMap.Internal.rocIterator t lowerBound upperBound).toList =
    List.filter (fun e => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true))
      t.toList
-- Batteries.Lean.Meta.UnusedNames
Lean.Name.MatchUpToIndexSuffix.suffixMatch.injEq : ∀ (i i_1 : ℕ),
  (Lean.Name.MatchUpToIndexSuffix.suffixMatch i = Lean.Name.MatchUpToIndexSuffix.suffixMatch i_1) = (i = i_1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_assoc : ∀ {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) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C}
  (h_1 : CategoryTheory.Functor.id C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b h)
      (CategoryTheory.CategoryStruct.comp (t.truncLEι b) h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncLEι a) h_1
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_neg_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), (-o).rightAngleRotation x = -o.rightAngleRotation x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.dist_toBCF_eq_dist : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  {f g : ZeroAtInftyContinuousMap α β}, dist f.toBCF g.toBCF = dist f g
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The inclusion functor `BifibrantObject.HoCat C ⥤ CofibrantObject.HoCat C`.  -/
HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject.HoCat C) (HomotopicalAlgebra.CofibrantObject.HoCat C)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_above_dvd`. -/
Ideal.inertiaDeg'_above_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], r.inertiaDeg S ∣ r.inertiaDeg R
-- Mathlib.Topology.Algebra.InfiniteSum.Order
lt_hasSum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop]
  [AddRightStrictMono α], HasSum f a L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 0 ≤ f j) → ∀ (j : ι), j ≠ i → 0 < f j → f i < a
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.castAdd m) (Finset.uIcc i j) = Finset.uIcc (Fin.castAdd m i) (Fin.castAdd m j)
-- Init.Data.Array.Range
Array.map_add_range' : ∀ {a : ℕ} (s n step : ℕ), Array.map (fun x => a + x) (Array.range' s n step) = Array.range' (a + s) n step
-- Mathlib.Algebra.Group.Basic
nsmul_zero_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℕ), n • (0 - a) = 0 - n • a
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySeparatedFor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {E : J.OneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  CategoryTheory.Presieve.IsSeparated J F → E.IsStronglySeparatedFor F
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_nil : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) (a : V),
  F.mapPath Quiver.Path.nil = Quiver.Path.nil
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.map_natDegree_eq_sub : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {F : Type u_3} [inst_1 : Semiring S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F}
  {p : Polynomial R} {k : ℕ},
  (∀ (f : Polynomial R), f.natDegree < k → φ f = 0) →
    (∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n - k) → (φ p).natDegree = p.natDegree - k
-- Mathlib.Logic.Equiv.Set
Equiv.setCongr_symm_apply : ∀ {α : Type u_3} {s t : Set α} (h : s = t) (b : { b // (fun x => x ∈ t) b }), (Equiv.setCongr h).symm b = ⟨↑b, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_natCast' : ∀ {x y : ℝ} {n : ℕ}, 0 ≤ x → y - ↑n ≠ 0 → x ^ (y - ↑n) = x ^ y / x ^ n
-- Mathlib.RingTheory.Congruence.Hom
/-- If `c` is a ring congruence on `M`, then the smallest ring
congruence relation on `N` deduced from `c` by a ring homomorphism
from `M` to `N` is the relation deduced from `c`.  -/
RingCon.mapGen_eq_map_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M} (f : M →+* N),
  RingCon.ker f ≤ c → Function.Surjective ⇑f → ⇑(RingCon.mapGen ⇑f) = Relation.Map ⇑c ⇑f ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The proposition that a Jacobian point representative `(x, y, z)` lies in a Weierstrass curve
`W`.

In other words, it satisfies the `(2, 3, 1)`-homogeneous Weierstrass equation `W(X, Y, Z) = 0`.  -/
WeierstrassCurve.Jacobian.Equation : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → Prop
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk_coe : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N)
  (h : ∀ {x : L} {m : M}, (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆), { toLinearMap := ↑f, map_lie' := h } = f
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (self : CategoryTheory.PresheafOfGroups.OneCochain G U) (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i)
  (b : T' ⟶ U j),
  (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (self.ev i j a b) =
    self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.finiteType : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {α : Type u_2} [Finite α]
  (P : Algebra.Generators R S α), Algebra.FiniteType R S
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.isSMulRegular_of_le_basicOpen : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U : (AlgebraicGeometry.Spec R).Opens} {f : ↑R},
  U ≤ PrimeSpectrum.basicOpen f → IsSMulRegular (↑(M.presheaf.obj (Opposite.op U))) f
-- Mathlib.Computability.EpsilonNFA
εNFA.step_one : ∀ {α : Type u} {σ : Type v} (s : σ) (a : Option α), εNFA.step 1 s a = ∅
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonMeasure_singleton : ∀ (r : NNReal) (n : ℕ),
  (ProbabilityTheory.poissonMeasure r) {n} = ENNReal.ofReal (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial)