mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃Functor_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) {X Y : C₃}
  (f : X ⟶ Y) (j : C₂), (((CategoryTheory.Functor.flip₂₃Functor.obj F).obj G).map f).app j = ((F.obj G).obj j).map f
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_bot_eq_bot : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) [inst_7 : T1Space M] [inst_8 : T1Space N], (ClosedSubmodule.mapEquiv f) ⊥ = ⊥
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Symmetric bilinear forms can be lifted to quadratic forms  -/
QuadraticMap.canLift : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Invertible 2],
  CanLift (LinearMap.BilinMap R M R) (QuadraticForm R M) (⇑(QuadraticMap.associatedHom ℕ)) LinearMap.IsSymm
-- Init.Data.List.FinRange
List.getElem_finRange : ∀ {n i : ℕ} (h : i < (List.finRange n).length), (List.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffine.of_isPullback : ∀ {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
  [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffineHom g],
  CategoryTheory.IsPullback fst snd f g → AlgebraicGeometry.IsAffine P
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Inherit `AddCommGroup` structure from `C(X, R) →L[R] E`.  -/
AbstractMeasure.instAddCommGroup : {X : Type u_1} →
  {R : Type u_3} →
    {E : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [inst_4 : CommRing R] →
                [inst_5 : TopologicalSpace R] →
                  [inst_6 : IsTopologicalRing R] → [inst_7 : Module R E] → AddCommGroup (AbstractMeasure X R E)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_tensorProduct : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N],
  (TensorProduct.mapBilinear (RingHom.id R) M N M N).compr₂ (LinearMap.trace R (TensorProduct R M N)) =
    (LinearMap.lsmul R R).compl₁₂ (LinearMap.trace R M) (LinearMap.trace R N)
-- Init.Data.UInt.Lemmas
UInt8.ofInt_mul : ∀ (x y : ℤ), UInt8.ofInt (x * y) = UInt8.ofInt x * UInt8.ofInt y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : MulOneClass α] [inst_5 : MulOneClass β] [inst_6 : MulOneClass γ]
  [inst_7 : MulOneClass δ] (f : γ →*o δ) (g : β →*o γ) (h : α →*o β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.mul : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {w x y z : M},
  ConGen.Rel r w x → ConGen.Rel r y z → ConGen.Rel r (w * y) (x * z)
-- Std.Internal.UV.Timer
/-- This creates a `Timer` in the initial state and doesn't run it yet.
- If `repeating` is `false` this constructs a timer that resolves once after `timeout`
  milliseconds, counting from when it's run.
- If `repeating` is `true` this constructs a timer that resolves after multiples of `timeout`
  milliseconds, counting from when it's run. Note that this includes the 0th multiple right after
  starting the timer. Furthermore a repeating timer will only be freed after `Timer.stop` is called.
 -/
Std.Internal.UV.Timer.mk : UInt64 → Bool → IO Std.Internal.UV.Timer
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.limitAddCommMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  AddCommMonCat.limitAddCommMonoid F =
    {
      add :=
        AddCommMonCat.limitAddCommMonoid._aux_1 F
          (AddMonCat.sectionsAddSubmonoid (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).toAddCommMonoid,
      add_assoc := ⋯,
      zero :=
        AddCommMonCat.limitAddCommMonoid._aux_4 F
          (AddMonCat.sectionsAddSubmonoid (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).toAddCommMonoid,
      zero_add := ⋯, add_zero := ⋯,
      nsmul :=
        AddCommMonCat.limitAddCommMonoid._aux_8 F
          (AddMonCat.sectionsAddSubmonoid (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).toAddCommMonoid,
      nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.Data.Num.Bitwise
PosNum.lor_eq_or : ∀ (p q : PosNum), p.lor q = p ||| q
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsInitial.uniqueUpToIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I I' : C} (hI : CategoryTheory.Limits.IsInitial I)
  (hI' : CategoryTheory.Limits.IsInitial I'), (hI.uniqueUpToIso hI').hom = hI.to I'
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_lt_one_or_eq_one : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), A.valuation ↑a < 1 ∨ A.valuation ↑a = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l l_1 : List ((a : α) × β a))
  (e_l : l = l_1) (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValueCast a l h = Std.Internal.List.getValueCast a l_1 ⋯
-- Mathlib.Data.Finset.Card
/-- A `Finset` of a subsingleton type has cardinality at most one.  -/
Finset.card_le_one_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (s : Finset α), s.card ≤ 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  Std.ExtDHashMap.Const.insertManyIfNewUnit m (k :: l) =
    Std.ExtDHashMap.Const.insertManyIfNewUnit (m.insertIfNew k ()) l
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.foldlMUnsafe.fold : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (β → α → m β) → Array α → USize → USize → β → m β
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflRight_one : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Path.delayReflRight 1 γ = γ
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An image map is a morphism `image f → image g` fitting into a commutative square and satisfying
the obvious commutativity conditions.  -/
CategoryTheory.Limits.ImageMap.map_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (self : CategoryTheory.Limits.ImageMap sq) {Z : C} (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.map
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.instCoeFunForallProd : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} → [inst_2 : TopologicalSpace Z] → CoeFun (Bundle.Trivialization F proj) fun x => Z → B × F
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.run_attachLift : ∀ {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type w} {x : m α},
  (Std.Iterators.PostconditionT.attachLift x).run = x
-- Init.Data.Rat.Lemmas
Rat.zpow_sub_one : ∀ {q : ℚ}, q ≠ 0 → ∀ (m : ℤ), q ^ (m - 1) = q ^ m * q⁻¹
-- Lean.Parser.Command
Lean.Parser.Command.declModifiers.formatter : Bool → Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.iff_symm_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The action on morphisms of the obvious functor
`WidePullbackShape_op : WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ`  -/
CategoryTheory.Limits.widePullbackShapeOpMap : (J : Type w) → (X Y : CategoryTheory.Limits.WidePullbackShape J) → (X ⟶ Y) → (Opposite.op X ⟶ Opposite.op Y)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he = t.maxKey?.get ⋯
-- Batteries.Data.AssocList
Batteries.AssocList.length_mapKey : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {β : Type u_3} {l : Batteries.AssocList α β},
  (Batteries.AssocList.mapKey f l).length = l.length
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_const_left : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => C * f x) l Filter.atBot
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
minimalPrimes.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R], minimalPrimes R = {p | IsMinimalPrime p}
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adj : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a b : α} {e : Sym2 α},
  a ≠ b → ¬G.Adj a b → SimpleGraph.incMatrix R G a e * SimpleGraph.incMatrix R G b e = 0
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.restrictDom_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (l : α →₀ M) [inst_3 : DecidablePred fun x => x ∈ s],
  ↑((Finsupp.restrictDom M R s) l) = Finsupp.filter (fun x => x ∈ s) l
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), dist a b = ‖a⁻¹ * b‖
-- Mathlib.MeasureTheory.Measure.Regular
/-- Given `r` larger than the measure of a set `A`, there exists an open superset of `A` with
measure less than `r`.  -/
Set.exists_isOpen_lt_of_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.OuterRegular]
  (A : Set α) (r : ENNReal), μ A < r → ∃ U ⊇ A, IsOpen U ∧ μ U < r
-- Mathlib.Data.W.Constructions
WType.ofNat.eq_1 : WType.ofNat Nat.zero = WType.mk WType.Natα.zero Empty.elim
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_one : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : Group Gᵣ] [IsRightUniformGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.2 / x.1) (nhds 1)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.single_boxes_val : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).boxes.val = {J}
-- Mathlib.Algebra.BigOperators.Fin
/-- A product of a function `f : Fin 0 → M` is `1` because `Fin 0` is empty  -/
Fin.prod_univ_zero : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 0 → M), ∏ i, f i = 1
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.id_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (d : CategoryTheory.Factorisation f),
  (CategoryTheory.CategoryStruct.id d).h = CategoryTheory.CategoryStruct.id d.mid
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.toFun = ⇑f
-- ProofWidgets.Component.RefreshComponent
/-- Will be cancelled whenever the widget is rendered with a new `state`, or unmounted,
or when the whole infoview is closed.  -/
ProofWidgets.RefreshComponent.Props.cancelTk : ProofWidgets.RefreshComponent.Props → Lean.Server.WithRpcRef IO.CancelToken
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_empty : ∀ {α : Type u_3} [inst : AddMonoid α] (h : {x | x ∈ 0}.Pairwise AddCommute), Multiset.noncommSum 0 h = 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddGroupOfIsTopologicalAddGroup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → AddGroup C(α, β)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.not_ex_isAtomic : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)), ¬φ.ex.IsAtomic
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.preimage_closure : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), e.source ∩ ↑e ⁻¹' closure s = e.source ∩ closure (↑e ⁻¹' s)
-- Mathlib.Data.Sum.Interval
Sum.Lex.Iic_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderBot α] [inst_4 : LocallyFiniteOrderBot β] (a : α),
  Finset.Iic (Sum.inlₗ a) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Iic a)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.symplComp.eq_1 : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H),
  S.symplComp = S.mulIᗮ
