mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Bounded
/-- A `BotHomClass` morphism preserves the bottom element.  -/
BotHomClass.map_bot : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Bot α} {inst_1 : Bot β}
  {inst_2 : FunLike F α β} [self : BotHomClass F α β] (f : F), f ⊥ = ⊥
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f t[k]?).isSome = true else k' ∈ t
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapM f it)).toListRev =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toListRev
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Counterpart to `List.sum_take_succ` when we have a negation operation  -/
List.sum_drop_succ : ∀ {G : Type u_7} [inst : AddGroup G] (L : List G) (i : ℕ) (p : i < L.length),
  (List.drop (i + 1) L).sum = -L[i] + (List.drop i L).sum
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.sSup_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (S : Set (I.Filtration M)), (sSup S).N = sSup (Ideal.Filtration.N '' S)
-- Init.Data.SInt.Bitwise
Int32.and_not_self : ∀ {a : Int32}, a &&& ~~~a = 0
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.toInvMemClass : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : DivInvMonoid G} {inst_1 : SetLike S G} [self : SubgroupClass S G],
  InvMemClass S G
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.rankGT : ∀ {α : Type u_1} {lt : α → α → Bool} {n : ℕ} {s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) s → s.rankGT n
-- Mathlib.Order.CompleteLattice.Basic
Pi.supSet : {α : Type u_8} → {β : α → Type u_9} → [(i : α) → SupSet (β i)] → SupSet ((i : α) → β i)
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.image_sdiff_preimage`. -/
Set.image_diff_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, f '' (s \ f ⁻¹' t) = f '' s \ t
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSemisimple.instDistribLattice : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → [LieAlgebra.IsSemisimple R L] → DistribLattice (LieIdeal R L)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape.congr_simp : ∀ {Γ : Type u_1} {n : ℕ} {enc enc_1 : Γ → List.Vector Bool n} (e_enc : enc = enc_1) [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (T T_1 : Turing.Tape Γ),
  T = T_1 → Turing.TM1to1.trTape enc0 T = Turing.TM1to1.trTape ⋯ T_1
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Abundant.mul_left : ∀ {n m : ℕ}, n.Abundant → m ≠ 0 → (m * n).Abundant
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- A version of `DifferentiableAt.cpow_const` for a real function.  -/
DifferentiableAt.ofReal_cpow_const : ∀ {c : ℂ} {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → f x ≠ 0 → c ≠ 0 → DifferentiableAt ℝ (fun y => ↑(f y) ^ c) x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_tensor : ∀ (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : AddCommMonoid P] [inst_10 : Module A P] [inst_11 : AddCommMonoid P'] [inst_12 : Module A P']
  [inst_13 : Module R P] [inst_14 : IsScalarTower R A P] [inst_15 : Module R P'] [inst_16 : IsScalarTower R A P']
  (g : P →ₗ[A] P'),
  LinearMap.rTensor (TensorProduct R M N) g =
    ↑(TensorProduct.AlgebraTensorModule.assoc R A A P' M N) ∘ₗ
      TensorProduct.AlgebraTensorModule.map (LinearMap.rTensor M g) LinearMap.id ∘ₗ
        ↑(TensorProduct.AlgebraTensorModule.assoc R A A P M N).symm
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.coe_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (s : Set α) (f : C(α, β)),
  ⇑(ContinuousMap.restrict s f) = s.domRestrict ⇑f
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) {FD : D → D → Type u_3} {CD : D → Type u_4}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : CategoryTheory.ConcreteCategory D FD]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (CategoryTheory.forget D)]
  [inst_12 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_13 : (CategoryTheory.forget D).ReflectsIsomorphisms],
  (J.sheafifyCompIso F P).inv = J.sheafifyLift (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) ⋯
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.Candidate.π_desc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v)
  {w : CategoryTheory.Arrow V} (g : v ⟶ w)
  (h : CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f g) 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Preadditive.RightFreyd.Candidate.π f)
      (CategoryTheory.Preadditive.RightFreyd.Candidate.desc f g h) =
    g
-- Mathlib.Algebra.Group.Translate
translate_smul_right : ∀ {α : Type u_2} {G : Type u_5} {H : Type u_6} [inst : AddCommGroup G] [inst_1 : SMul H α] (a : G) (f : G → α) (c : H),
  translate a (c • f) = c • translate a f
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α),
  μ s < ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.cyclesMap'_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R),
  CategoryTheory.ShortComplex.cyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂
-- Mathlib.Data.TypeVec
TypeVec.prod.snd.eq_def : ∀ (x : ℕ) (x_1 x_2 : TypeVec.{u} x) (x_3 : Fin2 x),
  TypeVec.prod.snd x_3 =
    match (motive := (x : ℕ) → (x_4 x_5 : TypeVec.{u} x) → (x_6 : Fin2 x) → x_4.prod x_5 x_6 → x_5 x_6) x, x_1, x_2,
      x_3 with
    | n.succ, α, β, i.fs => TypeVec.prod.snd i
    | n.succ, x, x_4, Fin2.fz => Prod.snd
-- Std.Http.Data.Request
/-- Creates a new HTTP PUT Request builder with the specified URI.
 -/
Std.Http.Request.put : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Order.Filter.NAry
Filter.map₂_mono : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β},
  f₁ ≤ f₂ → g₁ ≤ g₂ → Filter.map₂ m f₁ g₁ ≤ Filter.map₂ m f₂ g₂
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.congr_arrowMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂),
  CategoryTheory.SmallObject.SuccStruct.arrowMap iter₁.F k₁ k₂ h h₁ =
    CategoryTheory.SmallObject.SuccStruct.arrowMap iter₂.F k₁ k₂ h h₂
-- Mathlib.Tactic.Core
/-- `iterateUntilFailureWithResults` is a helper tactic which accumulates the list of results
obtained from iterating `tac` until it fails. Always succeeds.
 -/
Lean.Elab.Tactic.iterateUntilFailureWithResults : {m : Type → Type u} → [Monad m] → [MonadExcept Lean.Exception m] → {α : Type} → m α → m (List α)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovDist_self : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovDist μ μ = 0
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_zero_index : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (f : ℕ → R → S),
  SkewPolynomial.sum 0 f = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `Ω n` is the number of prime factors of `n`.  -/
ArithmeticFunction.Omega.termΩ : Lean.ParserDescr
-- Mathlib.Topology.Separation.Basic
SeparationQuotient.t1Space_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space (SeparationQuotient X) ↔ R0Space X
-- Lean.Data.Position
Lean.instDecidableEqPosition : DecidableEq Lean.Position
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The linear equivalence `Cochain K L n ≃+ Cochain K L⟦a⟧ n'` when `n' + a = n` and
the category is `R`-linear.  -/
CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type u_1) →
        [inst_2 : Ring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            (K L : CochainComplex C ℤ) →
              (n a n' : ℤ) →
                n' + a = n →
                  CochainComplex.HomComplex.Cochain K L n ≃ₗ[R]
                    CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
-- Mathlib.Topology.Sheaves.Limits
TopCat.isSheaf_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{v_1, w} J]
  [CategoryTheory.Limits.HasLimitsOfShape J C] {X : TopCat} (F : CategoryTheory.Functor J (TopCat.Presheaf C X)),
  (∀ (j : J), (F.obj j).IsSheaf) →
    ∀ {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c), c.pt.IsSheaf
-- Lean.Elab.Coinductive
Lean.Elab.Command.instInhabitedCoinductiveElabData : Inhabited Lean.Elab.Command.CoinductiveElabData
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.map_normNoninc : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {W₁ : Type u_6} {W₂ : Type u_7} [inst_2 : SeminormedAddCommGroup W₁] [inst_3 : SeminormedAddCommGroup W₂]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂}
  {ψ : NormedAddGroupHom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ),
  φ.NormNoninc → (NormedAddGroupHom.Equalizer.map φ ψ hf hg).NormNoninc
-- Lean.Parser.Term
Lean.Parser.Term.logNamedWarningMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.inv_comp_image_ι_map : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv
      (CategoryTheory.Limits.image.ι (L.map f)) =
    L.map (CategoryTheory.Limits.image.ι f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.union! m₂) k = Std.DTreeMap.Internal.Impl.Const.get! m₂ k
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.MonadGetStruct.mk : {m : Type → Type} → m Lean.Meta.Grind.AC.Struct → Lean.Meta.Grind.AC.MonadGetStruct m
-- Mathlib.Data.Nat.Bitwise
Nat.ldiff_bit : ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), (Nat.bit a m).ldiff (Nat.bit b n) = Nat.bit (a && !b) (m.ldiff n)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves the action.  -/
MulActionSemiHomClass.map_smulₛₗ : ∀ {F : Type u_8} {M : outParam (Type u_9)} {N : outParam (Type u_10)} {φ : outParam (M → N)} {X : outParam (Type u_11)}
  {Y : outParam (Type u_12)} {inst : SMul M X} {inst_1 : SMul N Y} {inst_2 : FunLike F X Y}
  [self : MulActionSemiHomClass F φ X Y] (f : F) (c : M) (x : X), f (c • x) = φ c • f x
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.continuousAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → ContinuousAt f x
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.encodePosNum.match_1.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → (Unit → motive PosNum.one) → ((n : PosNum) → motive n.bit0) → ((n : PosNum) → motive n.bit1) → motive x
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonPartialResultParams : Lean.ToJson Lean.Lsp.PartialResultParams
-- Mathlib.Algebra.BrauerGroup.Defs
CSA.mk.sizeOf_spec : ∀ {K : Type u} [inst : Field K] [inst_1 : SizeOf K] (toAlgCat : AlgCat K) [isCentral : Algebra.IsCentral K ↑toAlgCat]
  [isSimple : IsSimpleRing ↑toAlgCat] [fin_dim : FiniteDimensional K ↑toAlgCat],
  sizeOf { toAlgCat := toAlgCat, isCentral := isCentral, isSimple := isSimple, fin_dim := fin_dim } =
    1 + sizeOf toAlgCat + sizeOf isCentral + sizeOf isSimple + sizeOf fin_dim
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.Iter.toHashSet_equiv_ofList : ∀ {α β : Type w} {x : BEq β} {x_1 : Hashable β} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β},
  it.toHashSet.Equiv (Std.HashSet.ofList it.toList)
-- Mathlib.Order.WithBot
WithTop.untopA_eq_untop : ∀ {α : Type u_1} [inst : Nonempty α] {a : WithTop α} (ha : a ≠ ⊤), a.untopA = a.untop ha
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_edist_triangle : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g h : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable h μ →
      ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instAddCommMonoid.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddMonoidAlgebra.instAddCommMonoid = { toAddMonoid := AddMonoidAlgebra.instAddMonoid, add_comm := ⋯ }
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_mul_right : ∀ (a b : ℤ), a ∣ a * b
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.cocone_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C)
  (S : LightProfinite), (LightProfinite.Extend.cocone G S).pt = G.obj (Opposite.op S)
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a tower of algebras `S/P/R`, with `I = ker(P → S)` and `Q := P/I²`,
there is an isomorphism of `S`-modules `S ⊗[Q] Ω[Q/R] ≃ S ⊗[P] Ω[P/R]`.
 -/
tensorKaehlerQuotKerSqEquiv : (R : Type u_1) →
  (P : Type u_2) →
    (S : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                [inst_5 : Algebra R S] →
                  [IsScalarTower R P S] →
                    TensorProduct (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S
                        Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] ≃ₗ[S]
                      TensorProduct P S Ω[P⁄R]
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_inv : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  ⇑f⁻¹ = ⇑f.symm
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply : ∀ (R : Type u) (X : Type v) [inst : CommRing R] (a : UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)),
  (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X) a =
    ((UniversalEnvelopingAlgebra.lift R) ((FreeLieAlgebra.lift R) (FreeAlgebra.ι R))) a
-- Mathlib.Algebra.Category.Grp.Biproducts
/-- The map from an arbitrary cone over an indexed family of abelian groups
to the Cartesian product of those groups.
 -/
AddCommGrpCat.HasLimit.lift : {J : Type w} → (f : J → AddCommGrpCat) → (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ AddCommGrpCat.of ((j : J) → ↑(f j))
-- Init.Data.Order.Lemmas
Std.not_lt : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderLT α] {a b : α},
  ¬a < b ↔ b ≤ a
-- Lean.Elab.DocString
/-- Asserts that there are no further arguments to a documentation language extension.
 -/
Lean.Doc.done : StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM Unit
-- Mathlib.Tactic.Push.Attr
/-- The `push` environment extension  -/
Mathlib.Tactic.Push.pushExt : Lean.SimpleScopedEnvExtension Lean.Meta.SimpTheorem (Lean.Meta.DiscrTree Lean.Meta.SimpTheorem)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_sub_one_right_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a < b → insert b (Set.Ioc a (b - 1)) = Set.Ioc a b
-- Lean.Parser.Term
Lean.Parser.Term.matchAlt : optParam Lean.Parser.Parser Lean.Parser.termParser → Lean.Parser.Parser
-- Init.Data.BitVec.Lemmas
BitVec.abs_eq : ∀ {w : ℕ} (x : BitVec w), x.abs = if x.msb = true then -x else x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given `F : Set.Iio i ⥤ C`, with `i` a limit element, and `k` such that `hk : k < i`,
this is the map `colimit.ι F ⟨k, hk⟩`, as an element in `Arrow C`.  -/
CategoryTheory.SmallObject.SuccStruct.arrowι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [CategoryTheory.Limits.HasIterationOfShape J C] →
          {i : J} →
            CategoryTheory.Functor (↑(Set.Iio i)) C → Order.IsSuccLimit i → (k : J) → k < i → CategoryTheory.Arrow C
-- Mathlib.NumberTheory.LSeries.SumCoeff
/-- If `f` takes nonnegative real values and the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)`
for some real `0 ≤ r`, then the L-series `LSeries f` converges at `s : ℂ` for all `s`
such that `r < s.re`.  -/
LSeriesSummable_of_sum_norm_bigO_and_nonneg : ∀ {r : ℝ} {s : ℂ} {f : ℕ → ℝ},
  ((fun n => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun n => ↑n ^ r) →
    (∀ (n : ℕ), 0 ≤ f n) → 0 ≤ r → r < s.re → LSeriesSummable (fun n => ↑(f n)) s
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.self_trans_symm : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), e.trans e.symm = LieModuleEquiv.refl
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- An initial object is initial.  -/
CategoryTheory.Limits.initialIsInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] → CategoryTheory.Limits.IsInitial (⊥_ C)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier : ∀ {R : Type u} [inst : Semiring R], (CategoryTheory.forget (SemimoduleCat R)).ReflectsIsomorphisms
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_add : ∀ {a b c : UInt16}, b < 16 → c < 16 → b + c < 16 → a <<< (b + c) = a <<< b <<< c
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Given `K : ChainComplex C ℕ` and `L : CochainComplex C ℕ`, this data
allows to connect `K` and `L` in order to get a cochain complex indexed by `ℤ`,
see `ConnectData.cochainComplex`.  -/
CochainComplex.ConnectData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → ChainComplex C ℕ → CochainComplex C ℕ → Type v
-- Mathlib.CategoryTheory.Presentable.Finite
/-- A morphism `f : X ⟶ Y` is finitely presentable if it is so as an object of `Under X`.  -/
CategoryTheory.MorphismProperty.isFinitelyPresentable : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocRing.toMul : {α : Type u} → [self : NonUnitalNonAssocRing α] → Mul α
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_eq_zero_iff : ∀ {x : ℝ}, 1 ≤ x → (Real.arcosh x = 0 ↔ x = 1)
-- Mathlib.Algebra.Order.Floor.Defs
/-- `Int.ceil a` is the smallest integer `z` such that `a ≤ z`. It is denoted with `⌈a⌉`.  -/
Int.«term⌈_⌉» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Fork.ofι f pushout.condition` is a limit cone if and only if
`Cofork.ofπ f.op pullback.condition` in the opposite category is a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkOpPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasPushout f f] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯) ≃
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f.op ⋯)