mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_ones : ∀ {w : ℕ} (a : BitVec w), a &&& -1#w = a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- The canonical isomorphism from the opposite of the coproduct to the product in the opposite
category.
 -/
CategoryTheory.Limits.opCoproductIsoProduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      (Z : α → C) → [inst_1 : CategoryTheory.Limits.HasCoproduct Z] → Opposite.op (∐ Z) ≅ ∏ᶜ fun x => Opposite.op (Z x)
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (CategoryTheory.CategoryStruct.comp (K.D₁ c j j') h) =
    CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j')
      (CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j').hom h)
-- Mathlib.Order.Preorder.Chain
Flag.instBoundedOrderSubtypeMem : {α : Type u_1} → [inst : Preorder α] → [BoundedOrder α] → (s : Flag α) → BoundedOrder ↥s
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_refl : ∀ (α : Sort u_1), ⇑(Function.Embedding.refl α) = id
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.functor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (X Y : C), (CategoryTheory.Limits.coprod.functor.obj X).obj Y = (X ⨿ Y)
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.eqOn_Ioo_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X]
  {m : MeasurableSpace X} [inst_3 : TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {a b : X} {f g : X → Y},
  f =ᵐ[μ.restrict (Set.Ioo a b)] g →
    ContinuousOn f (Set.Ioo a b) → ContinuousOn g (Set.Ioo a b) → Set.EqOn f g (Set.Ioo a b)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isBigO_exp_comp_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ},
  ((fun x => Real.exp (f x)) =O[l] fun x => Real.exp (g x)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (f - g)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  0 ≤ᵐ[μ.restrict s] f → MeasureTheory.IntegrableOn f s μ → (∫ (x : X) in s, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict s] 0)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₃_of_right : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {left : Std.IterM m β₁}
  {b b' : Option { out // ∃ it, it.IsPlausibleOutput out }} {it' it : Std.IterM m β₂},
  b' = b →
    it'.finitelyManySkips.Rel it.finitelyManySkips →
      Std.Iterators.Types.Zip.Rel₃ m { internalState := { left := left, memoizedLeft := b', right := it' } }
        { internalState := { left := left, memoizedLeft := b, right := it } }
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getKey.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → Std.DTreeMap.Internal.Impl.contains k t = true → Sort u_3) (size : ℕ)
  (k' : α) (v : β k') (l r : Std.DTreeMap.Internal.Impl α β)
  (hlk : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) = true)
  (h_1 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hlk : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) = true) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v l r) hlk),
  (match Std.DTreeMap.Internal.Impl.inner size k' v l r, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v l r, hlk => h_1 size k' v l r hlk) =
    h_1 size k' v l r hlk
-- Mathlib.Data.Fintype.Pi
Singleton.singleton.hcongr_4 : ∀ (α α' : Type u),
  α = α' →
    ∀ (β β' : Type v),
      β = β' →
        ∀ (self : Singleton α β) (self' : Singleton α' β'), self ≍ self' → ∀ (a : α) (a' : α'), a ≍ a' → {a} ≍ {a'}
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
PrincipalSeg.cocone_ι_app : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β) {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_1, u_3} C] (F : CategoryTheory.Functor β C) (i : α),
  (f.cocone F).ι.app i = F.map (CategoryTheory.homOfLE ⋯)
-- Mathlib.Data.Set.Lattice.Image
Set.injective_iff_injective_of_iUnion_eq_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β},
  Set.iUnion U = Set.univ → (Function.Injective f ↔ ∀ (i : ι), Function.Injective ((U i).restrictPreimage f))
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.exists_finset_nhds' : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ∃ I,
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ∑ i ∈ I, (ρ i) x = 1) ∧
      ∀ᶠ (x : X) in nhds x₀, (Function.support fun x_1 => (ρ x_1) x) ⊆ ↑I
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeToSubmodule_eq_bot : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : FractionalIdeal S P}, ↑I = ⊥ ↔ I = 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? = Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? (i + 1) r.lower)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inverse.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
  f.inverse = (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).toLinearPMap
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_insert : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] (j : ι) [inst_2 : (i : ι) → Decidable (i ∈ insert j s)],
  (insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
-- Init.Data.String.Substring
Substring.Raw.prevn_zero : ∀ (s : Substring.Raw) (n : ℕ), s.prevn n 0 = 0
-- Mathlib.Data.Num.Lemmas
Num.cast_to_int : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : Num), ↑↑n = ↑n
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.smul_prod_smul : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  {S : Type u_1} [inst_10 : Monoid S] [inst_11 : DistribMulAction S M₂] [inst_12 : DistribMulAction S M₃]
  [inst_13 : ContinuousConstSMul S M₂] [inst_14 : SMulCommClass R S M₂] [inst_15 : ContinuousConstSMul S M₃]
  [inst_16 : SMulCommClass R S M₃] (c : S) (f : ContinuousMultilinearMap R M₁ M₂)
  (g : ContinuousMultilinearMap R M₁ M₃), (c • f).prod (c • g) = c • f.prod g
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.natCastFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Orientation
OrthonormalBasis.det_adjustToOrientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι],
  (e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_nnreal_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : NNReal), c ≠ 0 → MeasureTheory.llr (c • μ) ν =ᵐ[μ] fun x => MeasureTheory.llr μ ν x + Real.log ↑c