-- Batteries.Data.Fin.Lemmas
Fin.prod.eq_1 : ∀ {α : Type u_1} {n : ℕ} [inst : One α] [inst_1 : Mul α] (x : Fin n → α),
  Fin.prod x = Fin.foldr n (fun x1 x2 => x x1 * x2) 1
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- If `fn` is `UnifIntegrable`, then the family of a.e. limits of sequences of `fn` is
`UnifIntegrable`.  -/
MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {κ : Type u_4} (u : Filter κ) [u.NeBot] [u.IsCountablyGenerated]
  {fn : ι → α → β},
  MeasureTheory.UnifIntegrable fn p μ →
    (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (fn i) μ) → MeasureTheory.UnifIntegrable (fun f => ↑f) p μ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c),
  (E.sigmaOfIsColimit hc).I₀ = PUnit.{w + 1}
-- Mathlib.Order.KrullDimension
/-- The Krull dimension is the supremum of the elements' coheights.

This version of the lemma assumes that `α` is nonempty. In this case, the coercion from `ℕ∞` to
`WithBot ℕ∞` is on the outside of the right-hand side, which is usually more convenient.

If `α` were empty, then `krullDim α = ⊥`. See `krullDim_eq_iSup_coheight` for the more general
version, with the coercion under the supremum.
 -/
