mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.mk.injEq : ∀ (objects : Lean.Server.RpcObjectStore) (expireTime : ℕ) (objects_1 : Lean.Server.RpcObjectStore) (expireTime_1 : ℕ),
  ({ objects := objects, expireTime := expireTime } = { objects := objects_1, expireTime := expireTime_1 }) =
    (objects = objects_1 ∧ expireTime = expireTime_1)
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_mapRange : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0}
  {g : α →₀ M}, (Finsupp.mapRange f hf g).support ⊆ g.support
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.false : ∀ {α : Sort u} [self : IsEmpty α] (a : α), False
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.Rel.congr_simp : ∀ {α β : Type w} (m : Type w → Type w') [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Productive α m] (a a_1 : Std.IterM m β),
  a = a_1 →
    ∀ (a_2 a_3 : Std.IterM m β),
      a_2 = a_3 → Std.Iterators.Types.Take.Rel m a a_2 = Std.Iterators.Types.Take.Rel m a_1 a_3
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.Context.mk.injEq : ∀ (userName : Lean.Name) (explicitPatternVars : Array Lean.FVarId) (userName_1 : Lean.Name)
  (explicitPatternVars_1 : Array Lean.FVarId),
  ({ userName := userName, explicitPatternVars := explicitPatternVars } =
      { userName := userName_1, explicitPatternVars := explicitPatternVars_1 }) =
    (userName = userName_1 ∧ explicitPatternVars = explicitPatternVars_1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roo_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toArray[i]! ≠ 0 ↔ i < (n - (m + 1)).toNat ∧ m + ↑i ≠ -1
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileM`.
When `it.dropWhileM P` has stopped dropping elements, its new state cannot be created
directly with `IterM.dropWhileM` but only with `Intermediate.dropWhileM`.

`Intermediate.dropWhileM` is meant to be used only for internally or for verification purposes.
 -/
Std.IterM.Intermediate.dropWhileM : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] → [inst : MonadAttach m] → (P : β → m (ULift.{w, 0} Bool)) → Bool → Std.IterM m β → Std.IterM m β
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 5`.  -/
CategoryTheory.ComposableArrows.isoMk₅ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 5} →
      (app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝) →
        (app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝) →
          (app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝) →
            (app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝) →
              (app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝) →
                (app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝) →
                  CategoryTheory.CategoryStruct.comp
                        (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝) app₁.hom =
                      CategoryTheory.CategoryStruct.comp app₀.hom
                        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝) →
                    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂.hom =
                        CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_451✝) →
                      CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃.hom =
                          CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_452✝) →
                        CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄.hom =
                            CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_453✝) →
                          CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅.hom =
                              CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_453✝ _proof_454✝) →
                            (f ≅ g)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.pow_lt_one_of_lt`. -/
pow_lt_one' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M} {n : ℕ}, a < 1 → n ≠ 0 → a ^ n < 1
-- Mathlib.Logic.Basic
/-- **Alias** of the forward direction of `and_rotate`. -/
And.rotate : ∀ {a b c : Prop}, a ∧ b ∧ c → b ∧ c ∧ a
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Multiplicative (G × H)` is equivalent to `Multiplicative G × Multiplicative H`.  -/
MulEquiv.prodMultiplicative : (G : Type u_2) →
  (H : Type u_3) → [inst : Add G] → [inst_1 : Add H] → Multiplicative (G × H) ≃* Multiplicative G × Multiplicative H
-- Mathlib.Analysis.Normed.Algebra.Spectrum
SubalgebraClass.val.eq_1 : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [inst_4 : SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S),
  SubalgebraClass.val s =
    { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.ofLeftInverse'_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : M), (MulEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a
-- Init.Data.Order.Lemmas
Std.min_le_left : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderInf α] {a b : α},
  a ⊓ b ≤ a
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Computation of the `g'` field of `extend.rightHomologyData`.  -/
HomologicalComplex.extend.rightHomologyData_g' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).RightHomologyData) (hk'' : e.f k = k'),
  (HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).g' =
    CategoryTheory.CategoryStruct.comp h.g' (K.extendXIso e hk'').inv
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonCreateFile.toJson : Lean.Lsp.CreateFile → Lean.Json
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.homMk₀.match_1.eq_1 : ∀ (motive : Fin (0 + 1) → Sort u_1) (isLt : 0 < 0 + 1) (h_1 : (isLt : 0 < 0 + 1) → motive ⟨0, isLt⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt) =
    h_1 isLt
