mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instIsCentralScalar : ∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_6 : DistribSMul S M₂] [inst_7 : SMulCommClass R₂ S M₂]
  [inst_8 : DistribSMul Sᵐᵒᵖ M₂] [inst_9 : SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂],
  IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_sub_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E), Metric.ball 0 δ - s = Metric.thickening δ (-s)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₂ = T.obj₂
-- Mathlib.Order.Hom.PowersetCard
/-- The isomorphism of `OrderEmbedding`s from `Fin n` into `I` with `Set.powersetCard I n`
when `I` is linearly ordered.  -/
Set.powersetCard.ofFinEmbEquiv : {n : ℕ} → {I : Type u_1} → [inst : LinearOrder I] → Fin n ↪o I ≃ ↑(Set.powersetCard I n)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.isBoundedLinearMap_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → ∀ (y : F), IsBoundedLinearMap 𝕜 fun x => f (x, y)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
isAlgebraic_iff_exists_isTranscendenceBasis_subset : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [IsDomain A]
  [FaithfulSMul R A] {s : Set A},
  Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
-- Mathlib.RingTheory.Nilpotent.Exp
/-- The exponential map on algebras, defined in analogy with the usual exponential series.
It provides meaningful (non-junk) values for nilpotent elements.  -/
IsNilpotent.exp : {A : Type u_1} → [inst : Ring A] → [Module ℚ A] → A → A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app CategoryTheory.Limits.WalkingCospan.right = snd
-- Mathlib.RingTheory.WittVector.IsPoly
_private.Mathlib.RingTheory.WittVector.IsPoly.0.WittVector.Tactic.runIntro : Lean.Syntax → Lean.Name → Lean.Elab.Tactic.TacticM Lean.FVarId
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_id : ∀ {G : Type u_2} [inst : AddCommGroup G] (S : AddSubmonoid G), S.IsLocalizationMap id
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.Presheaf.isSheaf_functorEnrichedHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.MonoidalClosed A] (F G : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J G →
    ∀ [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G],
      CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
integralClosure.isIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (x : ↥(integralClosure R A)), IsIntegral R x
-- Mathlib.Algebra.Group.Nat.Hom
/-- If `M` is commutative, `multiplesHom` is an additive equivalence.  -/
multiplesAddHom : (M : Type u_1) → [inst : AddCommMonoid M] → M ≃+ (ℕ →+ M)
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_rightUnitor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c}
  (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf),
  CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.rightUnitor f) ≪≫ η_f =
    Mathlib.Tactic.Bicategory.normalizeIsoComp η_f (CategoryTheory.Bicategory.rightUnitor pf)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.mk.sizeOf_spec : ∀ (id structId : ℕ) (type : Lean.Expr) (u : Lean.Level) (natModuleInst : Lean.Expr)
  (leInst? ltInst? lawfulOrderLTInst? isPreorderInst? orderedAddInst? isLinearInst? addRightCancelInst? :
    Option Lean.Expr)
  (rfl_q zero toQFn addFn smulFn : Lean.Expr) (termMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)),
  sizeOf
      { id := id, structId := structId, type := type, u := u, natModuleInst := natModuleInst, leInst? := leInst?,
        ltInst? := ltInst?, lawfulOrderLTInst? := lawfulOrderLTInst?, isPreorderInst? := isPreorderInst?,
        orderedAddInst? := orderedAddInst?, isLinearInst? := isLinearInst?, addRightCancelInst? := addRightCancelInst?,
        rfl_q := rfl_q, zero := zero, toQFn := toQFn, addFn := addFn, smulFn := smulFn, termMap := termMap } =
    1 + sizeOf id + sizeOf structId + sizeOf type + sizeOf u + sizeOf natModuleInst + sizeOf leInst? + sizeOf ltInst? +
                          sizeOf lawfulOrderLTInst? +
                        sizeOf isPreorderInst? +
                      sizeOf orderedAddInst? +
                    sizeOf isLinearInst? +
                  sizeOf addRightCancelInst? +
                sizeOf rfl_q +
              sizeOf zero +
            sizeOf toQFn +
          sizeOf addFn +
        sizeOf smulFn +
      sizeOf termMap
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A meromorphic function has only removable singularities if and only if the logarithmic counting
function for its pole divisor is asymptotically bounded.
 -/
