mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_f : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).f = f
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instReprPosition : Repr Lean.Lsp.Position
-- Mathlib.Data.Set.Basic
Set.inter_subset_inter_left : ∀ {α : Type u} {s t : Set α} (u : Set α), s ⊆ t → s ∩ u ⊆ t ∩ u
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_ric : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f},
  (m.alter k f)[k'] = if heq : (k == k') = true then (f m[k]?).get ⋯ else m[k']
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.id : (X : CategoryTheory.Limits.WalkingParallelPair) → CategoryTheory.Limits.WalkingParallelPairHom X X
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- A (random) isomorphism between two algebraic closures of `R`.  -/
IsAlgClosure.equiv : (R : Type u) →
  [inst : CommRing R] →
    [IsDomain R] →
      (L : Type v) →
        (M : Type w) →
          [inst_2 : Field L] →
            [inst_3 : Field M] →
              [inst_4 : Algebra R M] →
                [inst_5 : Module.IsTorsionFree R M] →
                  [IsAlgClosure R M] →
                    [inst_7 : Algebra R L] → [inst_8 : Module.IsTorsionFree R L] → [IsAlgClosure R L] → L ≃ₐ[R] M
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData) {Z : C} (h_1 : h.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp h.homologyIso.hom h_1) =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.hom (CategoryTheory.CategoryStruct.comp h.π h_1)
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Iio : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], (Finset.Iio a).Nonempty ↔ ¬IsMin a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  (X_1 : C),
  X.tensorLeftUnmopIso.inv.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop X_1)
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Liff.symm : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type 2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Liff α f2 f1
-- Mathlib.Logic.Unique
instUniqueTrue : Unique True
-- Mathlib.Algebra.Homology.Opposite
/-- If `K` is a homological complex, then the homology of `K.op` identifies to
the opposite of the homology of `K`.  -/
HomologicalComplex.homologyOp : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (K : HomologicalComplex V c) →
            (i : ι) → [inst_2 : K.HasHomology i] → K.op.homology i ≅ Opposite.op (K.homology i)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- Assuming `α : R₀ ⟶ R.obj` is the sheafification map of a presheaf of rings `R₀`
and `φ : M₀.presheaf ⟶ A.obj` is the sheafification map of the underlying
sheaf of abelian groups of a presheaf of modules `M₀` over `R₀`, this is
the sheaf of modules over `R` which is obtained by endowing the sections of
`A.obj` with a scalar multiplication.  -/
PresheafOfModules.sheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [CategoryTheory.Presheaf.IsLocallySurjective J φ] → SheafOfModules R
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme_1 : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsIntegralHom
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.addLValArg.throwUnusableParameter : Option Lean.Expr → Lean.Expr → Bool → Lean.MetavarDecl → Lean.MetaM Unit
-- Std.Data.Internal.List.Associative
Std.Internal.List.forall_mem_keys_iff_forall_containsKey_getKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {p : α → Prop},
  Std.Internal.List.DistinctKeys l →
    ((∀ k ∈ Std.Internal.List.keys l, p k) ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true), p (Std.Internal.List.getKey k l h))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.alter t k f) k = f (Std.DTreeMap.Raw.Const.get? t k)
-- Init.Data.List.Monadic
List.zipWithM'_nil_right : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {l : List α} [inst : Monad m]
  {f : α → β → m γ}, List.zipWithM' f l [] = pure []
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- Special case of **Jensen's inequality** for `Nat.descFactorial`.  -/
descPochhammer_eval_le_sum_descFactorial : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ {ι : Type u_2} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ),
      (∀ i ∈ t, 0 ≤ w i) →
        ∑ i ∈ t, w i = 1 →
          ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i) →
            Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_bot_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.Kernel.Indep m' ⊥ κ μ
-- Mathlib.FieldTheory.IsSepClosed
/-- A (random) isomorphism between two separable closures of `K`.  -/
IsSepClosure.equiv : (K : Type u) →
  [inst : Field K] →
    (L : Type v) →
      (M : Type w) →
        [inst_1 : Field L] →
          [inst_2 : Field M] →
            [inst_3 : Algebra K M] → [IsSepClosure K M] → [inst_5 : Algebra K L] → [IsSepClosure K L] → L ≃ₐ[K] M
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition : ∀ {ι : Type u_1} [inst : Fintype ι] {c : NNReal} (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι),
  I.distortion ≤ c → ∀ (r : (ι → ℝ) → ↑(Set.Ioi 0)), ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_inter_self : ∀ {α : Type u_1} (s : Set α), sᶜ ∩ s = ∅
-- Lean.Meta.Eqns
/-- Returns `true` if `thmName` is an equational theorem.
 -/
