mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E),
  CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Iso.refl F) G = CategoryTheory.Iso.refl (F.comp G)
-- Init.Data.List.Pairwise
List.Pairwise.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, l₁.Sublist l₂ → List.Pairwise R l₂ → List.Pairwise R l₁
-- Lean.DocString.Syntax
/-- Anonymous positional argument  -/
Lean.Doc.Syntax.anon : Lean.ParserDescr
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isPeriodicPt_piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} {n : ℕ},
  Function.IsPeriodicPt (Pi.map f) n x ↔ ∀ (i : ι), Function.IsPeriodicPt (f i) n (x i)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The supremum of an increasing sequence  -/
OmegaCompletePartialOrder.ωSup : {α : Type u_6} → [self : OmegaCompletePartialOrder α] → OmegaCompletePartialOrder.Chain α → α
-- Lean.CoreM
Lean.Core.instNonemptyContext : Nonempty Lean.Core.Context
-- Init.Data.UInt.Basic
/-- Converts a natural number to a `USize`. Overflow is impossible on any supported platform because
`USize.size` is either `2^32` or `2^64`.

This function is overridden at runtime with an efficient implementation.
 -/
USize.ofNat32 : (n : ℕ) → n < 4294967296 → USize
-- Mathlib.Order.SupIndep
/-- **Alias** of the reverse direction of `iSupIndep_iff_supIndep_univ`.

---

A variant of `iSupIndep_comp_coe_iff_supIndep` for `Fintype`s.  -/
Finset.SupIndep.iSupIndep_of_univ : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
  Finset.univ.SupIndep f → iSupIndep f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_LpToLpOfMeasureLeSMul : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal}
  [inst_2 : Fact (1 ≤ p)] (hc : c ≠ ⊤) (h : μ ≤ c • ν) (f : ↥(MeasureTheory.Lp E p ν)),
  ↑↑((MeasureTheory.Lp.LpToLpOfMeasureLeSMul hc h) f) =ᵐ[μ] ↑↑f
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
/-- The **Data Processing Inequality** for the Kullback-Leibler divergence and a Markov kernel.  -/
InformationTheory.klDiv_comp_right_le : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  [ProbabilityTheory.IsMarkovKernel κ], InformationTheory.klDiv (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ InformationTheory.klDiv μ ν
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_zero : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ↑0 = ⊥
-- Mathlib.Data.Seq.Basic
Stream'.Seq.append_assoc : ∀ {α : Type u} (s t u : Stream'.Seq α), (s.append t).append u = s.append (t.append u)
-- Mathlib.Analysis.Polynomial.Order
Polynomial.negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos : ∀ {P : Polynomial ℝ} {x : ℝ},
  (∀ (y : ℝ), P.IsRoot y → x ≤ y) → P.leadingCoeff ≤ 0 → ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P ≤ 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.left_invariance : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'},
      e' ∈ G' → ContinuousWithinAt f s x → f x ∈ e'.source → (P (↑e' ∘ f) s x ↔ P f s x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.contains_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_ExceptT_lift : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α ε' : Type u} {x : ExceptT ε' m α} {h : ε → ExceptT ε' m α}
  [inst : Std.Do.WP m ps] [inst_1 : MonadExceptOf ε m] (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' ps)),
  ⦃(Std.Do.wp (MonadExceptOf.tryCatch x h)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)⦄
    MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.lift_zero : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G], ↑0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono : ∀ {n d : ℕ} (f : { len := d } ⟶ { len := n }),
  SSet.stdSimplex.objEquiv.symm f ∈ (SSet.stdSimplex.obj { len := n }).nonDegenerate d ↔ CategoryTheory.Mono f
-- Mathlib.Analysis.Calculus.Deriv.Inv
derivWithin_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x →
      d x ≠ 0 → derivWithin (c / d) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2
-- Mathlib.NumberTheory.GaussSum
/-- When `R'` has prime characteristic `p`, then the `p`th power of the Gauss sum
of `χ` and `ψ` is the Gauss sum of `χ^p` and `ψ^p`.  -/
gaussSum_frob : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
  [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (χ : MulChar R R') (ψ : AddChar R R'),
  gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
-- Std.Data.DHashMap.Internal.Defs
_private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.Raw₀.expand.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β))
  (target : { d // 0 < d.size }),
  Std.DHashMap.Internal.Raw₀.expand.go✝ i source target =
    if h : i < source.size then
      have es := source[i];
      have source := source.set i Std.DHashMap.Internal.AssocList.nil h;
      have target := Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target es;
      Std.DHashMap.Internal.Raw₀.expand.go✝ (i + 1) source target
    else target
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalGroup.t2Space_iff_one_closed : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G], T2Space G ↔ IsClosed {1}
-- Mathlib.CategoryTheory.Abelian.Injective.Basic
/-- The preadditive Yoneda functor on `J` preserves homology if `J` is injective.  -/
CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (J : C)
  [hJ : CategoryTheory.Injective J], (CategoryTheory.preadditiveYonedaObj J).PreservesHomology
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift_symm_injective_of_injective : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β] {f : WithZero α →+ β},
  Function.Injective ⇑f → Function.Injective ⇑(WithZero.lift.symm f)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  IsProperLinearSet.fract✝ hs x =
    x + ∑ i, (-IsProperLinearSet.floor✝ hs x i).toNat • ↑i - ∑ i, (IsProperLinearSet.floor✝ hs x i).toNat • ↑i
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum' : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M), iSupIndep u.stratum'
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffWithinAt.cle_arrowCongr : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂}
  {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun x => ↑(f x).symm) s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun x => ↑(g x)) s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n
        (fun y => ↑((f y).arrowCongr (g y))) s x