-- Mathlib.GroupTheory.Coset.Defs
/-- The canonical map from a group `α` to the quotient `α ⧸ s`.  -/
QuotientGroup.mk : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → α → α ⧸ s
-- Lean.Server.CodeActions.Attr
/-- Insert a command code action entry into the `CommandCodeActions` structure.  -/
Lean.CodeAction.CommandCodeActions.insert : Lean.CodeAction.CommandCodeActions →
  Array Lean.Name → Lean.CodeAction.CommandCodeAction → Lean.CodeAction.CommandCodeActions
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_const : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (a : 𝕜'), (logDeriv fun x => a) = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_apply : ∀ {k n : ℕ}, (ArithmeticFunction.sigma k) n = ∑ d ∈ n.divisors, d ^ k
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- Projective general linear group $PGL(n, R)$
defined as the quotient of the general linear group by its center.  -/
Matrix.ProjGenLinGroup : (n : Type u_1) → [Fintype n] → [DecidableEq n] → (R : Type u_2) → [CommRing R] → Type (max (max u_1 u_2) u_2 u_1)
-- Mathlib.Order.Fin.Tuple
Fin.preimage_insertNth_Icc_of_notMem : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i}
  {q₁ q₂ : (j : Fin (n + 1)) → α j}, x ∉ Set.Icc (q₁ i) (q₂ i) → i.insertNth x ⁻¹' Set.Icc q₁ q₂ = ∅
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.symm_ridIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), (TensorProduct.ridIsometry 𝕜 E).symm x = x ⊗ₜ[𝕜] 1
-- Init.Data.Order.Ord
Std.OrientedCmp.isGE_of_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp b a).isLE = true → (cmp a b).isGE = true
-- Mathlib.Analysis.Normed.Group.Hom
/-- A `NormedAddGroupHom` is bounded.  -/
NormedAddGroupHom.bound' : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  (self : NormedAddGroupHom V W), ∃ C, ∀ (v : V), ‖self.toFun v‖ ≤ C * ‖v‖
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.mk : {R : Type u_1} → [inst : CommSemiring R] → (asIdeal : Ideal R) → asIdeal.IsMaximal → MaximalSpectrum R
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char_zero_eq_one : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2},
  BoundedContinuousFunction.char he hL 0 = 1
-- Mathlib.Algebra.Module.Defs
Module.ext_iff : ∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} {x y : Module R M},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_add_sum_comm : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (f g h i : ι → M),
  ∑ a ∈ s, (f a + g a) + ∑ a ∈ s, (h a + i a) = ∑ a ∈ s, (f a + h a) + ∑ a ∈ s, (g a + i a)
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_zero : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)], WittVector.ghostFun✝ 0 = 0
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.quotient_finite_of_isOpen : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G]
  (U : Subgroup G), IsOpen ↑U → Finite (G ⧸ U)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base.eq_1 : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw}
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos),
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ h = s.pos (stackPos.unoffsetBy needlePos) ⋯
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Remove the last element from an injective (n + 1)-tuple.  -/
Fin.Embedding.init : {α : Type u_1} → {n : ℕ} → (Fin (n + 1) ↪ α) → Fin n ↪ α
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.equiv_symm_apply_ofLp : ∀ (p : ENNReal) (V : Type u_4) (ofLp : V), ((WithLp.equiv p V).symm ofLp).ofLp = ofLp
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInf_ne_top : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ENNReal → α), ⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) '' Set.Ici b = Set.Ici (b - a)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The lineality space of a cone lies in every face.  -/
PointedCone.IsFaceOf.lineal_le : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M}, F.IsFaceOf C → ↑C.lineal ≤ F
-- Mathlib.GroupTheory.Order.Min
AddMonoid.le_minOrder : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ∞},
  n ≤ AddMonoid.minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 0 → IsOfFinAddOrder a → n ≤ ↑(addOrderOf a)
-- Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
ProbabilityTheory.tendsto_zero_of_tendsto_mul_atTop : ∀ {p : ℕ → ℝ} {r : ℝ}, Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r) → Filter.Tendsto p Filter.atTop (nhds 0)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The canonical morphism `K ⟶ K.truncGE e` when `e` is an embedding of complex
shapes which satisfy `e.IsTruncGE`.  -/
HomologicalComplex.πTruncGE : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] → K ⟶ K.truncGE e
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.charRole : Option Lean.FuzzyMatching.CharType →
  Lean.FuzzyMatching.CharType → Option Lean.FuzzyMatching.CharType → Lean.FuzzyMatching.CharRole
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Helper function for constructing morphisms between coequalizer cotridents.
 -/
CategoryTheory.Limits.Cotrident.mkHom : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {s t : CategoryTheory.Limits.Cotrident f} →
              (k : s.pt ⟶ t.pt) →
                autoParam (CategoryTheory.CategoryStruct.comp s.π k = t.π)
                    CategoryTheory.Limits.Cotrident.mkHom._auto_1 →
                  (s ⟶ t)
-- Init.Grind.Ring.Basic
/-- Multiplication is commutative.  -/
Lean.Grind.CommRing.mul_comm : ∀ {α : Type u} [self : Lean.Grind.CommRing α] (a b : α), a * b = b * a
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.biUnion : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι},
  s.Countable → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.one_sub_inv : ∀ (p q : ENNReal) [p.HolderConjugate q], 1 - p⁻¹ = q⁻¹
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.partialOrder : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelMonoid α] → {s : Submonoid α} → PartialOrder (Localization s)
-- Init.While
Lean.Loop.noConfusionType : Sort v✝ → Lean.Loop → Lean.Loop → Sort v✝
-- Mathlib.Data.List.TakeDrop
List.span.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (a a_1 : List α),
  List.span.loop p a a_1 =
    match a, a_1 with
    | [], acc => (acc.reverse, [])
    | a :: as, acc =>
      match p a with
      | true => List.span.loop p as (a :: acc)
      | false => (acc.reverse, a :: as)
-- Mathlib.Analysis.Fourier.Convolution
SchwartzMap.convolution.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace ℂ F₁]
  [inst_8 : NormedSpace 𝕜 F₁] [inst_9 : SMulCommClass ℂ 𝕜 F₁] [inst_10 : NormedAddCommGroup F₂]
  [inst_11 : NormedSpace ℂ F₂] [inst_12 : NormedSpace 𝕜 F₂] [inst_13 : SMulCommClass ℂ 𝕜 F₂]
  [inst_14 : NormedAddCommGroup F₃] [inst_15 : NormedSpace ℂ F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : SMulCommClass ℂ 𝕜 F₃] (B B_1 : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
  B = B_1 → SchwartzMap.convolution B = SchwartzMap.convolution B_1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ofWithBot.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes boxes_1 : Finset (WithBot (BoxIntegral.Box ι)))
  (e_boxes : boxes = boxes_1) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint),
  BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint = BoxIntegral.Prepartition.ofWithBot boxes_1 ⋯ ⋯
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.monic_expand_iff : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ} {f : Polynomial R}, 0 < p → (((Polynomial.expand R p) f).Monic ↔ f.Monic)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hasLimit_of_hasLimit_forget₂ : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)}
  [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))],
  CategoryTheory.Limits.HasLimit F
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- The derivative of a normal function `f` is the sequence of fixed points of `f`.

This is defined as `Ordinal.derivFamily` applied to a trivial family consisting only of `f`.  -/
Ordinal.deriv : (Ordinal.{u_1} → Ordinal.{u_1}) → Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_doubleDualEquiv_symm_apply : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α] (a : AddChar (AddChar α ℂ) ℂ),
  AddChar.doubleDualEmb (AddChar.doubleDualEquiv.symm a) = a
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.applyFVarSubst : Lean.Meta.FVarSubst → Lean.Meta.Match.Example → Lean.Meta.Match.Example
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inter_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (a : E.I₀ × F.1),
  (E.inter F).X a =
    CategoryTheory.Limits.pullback (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm a).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm a).snd)
-- Mathlib.Logic.Lemmas
/-- **Alias** of the reverse direction of `heq_iff_eq`. -/
Eq.heq : ∀ {α : Sort u_1} {a b : α}, a = b → a ≍ b
-- Mathlib.Algebra.Group.Basic
sub_sub_sub_eq : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a - b - (c - d) = a + d - (b + c)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- The "base" of a set of points of a monoid relative to a morphism `f`.  -/
IsMulIndecomposable.baseOf : {ι : Type u_1} →
  {M : Type u_2} →
    {S : Type u_4} → [inst : Monoid M] → [LinearOrder S] → [inst_2 : Monoid S] → (ι → M) → (M →* S) → Set ι
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.quasiIsoAt_map_of_preservesHomology : ∀ {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C₂] [inst_2 : CategoryTheory.Preadditive C₁]
  [inst_3 : CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L)
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [F.PreservesHomology] (i : ι) [inst_6 : K.HasHomology i]
  [inst_7 : L.HasHomology i] [inst_8 : ((F.mapHomologicalComplex c).obj K).HasHomology i]
  [inst_9 : ((F.mapHomologicalComplex c).obj L).HasHomology i] [hφ : QuasiIsoAt φ i],
  QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i
-- Mathlib.Data.Set.Function
Set.image_eq_preimage_of_leftInvOn_injOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α},
  Set.LeftInvOn g f s → Set.InjOn g (g ⁻¹' s) → f '' s = g ⁻¹' s
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.le_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S T : CategoryTheory.Subgroupoid C),
  S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
iteratedFDeriv_sub_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f g : E → F},
  ContDiffAt 𝕜 (↑i) f x →
    ContDiffAt 𝕜 (↑i) g x → iteratedFDeriv 𝕜 i (f - g) x = iteratedFDeriv 𝕜 i f x - iteratedFDeriv 𝕜 i g x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instMulSubtypePreLpMemAddSubgroupTopENNReal : {I : Type u_5} → {B : I → Type u_6} → [inst : (i : I) → NonUnitalNormedRing (B i)] → Mul ↥(lp B ⊤)
-- Init.Data.Fin.Lemmas
Fin.coe_subNat : ∀ {n m : ℕ} (i : Fin (n + m)) (h : m ≤ ↑i), ↑(Fin.subNat m i h) = ↑i - m
-- Mathlib.Algebra.Order.Disjointed
Monotone.disjointed_add_one_sup : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : Add ι] [inst_4 : One ι] [SuccAddOrder ι] {f : ι → α},
  Monotone f → ∀ (i : ι), disjointed f (i + 1) ⊔ f i = f (i + 1)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Equality is achieved in the triangle inequality iff the two vectors are collinear.  -/
norm_add_eq_iff_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
-- Mathlib.Probability.HasLaw
MeasureTheory.MeasurePreserving.hasLaw : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  MeasureTheory.MeasurePreserving X P μ → ProbabilityTheory.HasLaw X μ P
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- See Note [custom simps projection].  -/
AbsoluteValue.Simps.apply : {R : Type u_5} →
  {S : Type u_6} → [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → R → S
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.summable : ∀ {α : Type u_1} {f : α → ENNReal}, Summable f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a `Monoid` under pointwise operations if `α` is.  -/
Finset.monoid : {α : Type u_2} → [DecidableEq α] → [Monoid α] → Monoid (Finset α)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Measurable.im : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m : MeasurableSpace α} {f : α → 𝕜},
  Measurable f → Measurable fun x => RCLike.im (f x)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.kronecker_hadamard_kronecker : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : CommSemigroup R] (A : Matrix l m R)
  (B : Matrix n p R) (C : Matrix l m R) (D : Matrix n p R),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).hadamard (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) C D) =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A.hadamard C) (B.hadamard D)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZero_apply_apply : ∀ {G : Type u_6} {H : Type u_7} [inst : Group G] [inst_1 : PartialOrder G] [inst_2 : Group H] [inst_3 : PartialOrder H]
  (e : G ≃*o H) (a : WithZero G), (OrderMonoidIso.withZero e) a = (WithZero.map' ↑↑e) a
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_mul : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p q : Polynomial R},
  p * q ≠ 0 → (p * q).roots = p.roots + q.roots
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instCommRingSubtypeMem : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → CommRing ↥A
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_eq_insertIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a), (m.getThenInsertIfNew? a b).2 = m.insertIfNewₘ a b