mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_eq_true_iff_forall_mem_getKey_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Const.get m a h) = true
-- Init.Data.Vector.Lemmas
/-- See also `eq_push_append_of_mem`, which proves a stronger version
in which the initial array must not contain the element.
 -/
Vector.append_of_mem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n},
  a ∈ xs → ∃ m k, ∃ (w : m + 1 + k = n), ∃ ys zs, xs = Vector.cast w (ys.push a ++ zs)
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Increase the universe level of a profunctor.  -/
CategoryTheory.Profunctor.ulift : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D → CategoryTheory.Profunctor.{max w' w, v₁, v₂, u₁, u₂} C D
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.trans_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : Star A] [inst_5 : Star B] [inst_6 : Add C] [inst_7 : Mul C] [inst_8 : Star C] (e₁ : A ≃⋆+* B)
  (e₂ : B ≃⋆+* C) (x : A), (e₁.trans e₂) x = e₂ (e₁ x)
-- Mathlib.Analysis.Complex.Exponential
Real.add_one_le_exp : ∀ (x : ℝ), x + 1 ≤ Real.exp x
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformly.hasSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformly f g → HasSum (fun x_1 => f x_1 x) (g x)
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_toBitVec : ∀ (x : Int32), Int32.ofBitVec x.toBitVec = x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_neg : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : NumberField.mixedEmbedding.mixedSpace K),
  (NumberField.mixedEmbedding.normAtPlace w) (-x) = (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `isSubset`.  -/
Ordnode.isSubsetAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Bool
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.machine : {β : Type} →
  Std.Http.Server.Connection.ConnectionState✝ β → Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.mk.inj : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {inst : CommSemiring R} {inst_1 : AddCommMonoid M₁}
  {inst_2 : AddCommMonoid M₂} {inst_3 : Module R M₁} {inst_4 : Module R M₂} {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} {toLinearMap : M₁ →ₗ[R] M₂}
  {map_app' : ∀ (m m' : M₁), (B₂ (toLinearMap.toFun m)) (toLinearMap.toFun m') = (B₁ m) m'}
  {toLinearMap_1 : M₁ →ₗ[R] M₂}
  {map_app'_1 : ∀ (m m' : M₁), (B₂ (toLinearMap_1.toFun m)) (toLinearMap_1.toFun m') = (B₁ m) m'},
  { toLinearMap := toLinearMap, map_app' := map_app' } = { toLinearMap := toLinearMap_1, map_app' := map_app'_1 } →
    toLinearMap = toLinearMap_1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.length_attachWith : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [Monad n] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out}
  [Std.Iterators.Finite α m] [inst_4 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m],
  (it.attachWith P hP).length = it.length
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is another convenient method to verify that a pushout cocone is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.PushoutCocone.isColimitAux' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (t : CategoryTheory.Limits.PushoutCocone f g) →
            ((s : CategoryTheory.Limits.PushoutCocone f g) →
                { l //
                  CategoryTheory.CategoryStruct.comp t.inl l = s.inl ∧
                    CategoryTheory.CategoryStruct.comp t.inr l = s.inr ∧
                      ∀ {m : t.pt ⟶ s.pt},
                        CategoryTheory.CategoryStruct.comp t.inl m = s.inl →
                          CategoryTheory.CategoryStruct.comp t.inr m = s.inr → m = l }) →
              CategoryTheory.Limits.IsColimit t
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffAddOfNatWithTopENatOfContinuousAdd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContinuousAdd G], ContMDiffAdd I 0 G
-- Mathlib.NumberTheory.NumberField.ClassNumber
NumberField.classNumber_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.classNumber K ≠ 0
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsQuasiPreprimitive.toIsPretransitive : ∀ {G : Type u_1} {X : Type u_2} {inst : AddGroup G} {inst_1 : AddAction G X} [self : AddAction.IsQuasiPreprimitive G X],
  AddAction.IsPretransitive G X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_one_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b c : α},
  a < 1 → b < c → a * b < c
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.isIntegral_iSup : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Sort u_5}
  (S : ι → Subalgebra R A), Algebra.IsIntegral R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral R ↥(S i)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.embeddingReal.congr_simp : ∀ (Ω : Type u_2) [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] (a a_1 : Ω),
  a = a_1 → MeasureTheory.embeddingReal Ω a = MeasureTheory.embeddingReal Ω a_1
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.convs'_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K],
  n ≤ m → g.TerminatedAt n → g.convs' m = g.convs' n
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.modularCharacterFun.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] (g : G),
  MeasureTheory.Measure.modularCharacterFun g =
    (MeasureTheory.Measure.map (fun x => x * g) MeasureTheory.Measure.haar).haarScalarFactor MeasureTheory.Measure.haar
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_neg : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G),
  Fintype.balance (-f) = -Fintype.balance f
-- Mathlib.Order.Quotient
Quotient.mk_lt_mk : ∀ {α : Type u_1} {s : Setoid α} [inst : LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected]
  {x y : α}, ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- `Ext` commutes with biproducts in its second variable.  -/
CategoryTheory.Abelian.Ext.addEquivBiproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        (X : C) →
          {J : Type u_1} →
            [Fintype J] →
              {Y : J → C} →
                {c : CategoryTheory.Limits.Bicone Y} →
                  c.IsBilimit →
                    (n : ℕ) → CategoryTheory.Abelian.Ext X c.pt n ≃+ ((i : J) → CategoryTheory.Abelian.Ext X (Y i) n)
-- Mathlib.Analysis.Convex.Extreme
isExtreme_sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {F : Set (Set E)}, F.Nonempty → (∀ B ∈ F, IsExtreme 𝕜 A B) → IsExtreme 𝕜 A (⋂₀ F)
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_bot : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Module.finrank R ↥⊥ = 0
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  {x y : P.FullSubcategory}, x = y ↔ x.obj = y.obj
-- Std.Data.DTreeMap.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.DTreeMap.Const.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} →
    {ρ : Type u_1} → [ForIn Id ρ α] → Std.DTreeMap α (fun x => Unit) cmp → ρ → Std.DTreeMap α (fun x => Unit) cmp
-- Init.Data.UInt.Lemmas
UInt8.ofNat_mod_size : ∀ {x : ℕ}, UInt8.ofNat (x % 2 ^ 8) = UInt8.ofNat x
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsCircuit.contract_sdiff_isCircuit`. -/
Matroid.IsCircuit.contract_diff_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, M.IsCircuit C → K.Nonempty → K ⊆ C → (M.contract (C \ K)).IsCircuit K
-- Mathlib.Analysis.SpecialFunctions.Log.Base
/-- The function `|logb b x|` tends to `+∞` as `x` tendsto `+∞`.
See also `tendsto_logb_atTop` and `tendsto_logb_atTop_of_base_lt_one`.
 -/
Real.tendsto_abs_logb_atTop : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → Filter.Tendsto (fun x => |Real.logb b x|) Filter.atTop Filter.atTop
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_sInf : ∀ {α : Type u_1} [inst : LE α] (S : Set (LowerSet α)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_union_Ioc_eq_Iic : ∀ {α : Type u_2} {a b : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : LocallyFiniteOrderBot α],
  a ≤ b → Finset.Iic a ∪ Finset.Ioc a b = Finset.Iic b
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_union_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s t : Finset α),
  addRothNumber (s ∪ t) ≤ addRothNumber s + addRothNumber t
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_one_right : ∀ (n : ℕ), n.choose 1 = n
-- Mathlib.Order.Filter.Lift
Filter.map_lift_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {m : β → γ},
  Monotone g → Filter.map m (f.lift g) = f.lift (Filter.map m ∘ g)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.sum : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {ι : Type} {t : Finset ι} {f : ι → M → E'}, (∀ i ∈ t, MDiff (f i)) → MDiff (∑ i ∈ t, f i)
-- Init.Data.Array.Count
Array.count_reverse : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, Array.count a xs.reverse = Array.count a xs
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertyInl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Y} {s : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [CategoryTheory.HasLiftingProperty f p],
  CategoryTheory.HasLiftingProperty (CategoryTheory.Limits.pushout.inl s f) p
-- Mathlib.Data.Int.Log
Int.clog_zero_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ), Int.clog b 0 = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace.expandedCoeDecls : Lean.Elab.Term.CoeExpansionTrace → List Lean.Name
-- Mathlib.Topology.UniformSpace.Pi
instIsCountablyGeneratedProdForallUniformityOfCountable : ∀ {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] [Countable ι]
  [∀ (i : ι), (uniformity (α i)).IsCountablyGenerated], (uniformity ((i : ι) → α i)).IsCountablyGenerated
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
biUnion_associatedPrimes_eq_compl_nonZeroDivisors : ∀ (R : Type u_1) [inst : CommSemiring R] [IsNoetherianRing R], ⋃ p ∈ associatedPrimes R R, ↑p = (↑(nonZeroDivisors R))ᶜ
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Lean.Meta.RefinedDiscrTree
/-- Creates the core context used for initializing a tree using the current context.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.0.Lean.Meta.RefinedDiscrTree.withTreeCtx : Lean.Core.Context → Lean.Core.Context
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- If `c` is a colimiting pushout cocone, then we have an `IsPushout f g c.inl c.inr`.  -/
CategoryTheory.IsPushout.of_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {c : CategoryTheory.Limits.PushoutCocone f g} (h : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsPushout f g c.inl c.inr
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_3.eq_1 : ∀ (motive : ONote × ℕ → Sort u_1) (h_1 : Unit → motive (ONote.zero, 0)) (h_2 : Unit → motive (ONote.zero, 1))
  (h_3 : (m : ℕ) → motive (ONote.zero, m.succ))
  (h_4 : (a a0 : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → a = a0.oadd a_1 a_2 → (m : ℕ) → motive (a0.oadd a_1 a_2, m)),
  (match (ONote.zero, 0) with
    | (ONote.zero, 0) => h_1 ()
    | (ONote.zero, 1) => h_2 ()
    | (ONote.zero, m.succ) => h_3 m
    | (a@h:(a0.oadd a_1 a_2), m) => h_4 a a0 a_1 a_2 h m) =
    h_1 ()
-- Init.Data.Rat.Lemmas
Rat.abs.eq_1 : ∀ (a : ℚ), a.abs = if 0 ≤ a then a else -a
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ),
  (f.sumElim g).support = f.support.disjSum g.support
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.residueFieldMapCAlgEquiv_symm_X : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (J : Ideal (Polynomial R)) [inst_2 : J.IsPrime]
  [inst_3 : J.LiesOver I] [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] (hJ : J = Ideal.map Polynomial.C I),
  (Polynomial.residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X = (algebraMap (Polynomial R) J.ResidueField) Polynomial.X
-- Mathlib.Logic.Denumerable
/-- A type equivalent to `ℕ` is denumerable.  -/
Denumerable.mk' : {α : Type u_3} → α ≃ ℕ → Denumerable α
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_zero_left : ∀ {p x : ℝ}, 0 < p → p.rpowIntegrand₀₁ 0 x = 0
-- Batteries.Recycling.RBTree.WF
/-- The `balance1` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.balance1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l →
    RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r →
      RBTree.RBNode.Ordered cmp l → RBTree.RBNode.Ordered cmp r → RBTree.RBNode.Ordered cmp (l.balance1 v r)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_update : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R) [inst_1 : Decidable (a = 0)],
  (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
-- Lean.Parser.Basic
Lean.Parser.ParserCategory.mk.sizeOf_spec : ∀ (declName : Lean.Name) (kinds : Lean.Parser.SyntaxNodeKindSet) (tables : Lean.Parser.PrattParsingTables)
  (behavior : Lean.Parser.LeadingIdentBehavior),
  sizeOf { declName := declName, kinds := kinds, tables := tables, behavior := behavior } =
    1 + sizeOf declName + sizeOf kinds + sizeOf tables + sizeOf behavior
-- Init.Data.Float.Model.Float
/-- Returns `true` if the float is `NaN`.
 -/
Float.Model.isNaN : Float.Model → Bool
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_cpow_of_lt : ∀ {a : ℂ}, a.re < -1 → ∀ {c : ℝ}, 0 < c → MeasureTheory.IntegrableOn (fun t => ↑t ^ a) (Set.Ioi c) MeasureTheory.volume
-- Init.Meta.Defs
Lean.Syntax.isCharLit? : Lean.Syntax → Option Char
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.eq_right : ∀ {α : Type u_2} [inst : AddCommMonoid α] [IsCancelAdd α] {s : Set α},
  ThreeAPFree s → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → b = c
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLp_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : RCLike 𝕜] [inst_2 : NormedSpace 𝕜 E] [inst_3 : OpensMeasurableSpace E]
  [inst_4 : Fact (1 ≤ p)], ¬MeasureTheory.MemLp id p μ → ∀ (L : StrongDual 𝕜 E), (StrongDual.toLp μ p) L = 0
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.fourierInv_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ),
  (FourierTransformInv.fourierInv f) g = f (FourierTransformInv.fourierInv g)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Reduction step for the multiplicative free group relation: `w * x * x⁻¹ * v ~> w * v`  -/
FreeGroup.Red.Step : {α : Type u} → List (α × Bool) → List (α × Bool) → Prop
-- Mathlib.Analysis.Convex.StrictCombination
dist_affineCombination_lt_of_strictConvexSpace : ∀ {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [StrictConvexSpace ℝ V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {t : Finset ι} {w : ι → ℝ}
  {p₀ : P} {r : ℝ} {p : ι → P},
  (∀ i ∈ t, 0 ≤ w i) →
    ∑ i ∈ t, w i = 1 →
      ∀ {i j : ι},
        i ∈ t →
          j ∈ t →
            p i ≠ p j →
              w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, dist (p i) p₀ ≤ r) → dist ((Finset.affineCombination ℝ t p) w) p₀ < r
-- Mathlib.Algebra.Group.Commute.Hom
AddSemiconjBy.of_map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {a x y : M} [inst_2 : FunLike F M N]
  [AddHomClass F M N] {f : F}, Function.Injective ⇑f → AddSemiconjBy (f a) (f x) (f y) → AddSemiconjBy a x y
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_at_ofNat : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ)
  [inst_2 : n.AtLeastTwo], Polynomial.eval₂ f (OfNat.ofNat n) p = f (Polynomial.eval (OfNat.ofNat n) p)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.range_comp : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : B →ₐ[R] C), (g.comp f).range = Subalgebra.map g f.range
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_eq_self_iff : ∀ {α : Type u} {d : α} {x : WithZero α}, WithZero.unzeroD d x = d ↔ x = ↑d ∨ x = 0
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.IsLeftDerivedFunctor.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : L.comp LF ⟶ F),
  α = α_1 →
    ∀ (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W],
      LF.IsLeftDerivedFunctor α W = LF.IsLeftDerivedFunctor α_1 W_1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_comp_natAdd : ∀ {n m : ℕ} {α : Sort u_2} (f : Fin (m + n) → α) (a : α), Fin.snoc f a ∘ Fin.natAdd m = Fin.snoc (f ∘ Fin.natAdd m) a
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.basicOpen_pow : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))) (n : ℕ), 0 < n → X.basicOpen (f ^ n) = X.basicOpen f
-- Std.Http.Data.URI.Basic
Std.Http.URI.instToStringAuthority : ToString Std.Http.URI.Authority
-- Mathlib.Algebra.Order.Floor.Defs
/-- A version of `Nat.mono_cast` for floor semirings, whose addition is not necessarily monotone.  -/
FloorSemiring.natCast_mono : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [FloorSemiring α], Monotone Nat.cast
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_inl : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [NontrivialTopology E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F],
  ‖ContinuousLinearMap.inl 𝕜 E F‖ = 1
-- Mathlib.Topology.Order.OrderClosed
instClosedIciTopology : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α], ClosedIciTopology α
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_of_yoneda_map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp x f) → CategoryTheory.IsIso f
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.quot_mk_eq_mk : ∀ {M : Type u_1} [inst : Monoid M] (a : M), Quot.mk (⇑(Associated.setoid M)) a = Associates.mk a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.anodyneExtensions.horn_ι : ∀ {n : ℕ} [NeZero n] (i : Fin (n + 1)), SSet.anodyneExtensions (SSet.horn n i).ι
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`,
with specialized universes.  -/
CategoryTheory.Limits.Types.pi_map_π_apply' : ∀ {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) =
    (CategoryTheory.ConcreteCategory.hom (α b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ : CategoryTheory.Subobject X) {J : Type w} [inst_3 : LinearOrder J] [OrderBot J] [inst_5 : SuccOrder J]
  [inst_6 : WellFoundedLT J],
  HasCardinalLT (CategoryTheory.Subobject X) (Cardinal.mk J) →
    ∃ j, transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀ = ⊤
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_two_mul : ∀ (x : ℝ), Real.cosh (2 * x) = Real.cosh x ^ 2 + Real.sinh x ^ 2