ValueDistribution.logCounting_isBigO_one_iff_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  Meromorphic f →
    (ValueDistribution.logCounting f ⊤ =O[Filter.atTop] 1 ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f Set.univ) Set.univ)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_addMonoidHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective AddMonoidHomClass.toAddMonoidHom
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLED_eq_getD_getEntryLE? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.getEntryLED k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).getD fallback
-- Init.Data.SInt.Bitwise
Int16.toBitVec_shiftRight : ∀ (a b : Int16), (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 16)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Weierstrass `℘` function. This has the notation `℘[L]` in the namespace `PeriodPairs`.  -/
PeriodPair.weierstrassP : PeriodPair → ℂ → ℂ
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instTopologicalSpace.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  DomAddAct.instTopologicalSpace = TopologicalSpace.induced (⇑DomAddAct.mk.symm) inst
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestFirstTac : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- Any presheaf is a sheaf for the bottom (trivial) Grothendieck topology.  -/
CategoryTheory.Presieve.isSheaf_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presieve.IsSheaf ⊥ P
-- Mathlib.Order.WithBot
WithBot.map₂_bot_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithBot α), WithBot.map₂ f a ⊥ = ⊥
-- Mathlib.Tactic.CategoryTheory.Bicategory.Basic
/-- Normalize the both sides of an equality.  -/
Mathlib.Tactic.Bicategory.bicategoryNf : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Batteries.Data.AssocList
Batteries.AssocList.findEntryP?.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.findEntryP? p (Batteries.AssocList.cons a b es) =
    bif p a b then some (a, b) else Batteries.AssocList.findEntryP? p es
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_isDescendingCentralSeries`.

---

The lower central series of a group is a descending central series.  -/
lowerCentralSeries_isDescendingCentralSeries : ∀ {G : Type u_1} [inst : Group G], Subgroup.IsDescendingCentralSeries ⊤.lowerCentralSeries
-- Mathlib.Algebra.Ring.Parity
Nat.odd_add : ∀ {m n : ℕ}, Odd (m + n) ↔ (Odd m ↔ Even n)
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- The jump of `variationOnFromTo` on the right of a point is given by the distance between the
right limit and the value of the function.  -/
variationOnFromTo.tendsto_right : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {E : Type u_3} [inst_1 : PseudoMetricSpace E]
  [inst_2 : TopologicalSpace α] [OrderTopology α] {f : α → E} {l : E} {a b : α},
  a ∈ s →
    b ∈ s →
      LocallyBoundedVariationOn f s →
        Filter.Tendsto f (nhdsWithin b (s ∩ Set.Ioi b)) (nhds l) →
          Filter.Tendsto (variationOnFromTo f s a) (nhdsWithin b (s ∩ Set.Ioi b))
            (nhds (variationOnFromTo f s a b + dist (f b) l))
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- `ErdosStone.filter` is the set of vertices in the complement of a complete equipartite
subgraph, in `r` parts each of size `t'`, adjacent to at least `t` vertices in each part of the
complete equipartite subgraph.

This is an auxiliary definition for the Erdős-Stone theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter : {n : ℕ} →
  {G : SimpleGraph (Fin n)} →
    [DecidableRel G.Adj] → {r t' : ℕ} → G.CompleteEquipartiteSubgraph r t' → ℕ → Finset (Fin n)
-- Lean.Hygiene
Lean.Unhygienic.Context : Type
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Day.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toDays : Std.Time.WallTime → Std.Time.Day.Offset
-- Mathlib.Order.Filter.IndicatorFunction
indicator_biUnion_finset_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Zero β] (s : ι → Set α) (f : α → β) (a : α),
  (fun n => (⋃ i ∈ n, s i).indicator f a) =ᶠ[Filter.atTop] fun x => (Set.iUnion s).indicator f a
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of `sdiff_sup_self`. -/
sup_sdiff_self_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ a ⊔ a = b ⊔ a
-- Mathlib.GroupTheory.Exponent
AddMonoid.lcm_addOrderOf_eq_exponent : ∀ {G : Type u} [inst : AddMonoid G] [inst_1 : Fintype G], Finset.univ.lcm addOrderOf = AddMonoid.exponent G
-- Mathlib.Data.Set.Basic
Set.ofPred_injective : ∀ {α : Type u}, Function.Injective Set.ofPred
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addLeft.eq_1 : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G] (c : G),
  IsometryEquiv.addLeft c = { toEquiv := Equiv.addLeft c, isometry_toFun := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_of_append_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u}, ¬p.Nil → (p.append q).IsCycle → q.IsPath