-- Mathlib.Order.WithBot
WithTop.coe_le_coe : ∀ {α : Type u_1} {a b : α} [inst : LE α], ↑b ≤ ↑a ↔ b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g)
  {Z : C} (h : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelPair.one) h =
    CategoryTheory.CategoryStruct.comp s.ι (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.isIso_of_isDiscrete : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsDiscrete C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂),
  L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.eq_of_eq_of_eq : ∀ {α : Type u_1} [inst : Semiring α] {a b : α}, a = 0 → b = 0 → a + b = 0
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.orderIsoSubobject_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (A : CategoryTheory.Subfunctor F), (CategoryTheory.Subfunctor.orderIsoSubobject F) A = CategoryTheory.Subobject.mk A.ι
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.evenOdd_map_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (n : ZMod 2),
  Submodule.map CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toArray.congr_simp : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] (r r_1 : Std.Rii α),
  r = r_1 →
    ∀ [inst_2 : Std.Iterator (Std.Rxi.Iterator α) Id α] [inst_3 : Std.Iterators.Finite (Std.Rxi.Iterator α) Id],
      r.toArray = r_1.toArray
-- Mathlib.Order.Lattice
inf_eq_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ↔ b ≤ a
-- Mathlib.Order.Partition.Basic
/-- The parts are `sSupIndep`.  -/
Partition.sSupIndep' : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} (self : Partition s), sSupIndep self.parts
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_sub : ∀ {R : Type u} {M : Type v} [inst : Sub R] [inst_1 : Sub M] (x₁ x₂ : TrivSqZeroExt R M), (x₁ - x₂).snd = x₁.snd - x₂.snd
-- Lean.Expr
Lean.mkFVarEx : Lean.FVarId → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.minDegree_mono : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] {f : G.Copy H},
  Function.Surjective ⇑f → G.minDegree ≤ H.minDegree
-- Mathlib.Logic.Basic
/-- **Alias** of `imp_congr`. -/
Iff.imp : ∀ {a b c d : Prop}, (a ↔ c) → (b ↔ d) → (a → b ↔ c → d)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_eq_zero_of_not_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ι → M), ¬Function.Injective v → f v = 0
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.wideSpan_obj : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows : (j : J) → B ⟶ objs j) (j : CategoryTheory.Limits.WidePushoutShape J),
  (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).obj j = Option.casesOn j B objs
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.reindex_updateCol : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq o]
  [inst_1 : DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : m ≃ l) (f : n ≃ o),
  (Matrix.reindex e f) (A.updateCol j c) = ((Matrix.reindex e f) A).updateCol (f j) fun i => c (e.symm i)
