mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} [inst_4 : Nonempty ↥as]
  [inst_5 : as.direction.HasOrthogonalProjection],
  s.IsTangent as ↔ s.IsTangentAt (↑((EuclideanGeometry.orthogonalProjection as) s.center)) as
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorBasis.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), hA.eigenvectorBasis = (⋯.eigenvectorBasis ⋯).reindex (Fintype.equivOfCardEq ⋯)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- A real function whose derivative tends to minus infinity from the right at a point is not
differentiable on the right at that point  -/
not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi : ∀ (f : ℝ → ℝ) {a : ℝ},
  Filter.Tendsto (deriv f) (nhdsWithin a (Set.Ioi a)) Filter.atBot → ¬DifferentiableWithinAt ℝ f (Set.Ioi a) a
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (a a_1 : α), a = a_1 → UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors a_1
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- Any morphism to an initial object is split epi.  -/
CategoryTheory.Limits.initial.isSplitEpi_to : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} [inst_1 : CategoryTheory.Limits.HasInitial C]
  (f : Y ⟶ ⊥_ C), CategoryTheory.IsSplitEpi f
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasInserted : Lean.Widget.DiffTag
-- Mathlib.Topology.Algebra.Equicontinuity
equicontinuous_of_equicontinuousAt_zero : ∀ {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [inst : TopologicalSpace G] [inst_1 : UniformSpace M]
  [inst_2 : AddGroup G] [inst_3 : AddGroup M] [IsTopologicalAddGroup G] [IsUniformAddGroup M] [inst_6 : FunLike hom G M]
  [AddMonoidHomClass hom G M] (F : ι → hom), EquicontinuousAt (DFunLike.coe ∘ F) 0 → Equicontinuous (DFunLike.coe ∘ F)
-- Aesop.Rule.Name
Aesop.instToJsonBuilderName : Lean.ToJson Aesop.BuilderName
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesCokernel.π_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.π f))
      (CategoryTheory.Limits.PreservesCokernel.iso G f).hom =
    CategoryTheory.Limits.cokernel.π (G.map f)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_const_right : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (X : Ω → β) (c : β'),
  ProbabilityTheory.IndepFun X (fun x => c) μ
-- Plausible.Gen
Plausible.GenError.genError.inj : ∀ {a a_1 : String}, Plausible.GenError.genError a = Plausible.GenError.genError a_1 → a = a_1
-- Init.Data.Order.Ord
Std.OrientedOrd.eq_swap : ∀ {α : Type u} [inst : Ord α] [Std.OrientedOrd α] {a b : α}, compare a b = (compare b a).swap
-- Mathlib.Algebra.Order.Group.Basic
zsmul_strictMono_right : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ},
  0 < n → StrictMono fun x => n • x