-- Mathlib.Order.Filter.Tendsto
Filter.map_inf_principal_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} {l : Filter α},
  Filter.map f (l ⊓ Filter.principal (f ⁻¹' s)) = Filter.map f l ⊓ Filter.principal s
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.sup : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Lattice E] [ContinuousSup E] [HasSolidNorm E]
  [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {f g : ι → Ω → E},
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Submartingale g ℱ μ → MeasureTheory.Submartingale (f ⊔ g) ℱ μ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.le' : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δ → α},
  Measurable f → Measurable g → Measurable fun a => f a ≤ g a
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.forget₂_addCommMonCat_map : ∀ {R S : SemiRingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.MapSubtype.orderIso_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (H' : AddSubgroup ↥H),
  ↑((AddSubgroup.MapSubtype.orderIso H) H') = AddSubgroup.map H.subtype H'
-- Mathlib.Algebra.Module.Equiv.Defs
LinearMap.inverse.congr_simp : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (f f_1 : M →ₛₗ[σ] M₂) (e_f : f = f_1) (g g_1 : M₂ → M) (e_g : g = g_1)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = f_1.inverse g_1 ⋯ ⋯
-- Init.Data.SInt.Lemmas
ISize.ofInt_eq_iff_bmod_eq_toInt : ∀ (a : ℤ) (b : ISize), ISize.ofInt a = b ↔ a.bmod (2 ^ System.Platform.numBits) = b.toInt
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : (CategoryTheory.FunctorToTypes.prod F G).obj a),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a)) z) =
    z.1
-- Mathlib.Data.Set.FiniteExhaustion
/-- **Alias** of `Set.nonempty_finiteExhaustion_iff`. -/
Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iff : ∀ {α : Type u_1} {s : Set α}, Nonempty s.FiniteExhaustion ↔ s.Countable
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- An `𝓞_Spec R` module `M` is isomorphic to `Γ(M)^~` if and only if it is localizing
as a sheaf of `R` modules  -/
AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules),
  CategoryTheory.IsIso M.fromTildeΓ ↔ AlgebraicGeometry.IsLocalizing (AlgebraicGeometry.modulesSpecToSheaf.obj M)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_lt_norm_lt : ∀ (α : Type u_2) [inst : DenselyNormedField α] {r₁ r₂ : ℝ}, 0 ≤ r₁ → r₁ < r₂ → ∃ x, r₁ < ‖x‖ ∧ ‖x‖ < r₂
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashSet.emptyWithCapacity c).size = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.map_obj : ∀ {S T : SSet.Truncated 2} (f : S ⟶ T) (x : SSet.OneTruncation₂ S),
  (SSet.OneTruncation₂.map f).obj x =
    (CategoryTheory.ConcreteCategory.hom
        (f.app (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })))
      x
-- Init.Data.SInt.Lemmas
Int64.neg_sub : ∀ {a b : Int64}, -(a - b) = b - a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_insert : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] [inst_2 : TopologicalSpace α] {x : α}
  {s : Set α} {C : ℝ} {g : α → E} {g' : α → F},
  ‖g x‖ ≤ C * ‖g' x‖ →
    (Asymptotics.IsBigOWith C (nhdsWithin x (insert x s)) g g' ↔ Asymptotics.IsBigOWith C (nhdsWithin x s) g g')
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
MeasureTheory.lintegral_rnDeriv_compProd : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
    ∀ᵐ (a : 𝓧) ∂μ, ∫⁻ (b : 𝓨), (μ.compProd κ).rnDeriv (μ.compProd η) (a, b) ∂η a = (κ a) Set.univ
-- Mathlib.Order.Filter.Pi
Filter.pi_mem_pi_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), (f i).NeBot]
  {I : Set ι}, I.Finite → (I.pi s ∈ Filter.pi f ↔ ∀ i ∈ I, s i ∈ f i)