Lean.Meta.isEqnThm : Lean.Name → Lean.CoreM Bool
-- Batteries.Data.Int
Int.testBit_ofBits : ∀ {n i : ℕ} (f : Fin n → Bool), (Int.ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else decide (Int.ofBits f < 0)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Two points are coplanar.  -/
coplanar_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), Coplanar k {p₁, p₂}
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.exp (f x)) x
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.unsat_of_limplies_and_incompatible : ∀ (α : Type u) {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 →
    Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : ↥H) (n : ℤ), ↑(n • x) = n • ↑x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_hom_apply_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [inst_1 : Unique X]
  (X_1 : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : ↑X_1.sections) (j : C)
  (x_1 : ((CategoryTheory.Functor.const C).obj X).obj j),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).hom.app X_1)) x).app
          j))
      x_1 =
    ↑x j
-- Mathlib.Data.Set.Insert
Set.insert_eq : ∀ {α : Type u_1} (x : α) (s : Set α), insert x s = {x} ∪ s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_congr_ae₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
-- Mathlib.Algebra.GroupWithZero.Associated
Irreducible.isUnit_iff_not_associated_of_dvd : ∀ {M : Type u_1} [inst : Monoid M] {x y : M}, Irreducible x → y ∣ x → (IsUnit y ↔ ¬Associated x y)
-- Mathlib.GroupTheory.MonoidLocalization.Finite
/-- The localization of a finitely generated monoid at a finitely generated submonoid
is finitely generated.  -/
AddLocalization.fg : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} [AddMonoid.FG M], S.FG → AddMonoid.FG (AddLocalization S)
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.flat : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.WeaklyEtale f], AlgebraicGeometry.Flat f
-- Mathlib.Algebra.Group.ULift
ULift.subNegAddMonoid : {α : Type u} → [SubNegMonoid α] → SubNegMonoid (ULift.{u_1, u} α)
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  Topology.IsInducing i → DenseRange i → IsDenseInducing i
-- Mathlib.Order.Interval.Finset.Nat
Nat.mem_Ioc_succ' : ∀ {b : ℕ} (a : ↥(Finset.Ioc b (b + 1))), a = ⟨b + 1, ⋯⟩
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The range of a ring homomorphism is a subsemiring. See Note [range copy pattern].  -/
RingHom.rangeS : {R : Type u} → {S : Type v} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (R →+* S) → Subsemiring S
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying type.  -/
AddSemigrp.carrier : AddSemigrp → Type u
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zipWith_def : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι]
  [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)]
  [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)]
  {f : (i : ι) → β₁ i → β₂ i → β i} {hf : ∀ (i : ι), f i 0 0 = 0} {g₁ : Π₀ (i : ι), β₁ i} {g₂ : Π₀ (i : ι), β₂ i},
  DFinsupp.zipWith f hf g₁ g₂ = DFinsupp.mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- In each step, a preimage is constructed from the preimage of the previous step by
subtracting this delta.  -/
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimageDelta : {R : Type u} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type w} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {f : M →ₗ[R] N} →
                    Function.Surjective ⇑f →
                      (x : AdicCompletion.AdicCauchySequence I N) →
                        {n : ℕ} → {y yₙ : M} → f y = ↑x (n + 1) → f yₙ = ↑x n → ↑{d | f ↑d = f (yₙ - y)}
-- Mathlib.Tactic.Simps.Basic
/-- Get the default `ParsedProjectionData` for structure `str`.
It first returns the direct fields of the structure in the right order, and then
all (non-subobject fields) of all parent structures. The subobject fields are precisely the
non-default fields.  -/
Simps.mkParsedProjectionData : Lean.Name → Lean.CoreM (Array Simps.ParsedProjectionData)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  Array.map Sigma.fst m.toArray = m.keysArray
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).inv
      (CategoryTheory.Limits.pullback.snd f g) =
    (CategoryTheory.Limits.pushout.inr f.unop g.unop).op
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_right_pure : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto Int.floor (nhdsWithin (↑n) (Set.Ici ↑n)) (pure n)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.toOuterMeasure_injective : ∀ {α : Type u_1} [inst : MeasurableSpace α], Function.Injective MeasureTheory.Measure.toOuterMeasure
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.id_edge : ∀ {X : SSet} (x₀ : X.obj (Opposite.op { len := 0 })),
  (SSet.Edge.id x₀).edge = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0)) x₀
-- Batteries.Data.Array.Scan
Array.scanl.eq_1 : ∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (as : Array α) (start stop : ℕ),
  Array.scanl f init as start stop = (Array.scanlM (fun x1 x2 => pure (f x1 x2)) init as start stop).run
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`.  -/
fderiv_neg : ∀ {𝕜 : 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}
  {x : E}, fderiv 𝕜 (-f) x = -fderiv 𝕜 f x
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_sdiff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → Finset.Ico a b \ Finset.Ioo a b = {a}
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.instTopologicalSpace : (R : Type u_1) → [inst : CommRing R] → [WithIdeal R] → TopologicalSpace R
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at the
third point is zero.  -/
Sbtw.oangle₂₃₁_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₃ p₁ = 0
-- Lean.Elab.Do.InferControlInfo
/-- Infer the `ControlInfo` of `doSeq`.  -/
Lean.Elab.Do.inferControlInfoSeq : Lean.DoSeq → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Lean.Syntax
Lean.Syntax.Range.mk.inj : ∀ {start stop start_1 stop_1 : String.Pos.Raw},
  { start := start, stop := stop } = { start := start_1, stop := stop_1 } → start = start_1 ∧ stop = stop_1
-- Mathlib.Topology.Basic
Filter.lim.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Nonempty X] (f f_1 : Filter X), f = f_1 → f.lim = f_1.lim
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sq' : ∀ (x : ℝ), Real.cos x ^ 2 = 1 - Real.sin x ^ 2
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.coskAdj.reflective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
        [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
              (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] →
          CategoryTheory.Reflective (CategoryTheory.SimplicialObject.Truncated.cosk n)
-- Mathlib.Data.Seq.Basic
/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
statement of the where the sequence is not known to terminate see `length_le_iff'`.  -/
Stream'.Seq.length_le_iff : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ} {h : s.Terminates}, s.length h ≤ n ↔ s.TerminatedAt n
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the forward direction of `contMDiff_iff_contDiff`. -/
ContMDiff.contDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'}, ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f → ContDiff 𝕜 n f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The obvious homotopy between two equal morphisms of short complexes.  -/
CategoryTheory.ShortComplex.Homotopy.ofEq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → {φ₁ φ₂ : S₁ ⟶ S₂} → φ₁ = φ₂ → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂
-- Init.Data.Vector.Lemmas
Vector.unzip_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Array (α × β)} (h : xs.size = n),
  (Vector.mk xs h).unzip = (Vector.mk xs.unzip.1 ⋯, Vector.mk xs.unzip.2 ⋯)
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_append : ∀ {R : Type u_2} [inst : AddZeroClass R] (l₁ l₂ : List R) [inst_1 : DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0]
  [inst_2 : DecidablePred fun x => l₁.getD x 0 ≠ 0] [inst_3 : DecidablePred fun x => l₂.getD x 0 ≠ 0],
  (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.IsBalanced.isPerfectCompl : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : AddCommGroup M} {inst_1 : AddCommGroup N}
  {inst_2 : CommRing R} {inst_3 : Module R M} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsBalanced],
  P.IsPerfectCompl (P.rootSpan R) (P.corootSpan R)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_monomial_of_lt : ∀ {R : Type u_1} [inst : CommSemiring R] {m n : ℕ}, n < m → ∀ (r : R), ((Polynomial.monomial m) r).homogenize n = 0
-- Mathlib.Order.BoundedOrder.Basic
not_lt_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, ¬a < ⊥
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.eq_1 : ∀ (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1)
  (l₁ l₂ : List (Option Lean.LocalDecl)) (h_1 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂)
  (h_2 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive l₁ (none :: l₂))
  (h_3 :
    (d₁ : Lean.LocalDecl) →
      (l₁ : List (Option Lean.LocalDecl)) →
        (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂))
  (h_4 : Unit → motive [] []) (h_5 : (x x_1 : List (Option Lean.LocalDecl)) → motive x x_1),
  (match none :: l₁, l₂ with
    | none :: l₁, l₂ => h_1 l₁ l₂
    | l₁, none :: l₂ => h_2 l₁ l₂
    | some d₁ :: l₁, some d₂ :: l₂ => h_3 d₁ l₁ d₂ l₂
    | [], [] => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_1 l₁ l₂
-- Mathlib.Topology.Sheaves.Stalks
/-- Let `F` and `G` be sheaves valued in a concrete category, whose forgetful functor reflects
isomorphisms, preserves limits and filtered colimits. Then a morphism `f : F ⟶ G` is an
isomorphism if and only if all of its stalk maps are isomorphisms.
 -/
TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G),
  CategoryTheory.IsIso f ↔ ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
-- Init.Prelude
/-- The original (unhygienic) name.  -/
Lean.MacroScopesView.name : Lean.MacroScopesView → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When `S₁.g` and `S₂.g` are zero and we have chosen colimit cokernel coforks `c₁` and `c₂`
for `S₁.f` and `S₂.f` respectively, the action on right homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`φ.τ₂ ≫ c₂.π = c₁.π ≫ f`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hg₁ : S₁.g = 0) →
            (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) →
              (hc₁ : CategoryTheory.Limits.IsColimit c₁) →
                (hg₂ : S₂.g = 0) →
                  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) →
                    (hc₂ : CategoryTheory.Limits.IsColimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f →
                          CategoryTheory.ShortComplex.RightHomologyMapData φ
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
-- Mathlib.Order.RelSeries
SetRel.infiniteDimensional_iff : ∀ {α : Type u_1} (r : SetRel α α), r.InfiniteDimensional ↔ ∀ (n : ℕ), ∃ x, x.length = n
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isTypeAscription : Lean.Syntax → Bool