Order.krullDim_eq_iSup_coheight_of_nonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim α = ↑(⨆ a, Order.coheight a)
-- Mathlib.Analysis.Normed.Group.Hom
/-- The operator norm of a seminormed group homomorphism is the inf of all its bounds.  -/
NormedAddGroupHom.opNorm : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → ℝ
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_subtype_fun : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α},
  BddAbove (Set.range fun i => f ↑i) → sSup ∅ ≤ ⨆ i, f ↑i → ⨆ i, f ↑i = ⨆ t ∈ s, f t
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- View a term of `FundamentalGroupoid X` as a term of `X`.  -/
FundamentalGroupoid.as : {X : Type u_3} → FundamentalGroupoid X → X
-- Lean.Environment
/-- Modify the state of the given extension in the given environment by applying the given function.  -/
Lean.PersistentEnvExtension.modifyState : {α β σ : Type} →
  (ext : Lean.PersistentEnvExtension α β σ) →
    Lean.Environment →
      (σ → σ) →
        optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode →
          optParam Lean.Name Lean.Name.anonymous → Lean.Environment
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.δ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (n₀ n₁ : ℤ)
  (h : n₀ + 1 = n₁), DerivedCategory.HomologySequence.δ T n₀ n₁ h = DerivedCategory.HomologySequence.δ T n₀ n₁ h
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.add_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β]
  (x y : WithLp p (α × β)), (x + y).snd = x.snd + y.snd
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.size_toArray : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.toArray.size = r.size
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_attach_biUnion : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq A] {α : Type u_2} {s : Finset α} (f : ↥s → Finset A),
  Algebra.adjoin R ↑(s.attach.biUnion f) = ⨆ x, Algebra.adjoin R ↑(f x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
ContinuousLinearMap.isIdempotentElem_toLinearMap_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {f : M →L[R] M}, IsIdempotentElem ↑f ↔ IsIdempotentElem f
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- `cyclotomic n ℚ` is the minimal polynomial of a primitive `n`-th root of unity `μ`.  -/
Polynomial.cyclotomic_eq_minpoly_rat : ∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
  IsPrimitiveRoot μ n → 0 < n → ∀ [inst_1 : CharZero K], Polynomial.cyclotomic n ℚ = minpoly ℚ μ
-- Mathlib.Order.Filter.Pointwise
Filter.inv_le_inv_iff : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f g : Filter α}, f⁻¹ ≤ g⁻¹ ↔ f ≤ g
-- Batteries.Data.Nat.Bisect
Nat.avg_lt_left : ∀ {b a : ℕ}, b < a → a.avg b < a
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_self : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), Set.Icc a a = {a}
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The disjoint union of antidiagonals `Σ (n : A), antidiagonal n` is equivalent to the
product `A × A`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`.  -/
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd : {A : Type u_1} →
  [inst : AddMonoid A] →
    [inst_1 : Finset.HasAntidiagonal A] → (n : A) × ↥(Finset.HasAntidiagonal.antidiagonal n) ≃ A × A
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.asterisk : Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_inv_sq_add_sq : ∀ {a b c : ℝ}, c ≠ 0 → ∫ (x : ℝ) in a..b, (c ^ 2 + x ^ 2)⁻¹ = c⁻¹ * (Real.arctan (b / c) - Real.arctan (a / c))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.nonsingularLift_addMap : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : WeierstrassCurve.Projective.PointClass F},
  W.NonsingularLift P → W.NonsingularLift Q → W.NonsingularLift (W.addMap P Q)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If `F ⋙ G` preserves finite coproducts and `G` reflects finite coproducts, then `F` preserves
finite coproducts.
 -/
CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves : ∀ {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.Limits.PreservesFiniteCoproducts (F.comp G)]
  [CategoryTheory.Limits.ReflectsFiniteCoproducts G], CategoryTheory.Limits.PreservesFiniteCoproducts F
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (Set.Ioo a b)⁻¹ = Set.Ioo b⁻¹ a⁻¹
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeans.mk : Lean.Lsp.WaitForILeans
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X X_1 : C),
  ((CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost F).inv.app X).app X_1 =
    CategoryTheory.Functor.OplaxMonoidal.δ F X X_1
-- Mathlib.Data.Real.ENatENNReal
/-- Coercion `ℕ∞ → ℝ≥0∞` as an `OrderEmbedding`.  -/
ENat.toENNRealOrderEmbedding : ℕ∞ ↪o ENNReal
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeries.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | x => h_3 x) =
    h_2 ()
-- Mathlib.RingTheory.Localization.Basic
AlgEquiv.extendScalarsOfIsLocalization_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  (S : Type u_4) [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (M : Submonoid R) [inst_5 : IsLocalization M S]
  [inst_6 : Algebra R A] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] [inst_9 : Algebra R B]
  [inst_10 : Algebra S B] [inst_11 : IsScalarTower R S B] (f : A ≃ₐ[R] B) (a : A),
  (AlgEquiv.extendScalarsOfIsLocalization S M f) a = (↑↑(AlgHom.extendScalarsOfIsLocalization S M ↑f).toRingHom).toFun a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.map_lift_pullbackComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {W : C} {h : W ⟶ X} {k : W ⟶ Y} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
  {Z_1 : D} (h_1 : CategoryTheory.Limits.pullback (G.map f) (G.map g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h k w))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (G.map h) (G.map k) ⋯) h_1
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- Preimages of compact closed sets are compact under a cocompact continuous map.  -/
CocompactMap.isCompact_preimage_of_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : CocompactMap α β)
  ⦃s : Set β⦄, IsCompact s → IsClosed s → IsCompact (⇑f ⁻¹' s)
-- Mathlib.Analysis.InnerProductSpace.Continuous
_private.Mathlib.Analysis.InnerProductSpace.Continuous.0.«term⟪_,_⟫» : Lean.ParserDescr