-- Mathlib.Order.WithBot
WithBot.instOrderBot : {α : Type u_1} → [inst : LE α] → OrderBot (WithBot α)
-- Init.Data.Option.Lemmas
Option.join_filter : ∀ {α : Type u_1} {p : Option α → Bool} {o : Option (Option α)},
  (Option.filter p o).join = Option.filter (fun a => p (some a)) o.join
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.foldrM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeMap.Raw.foldrM f init t₁ = Std.TreeMap.Raw.foldrM f init t₂
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_inter : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : Subtype MeasurableSet), ↑(s ∩ t) = ↑s ∩ ↑t
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `n`-th root of
unity and `K` is an `n`-th cyclotomic extension of `ℚ`.  -/
IsPrimitiveRoot.adjoinEquivRingOfIntegers : {n : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [NeZero n] →
          [inst_2 : CharZero K] →
            [IsCyclotomicExtension {n} ℚ K] → IsPrimitiveRoot ζ n → ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α}, N.IsRestriction M → (N.Indep I ↔ M.Indep I ∧ I ⊆ N.E)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_inter : ∀ {x y z : ZFSet.{u}}, z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y
-- Mathlib.Data.List.Sort
List.sortedLE_insertionSort : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α], (List.insertionSort (fun x1 x2 => x1 ≤ x2) l).SortedLE
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyLE?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky v l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyLE?.go k best l
      | Ordering.eq => some ky
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLE?.go k (some ky) r
-- Mathlib.RingTheory.Perfection
Tilt.instField : (K : Type u₁) →
  [inst : Field K] →
    (v : Valuation K NNReal) →
      (O : Type u₂) →
        [inst_1 : CommRing O] →
          [inst_2 : Algebra O K] →
            (hv : v.Integers O) →
              (p : ℕ) → [inst_3 : Fact (Nat.Prime p)] → [hvp : Fact (v ↑p ≠ 1)] → Field (Tilt K v O hv p)
-- Mathlib.Order.BoundedOrder.Basic
Pi.instOrderBot.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → LE (α' i)] [inst_1 : (i : ι) → OrderBot (α' i)],
  Pi.instOrderBot = { toBot := Pi.instBotForall, bot_le := ⋯ }
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version at a point.  -/
MDifferentiableAt.mpullback_vectorField : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} [inst_11 : IsManifold I 2 M] [inst_12 : IsManifold I' 2 M']
  [CompleteSpace E],
  MDiffAt (T% V) (f x₀) →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible → 2 ≤ n → (MDiffAt fun x => ⟨x, VectorField.mpullback I I' f V x⟩) x₀
-- Mathlib.Topology.Homotopy.Lifting
/-- If `p : E → X` is a local homeomorphism, and if `g : I × A → E` is a lift of `f : C(I × A, X)`
continuous on `{0} × A ∪ I × {a}` for some `a : A`, then there exists a neighborhood `N ∈ 𝓝 a`
and `g' : I × A → E` continuous on `I × N` that agrees with `g` on `{0} × A ∪ I × {a}`.
The proof follows [hatcher02], Proof of Theorem 1.7, p.30.

Possible TODO: replace `I` by an arbitrary space assuming `A` is locally connected
and `p` is a separated map, which guarantees uniqueness and therefore well-definedness
on the intersections.  -/
IsLocalHomeomorph.exists_lift_nhds : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X},
  IsLocalHomeomorph p →
    ∀ {f : C(↑unitInterval × A, X)} {g : ↑unitInterval × A → E},
      p ∘ g = ⇑f →
        (Continuous fun x => g (0, x)) →
          ∀ (a : A),
            (Continuous fun x => g (x, a)) →
              ∃ N ∈ nhds a,
                ∃ g',
                  ContinuousOn g' (Set.univ ×ˢ N) ∧
                    p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : ↑unitInterval), g' (t, a) = g (t, a)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → Std.ExtDHashMap.Const.get? (m₁ \ m₂) k = none
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm_const_smul_le : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {𝕜 : Type u_3} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 F]
  [IsBoundedSMul 𝕜 F] {c : 𝕜}, MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm f p μ