-- Mathlib.Data.Sum.Order
Sum.denselyOrdered : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [DenselyOrdered α] [DenselyOrdered β],
  DenselyOrdered (α ⊕ β)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.adjoin_range_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], Algebra.adjoin R (Set.range MvPolynomial.X) = ⊤
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.antitone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Antitone g → QuasiconvexOn 𝕜 s f → QuasiconcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Topology.Category.Sequential
Sequential.isoEquivHomeo_apply : ∀ {X Y : Sequential} (f : X ≅ Y), Sequential.isoEquivHomeo f = Sequential.homeoOfIso f
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The norm of any root of `p` is bounded by the spectral value of `p`. See
[S. Bosch, U. Güntzer, R. Remmert, *Non-Archimedean Analysis* (Proposition 3.1.2/1(1))]
[bosch-guntzer-remmert].  -/
norm_root_le_spectralValue : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f → ∀ {p : Polynomial K}, p.Monic → ∀ {x : L}, (Polynomial.aeval x) p = 0 → f x ≤ spectralValue p
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- The main loop for `encodeExpr`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodeExprWithEta.go : Array (Array Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry) →
  Array (Array Lean.Meta.RefinedDiscrTree.Key) → Lean.MetaM (Array (Array Lean.Meta.RefinedDiscrTree.Key))
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrRight_symm : ∀ {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [inst : (i : ι) → TopologicalSpace (Y₁ i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i),
  (Homeomorph.piCongrRight F).symm = Homeomorph.piCongrRight fun i => (F i).symm
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the two vectors passed to `oangle` are the same, the result is 0.  -/
Orientation.oangle_self : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle x x = 0
-- Init.Core
ULift.up.injEq : ∀ {α : Type s} (down down_1 : α), ({ down := down } = { down := down_1 }) = (down = down_1)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_mul : ∀ {R : Type u_1} [inst : Semiring R] {a b : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C (a * b) = SkewPolynomial.C a * SkewPolynomial.C b
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.mod : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n x → Function.IsPeriodicPt f (m % n) x
-- Mathlib.Algebra.Order.Ring.Abs
/-- If `a` is even, then `n` is even iff `n % a` is even.  -/
Even.mod_even_iff : ∀ {n a : ℕ}, Even a → (Even (n % a) ↔ Even n)
-- Mathlib.Tactic.Module
/-- Postprocessing for the scalar goals constructed in the `match_scalars` and `module` tactics.
These goals feature a proliferation of `algebraMap` operations (because the scalars start in `ℕ` and
get successively bumped up by `algebraMap`s as new semirings are encountered), so we reinterpret the
most commonly occurring `algebraMap`s (those out of `ℕ`, `ℤ` and `ℚ`) into their standard forms
(`ℕ`, `ℤ` and `ℚ` casts) and then try to disperse the casts using the various `push_cast` lemmas.  -/
Mathlib.Tactic.Module.postprocess : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
analyticOnNhd_log : AnalyticOnNhd ℝ Real.log (Set.Ioi 0)
-- Mathlib.Data.Multiset.AddSub
Multiset.mem_sub_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Multiset α}, s.Nodup → (a ∈ s - t ↔ a ∈ s ∧ a ∉ t)
-- Mathlib.Data.Bool.Basic
Bool.right_le_or : ∀ (x y : Bool), y ≤ (x || y)
-- Init.Data.UInt.Bitwise
USize.ofFin_shiftRight_mod : ∀ (a b : Fin USize.size),
  USize.ofFin (a >>> (b % ⟨System.Platform.numBits, USize.ofFin_shiftLeft_mod._proof_1⟩)) =
    USize.ofFin a >>> USize.ofFin b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_coeMulHom : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Monoid M], ⇑(Filter.Germ.coeMulHom l) = Filter.Germ.ofFun
-- Std.Http.Data.Extensions
Std.Http.instInhabitedExtensions : Inhabited Std.Http.Extensions
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.rangeKerLift_injective : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  Function.Injective ⇑(QuotientGroup.rangeKerLift φ)
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roo_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced_le : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε δ : 𝕜},
  SimpleGraph.regularityReduced P G ε δ ≤ G
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
/-- The Dold-Kan equivalence `Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)`
for additive categories.  -/
CategoryTheory.Preadditive.DoldKan.equivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C) ≌
          CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.ofMeasure.sizeOf_spec : ∀ {α : Type u_2} [inst : SizeOf α] (toMeasure : α),
  sizeOf (MeasureTheory.LevyProkhorov.ofMeasure toMeasure) = 1 + sizeOf toMeasure
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.toAddCommMonoid : {α : Type u_3} → [self : LinearOrderedAddCommMonoidWithTop α] → AddCommMonoid α
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_id_apply : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R), (MvPolynomial.rename id) p = p
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → Differentiable 𝕜 f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homAddEquiv_symm_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M),
  (CategoryTheory.Functor.FullyFaithful.homAddEquiv F hF).symm f = hF.preimage f
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_natCard : ∀ {G : Type u_6} [inst : AddGroup G] (x : G), addOrderOf x ∣ Nat.card G
-- Mathlib.Order.Heyting.Basic
sdiff_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ (b ⊓ c) = a \ b ⊔ a \ c
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Reinterpret a `Subring` as a `Subsemiring`.  -/
Subring.toSubsemiring : {R : Type u} → [inst : NonAssocRing R] → Subring R → Subsemiring R
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).pt = t.pt
-- Std.Internal.Do.WP.Basic
/-- A monadic `WP` interpretation is sourced from the monad's `WPMonad` instance. Low priority so a
program type with a bespoke `WP` instance (e.g. a non-monadic one) is preferred.  -/
Std.Internal.Do.instWPOfWPMonad : {m : Type u → Type v} →
  {Pred : Type w} →
    {EPred : Type w'} →
      {α : Type u} →
        [inst : Monad m] →
          [inst_1 : Std.Internal.Do.Assertion Pred] →
            [inst_2 : Std.Internal.Do.Assertion EPred] →
              [inst : Std.Internal.Do.WPMonad m Pred EPred] → Std.Internal.Do.WP (m α) α Pred EPred
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_id : ∀ {V : Type u_1} {G : SimpleGraph V}, SimpleGraph.comap id G = G
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]? = m[k]?
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], -⊥ = ⊥
-- Init.Data.BitVec.Basic
/-- `smulOverflow x y` returns `true` if multiplying `x` and `y` results in *signed* overflow,
treating `x` and `y` as 2's complement signed bitvectors.

  SMT-Lib name: `bvsmulo`.
 -/
BitVec.smulOverflow : {w : ℕ} → BitVec w → BitVec w → Bool