-- Mathlib.Analysis.Distribution.Sobolev
/-- The Laplacian maps `H ^ s` to `H ^ {s - 2}`.  -/
TemperedDistribution.MemSobolev.laplacian : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s 2 f → TemperedDistribution.MemSobolev (s - 2) 2 (Laplacian.laplacian f)
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.toUInt32 : ByteArray → UInt32
-- Init.Data.String.Basic
String.Pos.Raw.isValid_copy_iff : ∀ {s : String.Slice} {p : String.Pos.Raw}, String.Pos.Raw.IsValid s.copy p ↔ String.Pos.Raw.IsValidForSlice s p
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂CompMap₂Iso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {C' : Type u₆} [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] {D' : Type u₅}
  [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] {L'' : D'} {R'' : CategoryTheory.Functor C' D'}
  {F' : CategoryTheory.Functor C' C} {G' : CategoryTheory.Functor D' D} (α' : L ⟶ G'.obj L'')
  (β' : R''.comp G' ⟶ F'.comp R) (X : CategoryTheory.StructuredArrow L'' R''),
  ((CategoryTheory.StructuredArrow.map₂CompMap₂Iso α β α' β').inv.app X).right =
    CategoryTheory.CategoryStruct.id (F.obj (F'.obj X.right))
-- Init.Data.Char.Ordinal
Char.ofOrdinal_comp_ordinal : Char.ofOrdinal ∘ Char.ordinal = id
-- Mathlib.Algebra.Algebra.Equiv
LinearMap.mulLeftRight.congr_simp : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (ab ab_1 : A × A),
  ab = ab_1 → LinearMap.mulLeftRight R ab = LinearMap.mulLeftRight R ab_1
-- Lean.Widget.Commands
Lean.Widget.elabWidgetInstanceSpec : Lean.TSyntax `Lean.Widget.widgetInstanceSpec → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.instInhabited : (M : Type u_1) →
  [inst : Monoid M] →
    (X : Type u) → [inst_1 : MulAction M X] → [Inhabited X] → Inhabited (CategoryTheory.ActionCategory M X)
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- Variant of `threeδ₃Toδ₂` for preorders.  -/
CategoryTheory.ComposableArrows.threeδ₃Toδ₂' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) ⟶
              CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE ⋯)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.cast_skipSuffixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy), (s.skipSuffixWhile pat).cast hst = t.skipSuffixWhile pat
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_concat_succ : ∀ {w : ℕ} {x : BitVec w} {b : Bool} {i : ℕ}, (x.concat b).getLsbD (i + 1) = x.getLsbD i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The size of `s + s` is at least the size of `s`, version with left-cancellative addition.
See `card_le_card_add_self'` for the version with right-cancellative addition.  -/
Finset.card_le_card_add_self : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] {s : Finset α}, s.card ≤ (s + s).card
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.extensiveCoverage.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.extensiveCoverage C = CategoryTheory.extensiveCoverage C
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.instCoeParenthesizerAliasValue : Coe Lean.PrettyPrinter.Parenthesizer Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue
-- Mathlib.Algebra.RingQuot
RingQuot.instMonoidWithZero : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → MonoidWithZero (RingQuot r)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_le_zero : ∀ {α : Type u} [inst : Zero α] {a : α} [inst_1 : LE α], ↑a ≤ 0 ↔ a ≤ 0
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderSup.mk : {α : Type u_3} →
  [toPartialOrder : PartialOrder α] →
    [toSupSet : SupSet α] →
      (∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)) →
        ConditionallyCompletePartialOrderSup α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Init.Data.List.Nat.TakeDrop
List.getLast?_drop : ∀ {α : Type u_1} {i : ℕ} {l : List α}, (List.drop i l).getLast? = if l.length ≤ i then none else l.getLast?
-- Mathlib.RingTheory.Ideal.Maps
RingHom.comap_ker : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (f : S →+* R)
  (g : T →+* S), Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.isGeneratedBy_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type v) [tY : TopologicalSpace Y],
  Topology.IsGeneratedBy X Y ↔ Continuous ⇑Topology.WithGeneratedByTopology.equiv.symm
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * 2^-n`, then `f` is a Cauchy sequence.  -/
cauchySeq_of_edist_le_geometric_two : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal),
  C ≠ ⊤ → ∀ {f : ℕ → α}, (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) → CauchySeq f
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.instHaveLebesgueDecompositionSelf : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.HaveLebesgueDecomposition μ
-- Init.Data.SInt.Lemmas
Int8.toInt32_div_of_ne_right : ∀ (a b : Int8), b ≠ -1 → (a / b).toInt32 = a.toInt32 / b.toInt32
-- Mathlib.Order.KrullDimension
Order.coheight_eq_coe_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.coheight x = ↑n ↔
    Order.coheight x < ⊤ ∧ (n = 0 ∨ ∃ y > x, Order.coheight y = ↑n - 1) ∧ ∀ y > x, Order.coheight y < ↑n
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The
size of `s + t` is lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size
of the smallest subgroup.  -/
cauchy_davenport_minOrder_add : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
  s.Nonempty → t.Nonempty → min (AddMonoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s + t).card
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.mk.inj : ∀ {X : SSet.Truncated 1} {n : ℕ}
  {vertex : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 })}
  {arrow : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 })}
  {arrow_src :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.castSucc}
  {arrow_tgt :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.succ}
  {vertex_1 : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 })}
  {arrow_1 : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 })}
  {arrow_src_1 :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow_1 i) =
        vertex_1 i.castSucc}
  {arrow_tgt_1 :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow_1 i) =
        vertex_1 i.succ},
  { vertex := vertex, arrow := arrow, arrow_src := arrow_src, arrow_tgt := arrow_tgt } =
      { vertex := vertex_1, arrow := arrow_1, arrow_src := arrow_src_1, arrow_tgt := arrow_tgt_1 } →
    vertex = vertex_1 ∧ arrow = arrow_1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_one_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.coeff 1 0 = 1
-- Mathlib.Algebra.Field.Defs
/-- The inverse of `0` is `0` by convention.  -/
DivisionRing.inv_zero : ∀ {K : Type u_2} [self : DivisionRing K], 0⁻¹ = 0
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_mul_of_isUnit_left : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a u : M}, IsUnit u → UniqueFactorizationMonoid.radical (u * a) = UniqueFactorizationMonoid.radical a
-- Mathlib.Order.UpperLower.Closure
IsUpperSet.upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → ↑(upperClosure s) = s
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.map_id : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι], Module.DirectLimit.map (fun x => LinearMap.id) ⋯ = LinearMap.id
-- Mathlib.Topology.ContinuousMap.Basic
Setoid.quotientKerEquivOfSurjective.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Surjective f),
  Setoid.quotientKerEquivOfSurjective f hf = Setoid.quotientKerEquivOfSurjective f hf
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- `derivSeries p` is a power series for `fderiv 𝕜 f` if `p` is a power series for `f`,
see `HasFPowerSeriesOnBall.fderiv`.  -/
FormalMultilinearSeries.derivSeries : {𝕜 : 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] → FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
-- Mathlib.Analysis.Normed.Field.UnitBall
Submonoid.mem_unitClosedBall : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜] {x : 𝕜}, x ∈ Submonoid.unitClosedBall 𝕜 ↔ ‖x‖ ≤ 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → (Std.DHashMap.Raw.Const.alter m k f).contains k = (f (Std.DHashMap.Raw.Const.get? m k)).isSome
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a : B} {a' : C} (f : G.obj a ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a).hom f))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom))
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `X × {*}` is homeomorphic to `X`.  -/
Homeomorph.uniqueProd : (X : Type u_7) → (Y : Type u_8) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [Unique X] → X × Y ≃ₜ Y
-- Mathlib.Data.List.Flatten
/-- See also `getLast_flatten_eq_getLast_getLast`, which switches around the proof obligations.  -/
List.getLast_getLast_eq_getLast_flatten : ∀ {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.getLast hl ≠ []),
  (l.getLast hl).getLast hl' = l.flatten.getLast ⋯
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.dist_eq_tsum : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → PseudoMetricSpace (F i)]
  (x y : (i : ι) → F i), dist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i))
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_iff_forall_finite_subset_indep : ∀ {α : Type u_1} {I : Set α} {M : Matroid α} [M.Finitary], M.Indep I ↔ ∀ J ⊆ I, J.Finite → M.Indep J
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderiv_continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {x : E}
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  DifferentiableAt 𝕜 f x →
    (∀ (i : ι), DifferentiableAt 𝕜 (g i) x) →
      fderiv 𝕜 (fun x => (f x) fun x_1 => g x_1 x) x =
        (ContinuousAlternatingMap.apply 𝕜 F G fun x_1 => g x_1 x) ∘SL fderiv 𝕜 f x +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL fderiv 𝕜 (g i) x
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_eq_upperCrossingTime_of_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω} {M : ℕ},
  N ≤ M →
    MeasureTheory.upperCrossingTime a b f N n ω < N →
      MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω