mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- A function from sections of a vector bundle `V` on a manifold `M` to sections of $Hom(TM, E)$
is a *covariant derivative* over a set `s` in `M` if it is additive and satisfies the Leibniz rule
when applied to sections that are differentiable at a point of `s`.

Caution, the argument order is nonstandard: `cov σ x (X x)` corresponds to `∇_X σ x` on paper.
 -/
IsCovariantDerivativeOn : {𝕜 : 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] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [FiberBundle F V] →
                                            (((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) →
                                              optParam (Set M) Set.univ → Prop
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.FastSubsingleton.helim : ∀ {α β : Sort u} [Lean.Meta.FastSubsingleton α], α = β → ∀ (a : α) (b : β), a ≍ b
-- Mathlib.Order.BooleanAlgebra.Basic
sup_inf_inf_compl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⊓ y ⊔ x ⊓ yᶜ = x
-- Mathlib.Data.Set.Card
Set.one_lt_encard_iff_nontrivial : ∀ {α : Type u_1} {s : Set α}, 1 < s.encard ↔ s.Nontrivial
-- Init.Data.SInt.Bitwise
instAssociativeInt32HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  t.isEmpty = true → ∀ {fallback : α}, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKeyD fallback = k
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1}
  (U : ι → ↑Y.affineOpens), ⨆ i, ↑(U i) = ⊤ → (P f ↔ ∀ (i : ι), Q (f ∣_ ↑(U i)))
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv.eq_1 : ∀ {X : SSet} {n : SimplexCategory}, SSet.yonedaEquiv = CategoryTheory.uliftYonedaEquiv
-- Lean.Parser.Types
/-- Parser context updateable in `adaptUncacheableContextFn`.  -/
Lean.Parser.ParserContextCore : Type
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice},
  s.dropWhile pat = s ↔ s.startsWith pat = false
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mul_refl : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e : E ≃ₗᵢ[R] E), e * LinearIsometryEquiv.refl R E = e
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder β] (f : LatticeHom α β)
  (a : WithTop (WithBot α)), f.withTopWithBot' a = Option.elim a ⊤ ⇑f.withBot'
-- Lean.Data.KVMap
Lean.KVMap.getName : Lean.KVMap → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Lean.Name
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep_iff_iIndepSets : ∀ {Ω : Type u_1} {ι : Type u_2} (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndep m μ ↔ ProbabilityTheory.iIndepSets (fun x => {s | MeasurableSet s}) μ
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_nonneg' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)), 0 ≤ ‖f‖
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_leOnePart_inj : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a b : α} [MulLeftMono α], a⁺ᵐ = b⁺ᵐ ∧ a⁻ᵐ = b⁻ᵐ ↔ a = b
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.le_linearGrowthSup_comp : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  Monotone u →
    (LinearGrowth.linearGrowthInf fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * LinearGrowth.linearGrowthSup u ≤
        LinearGrowth.linearGrowthSup (u ∘ v)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe_ennreal : ∀ {α : Type u_2} {f : Filter α} {m : α → ENNReal} {a : ENNReal},
  Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)
-- Init.Core
/-- Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.

Given `s : Setoid α` and a quotient value `q : Quotient s`, applying a function `f : α → β` requires
a proof `c` that `f` respects the equivalence relation `s.r`. In this case, the term
`Quotient.liftOn q f h : β` reduces to the result of applying `f` to the underlying `α` value.

`Quotient.lift` is a version of this operation that takes the quotient value last, rather than
first.
 -/
Quotient.liftOn : {α : Sort u} → {β : Sort v} → {s : Setoid α} → Quotient s → (f : α → β) → (∀ (a b : α), a ≈ b → f a = f b) → β
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.instInhabited : {A : Type u_1} → [inst : Add A] → [inst_1 : Mul A] → [inst_2 : Star A] → Inhabited (A ≃⋆+* A)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mulTSupport_extend_one_subset : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : One β] {f : α → β} [T2Space α'],
  HasCompactMulSupport f → ∀ {g : α → α'}, Continuous g → mulTSupport (Function.extend g f 1) ⊆ g '' mulTSupport f
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.involute_e0 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), CliffordAlgebra.involute (CliffordAlgebra.EquivEven.e0 Q) = -CliffordAlgebra.EquivEven.e0 Q
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_injective_of_isUnit : ∀ {m : Type u_2} {R : Type u_7} [inst : Semiring R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {A : Matrix m m R},
  IsUnit A → Function.Injective A.mulVec
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'} {y : M'},
  MDiffAt[u] g y →
    MDiffAt[s] f x →
      f ⁻¹' u ∈ nhdsWithin x s → UniqueMDiffAt[s] x → f x = y → mfderiv[s] (g ∘ f) x = mfderiv[u] g y ∘SL mfderiv[s] f x
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LE β] (l : Filter α) (f g : α → β), (f ≤ᶠ[l] g) = ∀ᶠ (x : α) in l, f x ≤ g x
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instNonemptyExtensionProduct : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C) [P.Nonempty] [Q.Nonempty], (P.extensionProduct Q).Nonempty
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.rel_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  (i₁ i₂ : ι), c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveOn.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  IsIntegralCurveOn γ v s → ∀ (dt : ℝ), IsIntegralCurveOn (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt) (-dt +ᵥ s)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instInhabited : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Inhabited (ModularForm Γ k)
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `cancelDenoms pf` assumes `pf` is a proof of `t R 0`. If `t` contains the division symbol `/`,
it tries to scale `t` to cancel out division by numerals.
 -/
Mathlib.Tactic.Linarith.cancelDenoms : Mathlib.Tactic.Linarith.Preprocessor
-- Mathlib.MeasureTheory.Function.Jacobian
MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  MeasurableSet s →
    ∀ (f : E ≃ᵐ E) {g : E → ℝ},
      (∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x) →
        MeasureTheory.IntegrableOn g (⇑f '' s) μ →
          (∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x) →
            (MeasureTheory.Measure.map (⇑f.symm) (μ.withDensity fun x => ENNReal.ofReal (g x))) s =
              ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
-- Lean.Message
Lean.MessageLog.getWarningMessages : Lean.MessageLog → Lean.MessageLog
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k'
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.nhdsWithin_neBot : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → ∀ (b : β), (nhdsWithin b (Set.range i)).NeBot
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.pullback f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.op g.op)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g).op h
-- Mathlib.Tactic.Linter.Style
/-- The `setOption` linter: this lints any `set_option` command, term or tactic
which sets a `debug`, `pp`, `profiler` or `trace` option.
This also warns if an option containing `maxHeartbeats` (typically, the `maxHeartbeats` or
`synthInstance.maxHeartbeats` option) or the `linter.flexible` or
`backward.inferInstanceAs.wrap.reuseSubInstances ` option is set.

**Why is this bad?** The `debug`, `pp`, `profiler` and `trace` options are good for debugging,
but should not be used in production code.

`maxHeartbeats` options should be scoped as `set_option opt in ...` (and be followed by a comment
explaining the need for them; another linter enforces this).
The `linter.flexible` option should be scoped as `set_option opt in ...`.

**How to fix this?** The `maxHeartbeats` and `linter.flexible` option changes can be scoped to
individual commands, if they are truly necessary.
New `backward.inferInstanceAs.wrap.reuseSubInstances` instances are technical debt,
and should not be introduced.

The `debug`, `pp`, `profiler` and `trace` are usually not necessary for production code,
so you can simply remove them. (Some tests will intentionally use one of these options;
in this case, simply allow the linter.)
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.setOption.setOptionLinter : Lean.Linter
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' fallback : α}, cmp k k' = Ordering.eq → t.getD k fallback = t.getD k' fallback
-- Batteries.Data.List.Basic
/-- Auxiliary for `scanAuxM`  -/
List.scanAuxM.go : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → List α → β → List β → m (List β)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyLike.mk : ∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {F : Type u_5} {f₀ f₁ : outParam C(X, Y)} [inst_2 : FunLike F (↑unitInterval × X) Y]
  [toContinuousMapClass : ContinuousMapClass F (↑unitInterval × X) Y],
  (∀ (f : F) (x : X), f (0, x) = f₀ x) → (∀ (f : F) (x : X), f (1, x) = f₁ x) → ContinuousMap.HomotopyLike F f₀ f₁
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ContinuousMonoidHom.mk.congr_simp : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (toMonoidHom toMonoidHom_1 : A →* B) (e_toMonoidHom : toMonoidHom = toMonoidHom_1)
  (continuous_toFun : Continuous (↑toMonoidHom).toFun),
  { toMonoidHom := toMonoidHom, continuous_toFun := continuous_toFun } =
    { toMonoidHom := toMonoidHom_1, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `le_mul_of_one_le_right` for `a` non-positive instead of non-negative.  -/
mul_le_of_one_le_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R]
  [AddRightReflectLE R], a ≤ 0 → 1 ≤ b → a * b ≤ a
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.Hom.le_iff_le`. -/
CategoryTheory.CardinalFilteredPoset.Hom.le_iff_le : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J₁ J₂ : CategoryTheory.CardinalDirectedPoset κ} (f : J₁ ⟶ J₂)
  (x₁ x₂ : ↑J₁.obj), (CategoryTheory.ConcreteCategory.hom f) x₁ ≤ (CategoryTheory.ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] {c c' : C} {d d_1 : D} (f : c ⟶ c')
  (g : d ⟶ d_1),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom g f.mop
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_trans_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  h.symm.trans h = Diffeomorph.refl J N n
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.eval₂_eval₂RingHom_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x y : S)
  (p : Polynomial (Polynomial R)),
  Polynomial.eval₂ (Polynomial.eval₂RingHom f x) y p =
    Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom f) p)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t = ∅ ↔ ∀ (a : α), a ∉ t
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_cgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω},
  MeasurableSet s →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      (μ.tilted fun x => t * X x) s =
        ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a - ProbabilityTheory.cgf X μ t)) ∂μ
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.ofPowerSeries_apply_one : ∀ {R : Type u_1} [inst : CommSemiring R] (q : ℕ) (f : PowerSeries R),
  ((ArithmeticFunction.ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C),
  ((t.eTriangleLTGE.obj i).obj j).mor₃ = (t.eTruncGEδLT.app i).app j
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseRightKanExtension.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L L_1 : CategoryTheory.Functor C D) (e_L : L = L_1) (F F_1 : CategoryTheory.Functor C H) (e_F : F = F_1)
  [inst_3 : L.HasPointwiseRightKanExtension F], L.pointwiseRightKanExtension F = L_1.pointwiseRightKanExtension F_1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.inv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.toPartialEquiv_coe_symm : ∀ {𝕜 : 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),
  ↑I.symm = ↑I.symm
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves finite coproducts, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
products.  -/
CategoryTheory.Limits.preservesFiniteProducts_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteCoproducts F],
  CategoryTheory.Limits.PreservesFiniteProducts F.rightOp
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instSub : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → Sub (QuadraticMap R M N)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.isCoinductive : Lean.Elab.Command.AddAndFinalizeContext✝ → Bool
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_4 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (k : ℤ) (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match Int.Internal.Linear.Expr.num k with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_4 k
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monToMonad_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  (CategoryTheory.Monad.monToMonad C).obj M = CategoryTheory.Monad.ofMon M
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a + b`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalAdd : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprLevelMVarId_mathlib.toExpr : Lean.LevelMVarId → Lean.Expr
-- Mathlib.Data.PFunctor.Univariate.M
/-- constructor for M-types  -/
PFunctor.M.mk : {F : PFunctor.{uA, uB}} → ↑F F.M → F.M
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inl_left_mul_inr_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (x : N ⋊[φ] G),
  SemidirectProduct.inl x.left * SemidirectProduct.inr x.right = x
-- Init.Data.List.Lemmas
List.mem_ite_nil_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {l : List α}, (x ∈ if p then l else []) ↔ p ∧ x ∈ l
-- Mathlib.RingTheory.SimpleModule.Basic
isSimpleModule_iff_isAtom : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M},
  IsSimpleModule R ↥m ↔ IsAtom m
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₁_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.toCycles A 2 1) (groupHomology.isoCycles₁ A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom
      (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.f'
-- Init.Data.String.Defs
String.ofList.eq_1 : ∀ (data : List Char), String.ofList data = { toByteArray := data.utf8Encode, isValidUTF8 := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.arrow_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] (j : J),
  CategoryTheory.CategoryStruct.comp (arrows j) (CategoryTheory.Limits.WidePushout.ι arrows j) =
    CategoryTheory.Limits.WidePushout.head arrows
-- Mathlib.RingTheory.PrincipalIdealDomain
PrincipalIdealRing.factors_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] (a : R),
  a ≠ 0 → (∀ b ∈ PrincipalIdealRing.factors a, Irreducible b) ∧ Associated (PrincipalIdealRing.factors a).prod a
-- Batteries.Data.BitVec.Lemmas
BitVec.toFin_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnBE f).toFin = Fin.ofBits (f ∘ Fin.rev)
-- Lean.Data.KVMap
Lean.KVMap.Value.ofDataValue? : {α : Type} → [self : Lean.KVMap.Value α] → Lean.DataValue → Option α