-- Mathlib.Data.Nat.Factorization.PrimePow
isPrimePow_of_minFac_pow_factorization_eq : ∀ {n : ℕ}, n.minFac ^ n.factorization n.minFac = n → n ≠ 1 → IsPrimePow n
-- Init.Data.AC
Lean.Data.AC.instContextInformationContext : {α : Sort u_1} → Lean.Data.AC.ContextInformation (Lean.Data.AC.Context α)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Ioc : ∀ (a b : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Ioc a b)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- Right whiskering of a strong natural transformation between pseudofunctors
and a modification.  -/
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            (η ⟶ θ) → (ι : G ⟶ H) → CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.mapBifunctorAssociator.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (associator associator_1 : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃),
  associator = associator_1 →
    ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
      (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
      (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁)
      (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
      [inst_6 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
      [inst_7 :
        (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
                  (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
              X₃).HasMap
          ρ₁₂.q]
      [inst_8 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
      [inst_9 :
        (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
          ρ₂₃.q]
      [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
      [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃],
      CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃ =
        CategoryTheory.GradedObject.mapBifunctorAssociator associator_1 ρ₁₂ ρ₂₃ X₁ X₂ X₃
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddRightInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G},
  (∀ (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ) → μ.IsAddRightInvariant
-- Mathlib.Logic.Function.Basic
Function.Injective.antisymm_onFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [Std.Antisymm r], Std.Antisymm (Function.onFun r f)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_ι_mul : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (m : M)
  (x : CliffordAlgebra Q),
  (CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m * x) =
    (CliffordAlgebra.ι Q') m * (CliffordAlgebra.changeForm h) x -
      (CliffordAlgebra.contractLeft (B m)) ((CliffordAlgebra.changeForm h) x)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.toLinearMap_symm_lid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(TensorProduct.lid R M).symm = (TensorProduct.mk R R M) 1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent.  -/
Module.End.isNilpotent_restrict_genEigenspace_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ) (h : optParam (Set.MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯),
  IsNilpotent (LinearMap.restrict (f - μ • 1) h)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSymbolTag.beq : Lean.Lsp.SymbolTag → Lean.Lsp.SymbolTag → Bool
-- Mathlib.Order.InitialSeg
InitialSeg.mem_range_of_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a : α} {b : β},
  s b (f a) → b ∈ Set.range ⇑f
-- Mathlib.Logic.Equiv.Basic
/-- The type of all functions `X → Y` with prescribed values for all `x' ≠ x`
is equivalent to the codomain `Y`.  -/
Equiv.subtypeEquivCodomain : {X : Sort u_9} →
  {Y : Sort u_10} → [DecidableEq X] → {x : X} → (f : { x' // x' ≠ x } → Y) → { g // g ∘ Subtype.val = f } ≃ Y
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.showInferredTerminationBy : Lean.Option Bool
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorBasis.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A A_1 : Matrix n n 𝕜} (e_A : A = A_1)
  [inst_2 : DecidableEq n] (hA : A.IsHermitian), hA.eigenvectorBasis = ⋯.eigenvectorBasis
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exists_exp_neg_natCast_lt : ∀ {x : WithZero (Multiplicative ℤ)}, x ≠ 0 → ∃ k, WithZero.exp (-↑k) < x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend'_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Trivialization F proj)
  [inst_3 : Nonempty (B → F → Z)] (z : Z),
  ↑(Bundle.Trivialization.codExtend' hs e) z = (↑(↑e.toPretrivialization z).1, (↑e.toPretrivialization z).2)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- The minimal polynomial of a primitive `n`-th root of unity `μ` divides `cyclotomic n ℤ`.  -/
IsPrimitiveRoot.minpoly_dvd_cyclotomic : ∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
  IsPrimitiveRoot μ n → 0 < n → ∀ [CharZero K], minpoly ℤ μ ∣ Polynomial.cyclotomic n ℤ
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instRepr : {α : Type u} → {cmp : α → α → Ordering} → [Repr α] → Repr (Std.TreeSet.Raw α cmp)
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.epi_as_hom''_mkQ : ∀ {R : Type u} [inst : Ring R] {X : ModuleCat R} (U : Submodule R ↑X), CategoryTheory.Epi (ModuleCat.ofHom U.mkQ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
Std.Tactic.BVDecide.BVExpr.bitblast.blastSub : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Data.ENat.Lattice
ENat.add_biSup : ∀ {a : ℕ∞} {ι : Type u_4} {s : Set ι}, s.Nonempty → ∀ (f : ι → ℕ∞), a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
ContinuousOn.intervalIntegrable_of_Icc : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {u : ℝ → E} {a b : ℝ}, a ≤ b → ContinuousOn u (Set.Icc a b) → IntervalIntegrable u μ a b
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_submatrix : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11}
  (A : Matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o),
  (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_le : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → p ^ n.factorization p ≤ n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : α → δ → m' (ForInStep δ)} {init : δ}, (forIn m init fun a d => f a.fst d) = forIn m.keys init f
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_lt_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → T_gen✝ p F a < 1
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_left_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  b ≤ a → Set.Ioc (Order.pred b) a = insert b (Set.Ioc b a)
-- Mathlib.LinearAlgebra.Determinant
Module.Free.of_det_ne_one : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M},
  LinearMap.det f ≠ 1 → Module.Free R M
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_sub : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V),
  ⇑(s - t) = ⇑s - ⇑t
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal)
  (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : Delone.DeloneSet X),
  Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D =
    { carrier := ⇑f '' D.carrier, packingRadius := D.packingRadius / K₁, packingRadius_pos := ⋯,
      isSeparated_packingRadius := ⋯, coveringRadius := K₂ * D.coveringRadius, coveringRadius_pos := ⋯,
      isCover_coveringRadius := ⋯ }
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_sum : ∀ {α : Type u_1} (u : α → ℕ → ENNReal) (s : Finset α),
  ExpGrowth.expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, ExpGrowth.expGrowthSup (u x)
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_init : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_2} (m : ℕ) (h : m ≤ n) (v : (i : Fin (n + 1)) → α i),
  Fin.take m h (Fin.init v) = Fin.take m ⋯ v
-- Mathlib.Data.Sum.Order
Sum.Lex.boundedOrder : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [inst_1 : LE β] → [OrderBot α] → [OrderTop β] → BoundedOrder (α ⊕ₗ β)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable.  -/
MDifferentiableWithinAt.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {EM : Type u_6} [inst_12 : NormedAddCommGroup EM] [inst_13 : NormedSpace ℝ EM] {HM : Type u_7}
  [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [inst_15 : TopologicalSpace M]
  [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)}
  {s : Set M} {x : M},
  (MDiffAt[s] fun m => ⟨b m, v m⟩) x → (MDiffAt[s] fun m => ⟨b m, w m⟩) x → (MDiffAt[s] fun m => inner ℝ (v m) (w m)) x
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divRight_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a b : α), (OrderIso.divRight a) b = b / a
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.setLike : {V : Type u} → {G : SimpleGraph V} → {K : Set V} → SetLike (G.ComponentCompl K) V
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instIsEquivalenceActionTopModuleCatToActionTopModFunc : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G],
  TopRep.toActionTopModFunc.IsEquivalence
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Commutative convolution ring structure on linear maps from a cocommutative coalgebra to an
algebra.  -/
LinearMap.convCommRing : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommMonoid C] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R C] →
                [inst_5 : Coalgebra R C] → [Coalgebra.IsCocomm R C] → CommRing (WithConv (C →ₗ[R] A))
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.homAux.eq_3 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex C c} (φ : (i j : ι) → K.X i ⟶ L.X j) (i j : ι),
  Homotopy.extend.homAux φ (some i) (some j) = φ i j
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The (exact) short complex `H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g)` of a
spectral object, when `f ≫ g = fg`.  -/
CategoryTheory.Abelian.SpectralObject.sc₂ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) → CategoryTheory.CategoryStruct.comp f g = fg → ℤ → CategoryTheory.ShortComplex C
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsEmbedding.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsEmbedding f), Topology.IsEmbedding (TopologicalSpace.Compacts.map f ⋯)
-- Mathlib.Data.ENNReal.Basic
ENNReal.zero_eq_coe : ∀ {r : NNReal}, 0 = ↑r ↔ 0 = r
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G₀` is a group with zero with measurable multiplication, then right multiplication by a
nonzero element `g : G₀` is a measurable automorphism of `G₀`.  -/
MeasurableEquiv.mulRight₀ : {G₀ : Type u_2} →
  [inst : GroupWithZero G₀] → [inst_1 : MeasurableSpace G₀] → [MeasurableMul G₀] → (g : G₀) → g ≠ 0 → G₀ ≃ᵐ G₀
-- Mathlib.Algebra.Order.Floor.Ring
Mathlib.Meta.Positivity.int_ceil_pos : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 < a → 0 < ⌈a⌉
-- Mathlib.Data.Finsupp.Basic
/-- Given a finitely supported function `f` from a product type `α × β` to `γ`,
`curry f` is the "curried" finitely supported function from `α` to the type of
finitely supported functions from `β` to `γ`.  -/
Finsupp.curry : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → (α × β →₀ M) → α →₀ β →₀ M
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instLawfulUpwardEnumerableLEInt : Std.PRange.LawfulUpwardEnumerableLE ℤ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Total.toArray.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] (it it_1 : Std.IterM.Total m β), it = it_1 → it.toArray = it_1.toArray
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree.eq_1 : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree = (f.aroots f.SplittingField).toFinset.card
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id η).as.app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Init.Data.List.Monadic
List.idRun_forIn_yield_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → Id β) (init : β),
  (forIn l init fun a b => ForInStep.yield <$> f a b).run = List.foldl (fun b a => (f a b).run) init l
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_near_20 : |Real.exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_symm : ∀ {𝕜 : 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'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M'}, x ∈ e.target → MDiffAt ↑e.symm x
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (position : Lean.Lsp.Position),
  sizeOf { textDocument := textDocument, position := position } = 1 + sizeOf textDocument + sizeOf position
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.
There is a pigeonhole with at least as many pigeons as
the ceiling of the average number of pigeons across all pigeonholes.
("The maximum is at least the mean" specialized to integers.)

More formally, given a function `f` between finite types `α` and `β` and a number `n` such that
`card β * n < card α`, there exists an element `y : β` such that its preimage has more than `n`
elements.  -/
Fintype.exists_lt_card_fiber_of_mul_lt_card : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ},
  Fintype.card β * n < Fintype.card α → ∃ y, n < {x | f x = y}.card
-- Init.Data.List.OfFn
Fin.foldl_cons_eq_append : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α},
  Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs