mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁δ_naturality : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (a' b' c' : EInt) (hab' : a' ≤ b') (hbc' : b' ≤ c')
  (φ :
    CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hab) (CategoryTheory.homOfLE hbc) ⟶
      CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hab') (CategoryTheory.homOfLE hbc')),
  CategoryTheory.CategoryStruct.comp (t.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 1) (φ.app 2) ⋯))
      (t.ω₁δ a' b' c' hab' hbc') =
    CategoryTheory.CategoryStruct.comp (t.ω₁δ a b c hab hbc)
      (CategoryTheory.Functor.whiskerRight (t.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯))
        (CategoryTheory.shiftFunctor C 1))
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_rhs_prefix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
/-- The units of a complete normed ring form a Lie group.  -/
Units.instLieGroupModelWithCornersSelf : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {n : WithTop ℕ∞} {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAlgebra 𝕜 R], LieGroup (modelWithCornersSelf 𝕜 R) n Rˣ
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mk_coordChange : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (v : F), (b, (a.coordChange he he' b) v) = ↑e' ⟨b, e.symm b v⟩
-- Mathlib.RingTheory.Smooth.NoetherianDescent
Algebra.Smooth.exists_subalgebra_finiteType : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [Algebra.Smooth A B],
  ∃ A₀ B₀ x x_1, Algebra.FiniteType R ↥A₀ ∧ Algebra.Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {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_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : ⋯ = j), ⋯ = ⋯
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- A measurable set from the product sigma-algebra only depends on countably many coordinates.  -/
MeasureTheory.MeasurableSet.eq_preimage_restrict_countable : ∀ {ι : Type u_2} {α : ι → Type u_1} [inst : (i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)},
  MeasurableSet s → ∃ I t, I.Countable ∧ s = I.domRestrict ⁻¹' t
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommRing : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [CommRing Y] → CommRing (LocallyConstant X Y)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_ext'_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C}
  {z w : (F ⨯ G).obj a},
  z = w ↔
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) z =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) w ∧
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) z =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) w
-- Mathlib.Data.Sum.Order
Sum.instPartialOrder : {α : Type u_1} → {β : Type u_2} → [PartialOrder α] → [PartialOrder β] → PartialOrder (α ⊕ β)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y)
  [inst_2 : AlgebraicGeometry.IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂)
  {Z : AlgebraicGeometry.Scheme} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H) h) =
    CategoryTheory.CategoryStruct.comp f₁ h
-- Mathlib.Topology.Bases
/-- In a disjoint union space `Σ i, E i`, one can form a topological basis by taking the union of
topological bases on each of the parts of the space.  -/
TopologicalSpace.IsTopologicalBasis.sigma : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (E i)] {s : (i : ι) → Set (Set (E i))},
  (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (s i)) →
    TopologicalSpace.IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.toMatrixOrthonormal_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : Type u_6} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : FiniteDimensional 𝕜 E]
  (v₁ : OrthonormalBasis n 𝕜 E) (a : Matrix n n 𝕜),
  (LinearMap.toMatrixOrthonormal v₁).symm a = (LinearMap.toMatrix v₁.toBasis v₁.toBasis).invFun a
-- Mathlib.Algebra.Group.Action.Sum
Sum.instAddAction : {M : Type u_1} →
  {α : Type u_3} → {β : Type u_4} → {m : AddMonoid M} → [AddAction M α] → [AddAction M β] → AddAction M (α ⊕ β)
-- Mathlib.Topology.Algebra.Group.Basic
continuousDiv_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Div H] [DiscreteTopology H], ContinuousDiv H
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P ≈ Q
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
/-- The L2 norm of the cross product of two real vectors (of type `EuclideanSpace ℝ (Fin 3)`)
equals the product of their individual norms times the sine of the angle between them.  -/
InnerProductGeometry.norm_ofLp_crossProduct : ∀ (a b : EuclideanSpace ℝ (Fin 3)),
  ‖WithLp.toLp 2 ((crossProduct a.ofLp) b.ofLp)‖ = ‖a‖ * ‖b‖ * Real.sin (InnerProductGeometry.angle a b)
-- Mathlib.Data.List.OffDiag
List.offDiag_nil : ∀ {α : Type u_1}, [].offDiag = []
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- In extended charts at `p`, `Sum.swap` looks like the identity near `p`.  -/
writtenInExtChartAt_sumSwap_eventuallyEq_id : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'},
  writtenInExtChartAt I I p Sum.swap =ᶠ[nhdsWithin (↑I (↑(chartAt H p) p)) (Set.range ↑I)] id
-- Mathlib.Algebra.WithConv
WithConv.instMulAction.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : MulAction R A],
  WithConv.instMulAction =
    { smul := fun a a_1 => (WithConv.equiv A).2 (a • (WithConv.equiv A).toFun a_1), mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_zero_right : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ),
  PerfectClosure.mk K p (n, 0) = 0
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.Shrink.inflate.eq_1 : ∀ {α : Type u_1} (x : Std.Shrink α), x.inflate = cast ⋯ x
-- Mathlib.Data.Real.Basic
Real.cauchy_add : ∀ (a b : ℝ), (a + b).cauchy = a.cauchy + b.cauchy
-- Mathlib.Data.Real.Basic
Real.instOne : One ℝ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in the right argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B B' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (g : B ⟶ B')
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B')],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g))
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B'))
-- Mathlib.Control.Traversable.Lemmas
/-- The natural applicative transformation from the identity functor
to `F`, defined by `pure : Π {α}, α → F α`.  -/
Traversable.PureTransformation : (F : Type u → Type u) → [inst : Applicative F] → [LawfulApplicative F] → ApplicativeTransformation Id F
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearMap_mapInclIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E)
  (F' : Submodule 𝕜 F), (TensorProduct.mapInclIsometry E' F').toLinearMap = TensorProduct.mapIncl E' F'
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.closed.sizeOf_spec : sizeOf Lean.Meta.TacticResultCNM.closed = 1
-- Mathlib.Order.CompleteLattice.Basic
biInf_gt_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : LT ι] [NoMinOrder ι] {f : ι → α},
  ⨅ i, ⨅ j, ⨅ (_ : j > i), f j = ⨅ i, f i
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.instSubsingletonOfWellFoundedLT : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J),
  Subsingleton (d.Extension val₀ j)
-- Mathlib.Algebra.Star.StarProjection
isStarProjection_one_sub_iff : ∀ {R : Type u_1} {p : R} [inst : NonAssocRing R] [inst_1 : StarRing R], IsStarProjection (1 - p) ↔ IsStarProjection p
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnitImpl_rel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Dial.tensorUnitImpl.rel = ⊤
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- A subspace is complement to its orthogonal complement with respect to some
reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate.  -/
LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → (B.restrict W).Nondegenerate → IsCompl W (B.orthogonal W)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, t.WF → (t.modify k f).maxKey? = t.maxKey?
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') [G.IsEquivalence] (f : L' ⟶ L.comp G) [CategoryTheory.IsIso f]
  (F : CategoryTheory.Functor C H), (CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).IsEquivalence
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiSeparated (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.commute_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ), Commute φ (PowerSeries.X ^ n)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.quot_map_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool))
  (H : Relator.LiftFun FreeGroup.Red.Step FreeGroup.Red.Step f f), Quot.map f H (FreeGroup.mk L) = FreeGroup.mk (f L)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mapsto_domChart_source_codChart_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LocalPresentationAt I J n f x P), Set.MapsTo f h.domChart.source h.codChart.source
-- Mathlib.Order.Grade
Flag.coe_wcovBy_coe : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Flag α} {a b : ↥s}, ↑a ⩿ ↑b ↔ a ⩿ b
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.seq_destruct_nil : ∀ {α : Type u}, Stream'.Seq.destruct Stream'.WSeq.nil = none
-- Init.WF
Prod.Lex.instDecidableRelOfDecidableEq : {α : Type u} →
  {β : Type v} →
    [αeqDec : DecidableEq α] →
      {r : α → α → Prop} →
        [rDec : DecidableRel r] → {s : β → β → Prop} → [sDec : DecidableRel s] → DecidableRel (Prod.Lex r s)
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.eventually_meas_ne_zero : ∀ {G : Type u_4} {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} {l : Filter ι} {F : ι → Set X},
  IsAddFoelner G μ l F → ∀ᶠ (i : ι) in l, μ (F i) ≠ 0
-- Mathlib.Algebra.Order.AddTorsor
VAdd.vadd_lt_vadd_of_lt_of_le : ∀ {G : Type u_1} {P : Type u_2} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P]
  {a b : G} {c d : P}, a < b → c ≤ d → a +ᵥ c < b +ᵥ d
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The source of the arrows defining the relation.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → {I₁ I₂ : S.Arrow} → I₁.Relation I₂ → C
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_5.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : List Lean.Elab.InfoTree) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_6 t (Lean.Elab.InfoTree.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mk.injEq : ∀ {α : Type u_2} (toFilter : Filter α) (neBot' : toFilter.NeBot)
  (le_of_le : ∀ (g : Filter α), g.NeBot → g ≤ toFilter → toFilter ≤ g) (toFilter_1 : Filter α)
  (neBot'_1 : toFilter_1.NeBot) (le_of_le_1 : ∀ (g : Filter α), g.NeBot → g ≤ toFilter_1 → toFilter_1 ≤ g),
  ({ toFilter := toFilter, neBot' := neBot', le_of_le := le_of_le } =
      { toFilter := toFilter_1, neBot' := neBot'_1, le_of_le := le_of_le_1 }) =
    (toFilter = toFilter_1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- The linear map between the colimit modules induced by a morphism of modules.  -/
PresheafOfModules.ModuleColimit.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.IsCofiltered C] →
        [inst_3 : CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              (hcR : CategoryTheory.Limits.IsColimit cR) →
                {M : PresheafOfModules R} →
                  {cM : CategoryTheory.Limits.Cocone M.presheaf} →
                    (hcM : CategoryTheory.Limits.IsColimit cM) →
                      {M' : PresheafOfModules R} →
                        {cM' : CategoryTheory.Limits.Cocone M'.presheaf} →
                          (hcM' : CategoryTheory.Limits.IsColimit cM') →
                            (M ⟶ M') →
                              PresheafOfModules.ModuleColimit hcR hcM →ₗ[↑cR.pt]
                                PresheafOfModules.ModuleColimit hcR hcM'
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_sub_one_right_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a < b → insert b (Finset.Ioc a (b - 1)) = Finset.Ioc a b
-- Init.Data.SInt.Lemmas
Int64.zero_mod : ∀ {a : Int64}, 0 % a = 0
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If a normed space is (topologically) non-trivial, then the norm of the identity equals `1`.  -/
ContinuousLinearMap.nnnorm_id : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [NontrivialTopology E], ‖ContinuousLinearMap.id 𝕜 E‖₊ = 1
-- Mathlib.Algebra.Quaternion
/-- Square of the norm.  -/
Quaternion.normSq : {R : Type u_3} → [inst : CommRing R] → Quaternion R →*₀ R
-- Mathlib.Data.Complex.BigOperators
Complex.ofReal_comp_balance : ∀ {ι : Type u_2} [inst : Fintype ι] (f : ι → ℝ),
  Complex.ofReal ∘ Fintype.balance f = Fintype.balance (Complex.ofReal ∘ f)
-- Mathlib.Order.Completion
/-- The left set of a Dedekind cut. This is an alias for `Concept.extent`.  -/
DedekindCut.left : {α : Type u_1} → [inst : Preorder α] → DedekindCut α → Set α
-- Mathlib.Topology.Category.TopCat.Monoidal
/-- The inclusion `X ⟶ X ⊗ I` given by `1 : I` for `X : TopCat`.  -/
TopCat.ι₁ : {X : TopCat} → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.expr : Lean.Expr → Lean.Elab.Tactic.ResolveSimpIdResult
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_disjUnion : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} (h : Disjoint s₁ s₂),
  ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeGrpCat.eq_1 : CommGrpCat.instCoeGrpCat = { coe := (CategoryTheory.forget₂ CommGrpCat GrpCat).obj }
-- Mathlib.Order.Defs.Unbundled
/-- `IsEquiv X r` means that the binary relation `r` on `X` is an equivalence relation, that
is, `IsPreorder X r` and `Std.Symm r`.  -/
IsEquiv : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
_private.Mathlib.Analysis.SpecialFunctions.Pow.Continuity.0.ENNReal.continuousAt_rpow_const_of_pos : ∀ {x : ENNReal} {y : ℝ}, 0 < y → ContinuousAt (fun a => a ^ y) x
-- Std.Http.Protocol.H1.Reader
/-- Transitions to the state for reading chunked transfer encoding.
 -/
Std.Http.Protocol.H1.Reader.startChunkedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Order.Cover
Set.Ico_eq_singleton_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, Set.Ico a b = {c} ↔ a = c ∧ a ⋖ b
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.mk.sizeOf_spec : ∀ (startPos stopPos : String.Pos.Raw) (token : Lean.Syntax),
  sizeOf { startPos := startPos, stopPos := stopPos, token := token } =
    1 + sizeOf startPos + sizeOf stopPos + sizeOf token
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.instDecidableEqDiscrete : {α : Type u₁} → [DecidableEq α] → DecidableEq (CategoryTheory.Discrete α)