mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A free variable. It stores the `FVarId` and the arity.  -/
Lean.Meta.RefinedDiscrTree.Key.fvar : Lean.FVarId → ℕ → Lean.Meta.RefinedDiscrTree.Key
-- Init.Data.Nat.Dvd
Nat.le_of_dvd : ∀ {m n : ℕ}, 0 < n → m ∣ n → m ≤ n
-- Init.Data.List.MinMaxOn
List.get_minOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  (List.minOn? f xs).get ⋯ = List.minOn f xs h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      t.isEmpty = true → ∀ {fallback : α}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKeyD fallback = k
-- Mathlib.Data.Set.Basic
Equiv.setSubtypeComm_symm_apply : ∀ {α : Type u_1} (p : α → Prop) (s : { s // ∀ a ∈ s, p a }), (Equiv.setSubtypeComm p).symm s = {a | ↑a ∈ ↑s}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.unop),
  CategoryTheory.Limits.coconeUnopOfConeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c)
-- Init.Data.Array.Attach
Array.size_attach : ∀ {α : Type u_1} {xs : Array α}, xs.attach.size = xs.size
-- Mathlib.Analysis.Convex.Gauge
gauge_pos : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [T1Space E], Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → (0 < gauge s x ↔ x ≠ 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasBinaryCoproductOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.Limits.HasBinaryCoproduct (Opposite.op A) (Opposite.op B)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.kind : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → Lean.Lsp.SymbolKind
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.quot_mk_eq_mk : ∀ {α : Type u} {L : List (α × Bool)}, Quot.mk FreeGroup.Red.Step L = FreeGroup.mk L
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsTopologicalGroup.leftUniformSpace.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup.leftUniformSpace G =
    { toTopologicalSpace := inst_1, uniformity := Filter.comap (fun p => p.1⁻¹ * p.2) (nhds 1), symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.isIso_map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso (F₁.map f) ↔ CategoryTheory.IsIso (F₂.map f)
-- Lean.Meta.Tactic.Intro
/-- Like `mkFreshBinderNameForTactic`, but takes the local context and `tactic.hygienic` value explicitly.
Use this variant when the relevant local context is being built incrementally and differs from the
ambient `← getLCtx` (e.g. when introducing several binders in a single pass).
 -/
Lean.Meta.mkFreshBinderNameForTacticCore : Lean.LocalContext → Lean.Name → optParam Bool true → Lean.MetaM Lean.Name
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.div_certC.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.div_certC p₁ k p c =
    (!k.beq' 0).and' ((Lean.Grind.CommRing.Poly.mulConstC k p c).beq' p₁)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mk.injEq : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] {m : MeasurableSpace Ω} (seq : ι → MeasurableSpace Ω)
  (mono' : Monotone seq) (le' : ∀ (i : ι), seq i ≤ m) (seq_1 : ι → MeasurableSpace Ω) (mono'_1 : Monotone seq_1)
  (le'_1 : ∀ (i : ι), seq_1 i ≤ m),
  ({ seq := seq, mono' := mono', le' := le' } = { seq := seq_1, mono' := mono'_1, le' := le'_1 }) = (seq = seq_1)
-- Init.Data.String.Iterator
/-- Moves the iterator's position forward by the specified number of characters.

The resulting iterator is only valid if the number of characters to skip is less than or equal
to the number of characters left in the iterator.
 -/
String.Legacy.Iterator.nextn : String.Legacy.Iterator → ℕ → String.Legacy.Iterator
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableAdd₂` if `uncurry (· + ·)` is a measurable function.
For a typeclass assuming measurability of `(c + ·)` and `(· + c)` see `MeasurableAdd`.  -/
MeasurableAdd₂ : (M : Type u_2) → [MeasurableSpace M] → [Add M] → Prop
-- Mathlib.Order.Notation
/-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order.  -/
Mathlib.Meta.delabInf : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equivFunctor_obj : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (D : Type u'')
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D]
  (X : CategoryTheory.ForgetEnrichment V D),
  (CategoryTheory.ForgetEnrichment.equivFunctor V D).obj X = CategoryTheory.ForgetEnrichment.to V X
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The defining properties of `Ind C` are that its morphisms live in `v` and that it is equivalent
to the full subcategory of `Cᵒᵖ ⥤ Type v` containing the ind-objects.  -/
CategoryTheory.Ind.equivalence : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Ind C ≌ CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Limits.IsIndObject
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.doubleCoset.eq_1 : ∀ {α : Type u_2} [inst : Mul α] (a : α) (s t : Set α), DoubleCoset.doubleCoset a s t = s * {a} * t
-- Init.Data.Sum.Basic
/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
respective order on `α` or `β`.  -/
Sum.Lex : {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → α ⊕ β → α ⊕ β → Prop
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk.inj : ∀ {B : Type u_1} {F : Type u_4} {E : B → Type u_5} {proj : B} {snd : E proj} {proj_1 : B} {snd_1 : E proj_1},
  ⟨proj, snd⟩ = ⟨proj_1, snd_1⟩ → proj = proj_1 ∧ snd ≍ snd_1
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.mk.congr_simp : ∀ {A : Type u_6} {B : Type u_7} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  (toMonoidHom toMonoidHom_1 : A →* B) (e_toMonoidHom : toMonoidHom = toMonoidHom_1)
  (map_star' : ∀ (a : A), (↑toMonoidHom).toFun (star a) = star ((↑toMonoidHom).toFun a)),
  { toMonoidHom := toMonoidHom, map_star' := map_star' } = { toMonoidHom := toMonoidHom_1, map_star' := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraAddEquivDirectSum_apply_support' : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : AddMonoidAlgebra M ι), (addMonoidAlgebraAddEquivDirectSum f).support' = Trunc.mk ⟨f.coeff.support.val, ⋯⟩
-- Init.Data.UInt.Basic
instAddUInt8 : Add UInt8
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).IsVeryGood
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ι_comp_t : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  (d : CategoryTheory.OrthogonalReflection.D₁ W Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι CategoryTheory.OrthogonalReflection.D₁.obj₁ d)
      (CategoryTheory.OrthogonalReflection.D₁.t W Z) =
    CategoryTheory.CategoryStruct.comp (↑d.fst).hom
      (CategoryTheory.Limits.Sigma.ι CategoryTheory.OrthogonalReflection.D₁.obj₂ d)
-- Init.Data.Nat.Bitwise.Basic
Nat.lor_eq : ∀ {m n : ℕ}, m.lor n = m ||| n
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.hasDerivAt_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₀ f₁ : 𝕜 → F} {f' : F} {x : 𝕜},
  f₀ =ᶠ[nhds x] f₁ → (HasDerivAt f₀ f' x ↔ HasDerivAt f₁ f' x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.left =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.left)
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_congr : ∀ {α : Type u_3} {β : Type u_4} (f : α ≃ β), ENat.card α = ENat.card β
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.boundary_zero : ∀ {n : ℕ} (c : Composition n), c.boundary 0 = 0
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], Colex.instOne = inst
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- If `w : InfinitePlace L` lies above `v : InfinitePlace K` and `v` is complex, then so is `w`.  -/
NumberField.InfinitePlace.LiesOver.isComplex_of_isComplex_under : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) {v : NumberField.InfinitePlace K} [w.LiesOver v], v.IsComplex → w.IsComplex
-- Mathlib.Data.TwoPointing
TwoPointing.ext_iff : ∀ {α : Type u_3} {x y : TwoPointing α}, x = y ↔ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 = y.toProd.2
-- Lean.DocString.Parser
/-- Recovers from a parse error by skipping input until one or more complete blank lines has been
skipped.
 -/
Lean.Doc.Parser.recoverBlock : Lean.Parser.ParserFn → optParam Lean.Parser.ParserFn Lean.Doc.Parser.skipFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise negation of set `-s` is defined as `{x | -x ∈ s}` in scope `Pointwise`.
It is equal to `{-x | x ∈ s}`, see `Set.image_neg_eq_neg`.  -/
Set.neg : {α : Type u_2} → [Neg α] → Neg (Set α)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.mul_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {E'' : Type u_7} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E''] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {N' : Type u_9} [inst_12 : TopologicalSpace N']
  [inst_13 : ChartedSpace H'' N'] {n : WithTop ℕ∞} {G : Type u_10} [inst_14 : Mul G] [inst_15 : TopologicalSpace G]
  [inst_16 : ChartedSpace H' G] [inst_17 : ContMDiffMul I' n G] (f g : ContMDiffMap I'' I' N' G n)
  (h : ContMDiffMap I I'' N N' n), (f * g).comp h = f.comp h * g.comp h
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams.mk.inj : ∀ {expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx}, { expr := expr } = { expr := expr_1 } → expr = expr_1
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits : ∀ (J : Type w) [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J]
  [CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J P.FullSubcategory
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Order.Category.BddDistLat
BddDistLat.comp_apply : ∀ {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toDistLat),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.left.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g), h.left = CategoryTheory.Retract.map h CategoryTheory.Arrow.leftFunc
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Any finite-dimensional vector space over a locally compact field is proper.
We do not register this as an instance to avoid an instance loop when trying to prove the
properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
explicitly when needed.  -/
FiniteDimensional.proper : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] (E : Type v) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E], ProperSpace E
-- Lean.Language.Basic
Lean.Language.SnapshotBundle.mk.inj : ∀ {α : Type} {old? : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))} {new : IO.Promise α}
  {old?_1 : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))} {new_1 : IO.Promise α},
  { old? := old?, new := new } = { old? := old?_1, new := new_1 } → old? = old?_1 ∧ new = new_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.sum_single_index : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid N] {m : M} {r : R}
  {h : M → R → N}, h m 0 = 0 → (MonoidAlgebra.single m r).coeff.sum h = h m r
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.model_singleton_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {φ : L.Sentence}, M ⊨ {φ} ↔ M ⊨ φ
-- Mathlib.Control.Monad.Writer
instMonadWriterStateTOfMonad : {M : Type u → Type v} → {ω σ : Type u} → [Monad M] → [MonadWriter ω M] → MonadWriter ω (StateT σ M)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
TopologicalSpace.Opens.instIsManifoldSubtypeMem : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I n M]
  (s : TopologicalSpace.Opens M), IsManifold I n ↥s
-- Mathlib.Order.Lattice
le_sup_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ b
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.tendsto_rpow_atTop_of_one_lt_base : ∀ {b : ENNReal}, 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atTop (nhds ⊤)
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `Homeomorph.quotientKerEquivRange`.

---

The homeomorphism `Quotient (Setoid.ker f) ≃ₜ Set.range f` given by a strict map `f`.
This is the homeomorphism obtained from the first isomorphism theorem.  -/
Topology.Homeomorph.quotientKerEquivRange : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsStrictMap f → Quotient (Setoid.ker f) ≃ₜ ↑(Set.range f)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Lazy entries for root of trie.  -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree.tries : {α : Type} → Lean.Meta.RefinedDiscrTree.PreDiscrTree α → Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α))
-- Mathlib.Data.ENNReal.Inv
ENNReal.top_div_coe : ∀ {p : NNReal}, ⊤ / ↑p = ⊤
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.etaFn.eq_1 : ∀ (G : GrpCat) (x : ↑G), ProfiniteGrp.ProfiniteCompletion.etaFn G x = ⟨fun x_1 => ↑x, ⋯⟩
-- Init.Grind.Module.Basic
Lean.Grind.NoNatZeroDivisors.eq_zero_of_mul_eq_zero : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [Lean.Grind.NoNatZeroDivisors α] {k : ℕ} {a : α},
  k ≠ 0 → k • a = 0 → a = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat.sizeOf_spec : ∀ (e : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e natStructId lhs rhs) =
    1 + sizeOf e + sizeOf natStructId + sizeOf lhs + sizeOf rhs
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_mul : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  sSup (s * t) = sSup s * sSup t
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (P : CategoryTheory.MorphismProperty D)
  (F : CategoryTheory.Functor C D) (X : D) [F.Faithful],
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P F X).Faithful
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.refl_comp : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G'), SimpleGraph.Iso.refl.comp f = f
-- Init.Data.UInt.Bitwise
UInt8.not_and_self : ∀ {a : UInt8}, ~~~a &&& a = 0
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.uncenteredCovarianceBilinDual.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E),
  ProbabilityTheory.uncenteredCovarianceBilinDual μ =
    ⋯.toContinuousLinearMap.bilinearComp (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)
-- Init.Data.Vector.Lemmas
Vector.sum_singleton : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulRightIdentity (fun x1 x2 => x1 + x2) 0] {x : α},
  #v[x].sum = x
-- Mathlib.Data.List.Perm.Basic
List.Perm.subset_congr_right : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Perm l₂ → (l₃ ⊆ l₁ ↔ l₃ ⊆ l₂)
-- Mathlib.Data.Set.Sups
Set.image_sups : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : FunLike F α β] [SupHomClass F α β] (f : F) (s t : Set α), ⇑f '' (s ⊻ t) = ⇑f '' s ⊻ ⇑f '' t
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.exists_triangle_zero_one : ∀ {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]
  (self : CategoryTheory.Triangulated.TStructure C) (A : C),
  ∃ X Y,
    ∃ (_ : self.le 0 X) (_ : self.ge 1 Y),
      ∃ f g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Analysis.Analytic.Composition
/-- Technical lemma stating how `p.applyComposition` commutes with updating variables. This
will be the key point to show that functions constructed from `applyComposition` retain
multilinearity.  -/
FormalMultilinearSeries.applyComposition_update : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) (j : Fin n)
  (v : Fin n → E) (z : E),
  p.applyComposition c (Function.update v j z) =
    Function.update (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z))
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ μ.sigmaFiniteSetᶜ = 0 → MeasureTheory.SigmaFinite μ
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Finset α} (s : Finset α) {x : α}, x ∈ t → insert x s \ t = s \ t
-- Mathlib.Algebra.DirectSum.Module
DirectSum.ext_component : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {f g : DirectSum ι fun i => M i},
  (∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g) → f = g
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableAt.eq_1 : ∀ {𝕜 : 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') (x : M),
  MDiffAt f x = ChartedSpace.LiftPropAt (DifferentiableWithinAtProp I I') f x
-- Mathlib.Logic.Relation
Relation.EqvGen.reflTransGen_le_eqvGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.ReflTransGen r ≤ Relation.EqvGen r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- a `CatCommSq` bundling the natural isomorphism `G ⋙ base ≅ right ⋙ G'`.  -/
CategoryTheory.Limits.CatCospanTransform.squareRight : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                (self : CategoryTheory.Limits.CatCospanTransform F G F' G') →
                                  CategoryTheory.CatCommSq G self.right self.base G'
-- Init.System.IOError
/-- An operation timed out.

This corresponds to the POSIX errors `ETIME`, and `ETIMEDOUT`.
 -/
IO.Error.timeExpired : UInt32 → String → IO.Error
-- Mathlib.Order.Heyting.Basic
Prod.instSDiff.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiff α] [inst_1 : SDiff β],
  Prod.instSDiff = { sdiff := fun b a => (b.1 \ a.1, b.2 \ a.2) }