mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift.tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ : MultilinearMap R s E} (f : (i : ι) → s i), (PiTensorProduct.lift φ) ((PiTensorProduct.tprod R) f) = φ f
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocks.eq_1 : ∀ {n : ℕ} (c : CompositionAsSet n), c.blocks = List.ofFn c.blocksFun
-- Init.Data.Ord.Basic
Ordering.ofNat_ctorIdx : ∀ (x : Ordering), Ordering.ofNat x.ctorIdx = x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Clopen subsets in the prime spectrum of a commutative ring are in 1-1 correspondence
with idempotent elements in the ring.  -/
PrimeSpectrum.isIdempotentElemEquivClopens : {R : Type u} → [inst : CommRing R] → { e // IsIdempotentElem e } ≃o TopologicalSpace.Clopens (PrimeSpectrum R)
-- Mathlib.Analysis.MeanInequalities
NNReal.summable_Lp_add : ∀ {ι : Type u} {f g : ι → NNReal} {p : ℝ},
  1 ≤ p → (Summable fun i => f i ^ p) → (Summable fun i => g i ^ p) → Summable fun i => (f i + g i) ^ p
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_right_iff_lt_one : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → ((AffineMap.lineMap a b) r < b ↔ r < 1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs.sizeOf_spec : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [inst_3 : SizeOf R] [inst_4 : SizeOf S] (ofAbs : R),
  sizeOf (WithAbs.toAbs v ofAbs) = 1 + sizeOf ofAbs
-- Mathlib.RingTheory.Valuation.Integers
Valuation.mem_ltIdeal_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀ˣ}
  {x : ↥v.integer}, x ∈ v.ltIdeal γ ↔ v ↑x < ↑γ
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_eq' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : N ≃+ P} (x : N),
  (f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k)) x = k x
-- Mathlib.Probability.Independence.Conditional
/-- Two measurable space structures (or σ-algebras) `m₁, m₂` are conditionally independent given
`m'` with respect to a measure `μ` (defined on a third σ-algebra) if for any sets
`t₁ ∈ m₁, t₂ ∈ m₂`, `μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧`.
See `ProbabilityTheory.condIndep_iff`.  -/
ProbabilityTheory.CondIndep : {Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    MeasurableSpace Ω →
      MeasurableSpace Ω →
        {mΩ : MeasurableSpace Ω} →
          [StandardBorelSpace Ω] →
            m' ≤ mΩ →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndep._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.Algebra.GCDMonoid.Basic
Associated.gcd_eq_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {m n : α},
  Associated m n → ∀ (k : α), gcd m k = gcd n k
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.tendsto_rpow_atBot_of_one_lt_base : ∀ {b : ENNReal}, 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atBot (nhds 0)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.mem_adjoin_of_mem : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A} {x : A},
  x ∈ s → x ∈ StarAlgebra.adjoin R s
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.image : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : Set ι},
  s.Pairwise (Function.onFun r f) → (f '' s).Pairwise r
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.functor.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C),
  CategoryTheory.Quotient.functor r =
    { obj := fun a => { as := a }, map := fun {X Y} f => Quot.mk (CategoryTheory.HomRel.CompClosure r) f, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natIso_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i)
  (i : CategoryTheory.Discrete I), (CategoryTheory.Discrete.natIso f).app i = f i
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.mk : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  p ∈ s₁ → p ∈ s₂ → Wbtw ℝ s₁.center p s₂.center → s₁.IsExtTangentAt s₂ p
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.mk.injEq : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] (toFun : Y → Z) (prop : Topology.ContinuousGeneratedBy X toFun)
  (toFun_1 : Y → Z) (prop_1 : Topology.ContinuousGeneratedBy X toFun_1),
  ({ toFun := toFun, prop := prop } = { toFun := toFun_1, prop := prop_1 }) = (toFun = toFun_1)
-- Init.Data.Ord.Basic
Ordering.not_isLT_eq_isGE : ∀ {o : Ordering}, (!o.isLT) = o.isGE
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_apply_coe : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] (f : Equiv.Perm (Subtype p)) (x : Subtype p),
  (Equiv.Perm.ofSubtype f) ↑x = ↑(f x)
-- Mathlib.Algebra.Group.Action.Prod
smulMonoidHom_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulOneClass β] [inst_2 : MulAction α β]
  [inst_3 : IsScalarTower α β β] [inst_4 : SMulCommClass α β β] (a : α × β), smulMonoidHom a = smulMulHom.toFun a
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_le_const : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  b ≤ c → ∀ {a : α}, 0 ≤ a → b * a ≤ c * a
-- Mathlib.Data.Finmap
Finmap.mk.inj : ∀ {α : Type u} {β : α → Type v} {entries : Multiset (Sigma β)} {nodupKeys : entries.NodupKeys}
  {entries_1 : Multiset (Sigma β)} {nodupKeys_1 : entries_1.NodupKeys},
  { entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 } →
    entries = entries_1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.isUnit_sqrt_iff_isStrictlyPositive : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  IsUnit (CFC.sqrt a) ↔ IsStrictlyPositive a
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivCodomain_symm_apply : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X),
  ↑((Equiv.subtypeEquivCodomain f).symm y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y
-- Mathlib.Topology.Maps.Strict.Group
/-- The product (in the sense of `MonoidHom.prodMap`) of strict group homomorphisms is strict.  -/
MonoidHom.isStrictMap_prodMap : ∀ {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [inst : Group G'] [inst_1 : Group H'] [inst_2 : Group G]
  [inst_3 : Group H] {f : G →* H} {g : G' →* H'} [inst_4 : TopologicalSpace G] [inst_5 : TopologicalSpace H]
  [IsTopologicalGroup G] [inst_7 : TopologicalSpace G'] [IsTopologicalGroup G'] [inst_9 : TopologicalSpace H'],
  Topology.IsStrictMap ⇑f → Topology.IsStrictMap ⇑g → Topology.IsStrictMap ⇑(f.prodMap g)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_withDensity_right`.  -/
MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {ν : MeasureTheory.Measure α}
  [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    AEMeasurable f ν →
      (∀ᵐ (x : α) ∂ν, f x ≠ 0) →
        (∀ᵐ (x : α) ∂ν, f x ≠ ⊤) → μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.move a q → motive (Turing.TM1.Stmt.move a q))
  (h_2 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Γ) →
        (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.write a q → motive (Turing.TM1.Stmt.write a q))
  (h_3 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.load a q → motive (Turing.TM1.Stmt.load a q))
  (h_4 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Bool) →
        (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.branch a q₁ q₂ → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (Q : Turing.TM1.Stmt Γ Λ σ) → motive Q),
  (match Turing.TM1.Stmt.move a q with
    | Q@h:(Turing.TM1.Stmt.move a q) => h_1 Q a q h
    | Q@h:(Turing.TM1.Stmt.write a q) => h_2 Q a q h
    | Q@h:(Turing.TM1.Stmt.load a q) => h_3 Q a q h
    | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => h_4 Q a q₁ q₂ h
    | Q => h_5 Q) =
    h_1 (Turing.TM1.Stmt.move a q) a q ⋯
-- Mathlib.Data.Nat.Factorial.Basic
/-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. ℕ-division isn't worth it.  -/
Nat.ascFactorial_eq_div : ∀ (n k : ℕ), (n + 1).ascFactorial k = (n + k).factorial / n.factorial
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.integrable_of_nnreal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure μ] [OpensMeasurableSpace X] (f : BoundedContinuousFunction X NNReal),
  MeasureTheory.Integrable (NNReal.toReal ∘ ⇑f) μ
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ GrpCat MonCat).Full
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.mem_closure_iff_bsup : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  a ∈ closure s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_closedEBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Entry.measure.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, Lean.PersistentHashMap.Entry.null.measure = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.ext_iff : ∀ {a b : SimplexCategory} {f g : a ⟶ b}, f = g ↔ SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.mk : {𝕜 : outParam (Type u_1)} →
  {H : Type u_2} →
    {X : outParam (Type u_3)} →
      {V : outParam (Type u_4)} →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup V] →
            [inst_2 : InnerProductSpace 𝕜 V] →
              [inst_3 : NormedAddCommGroup H] →
                [inst_4 : InnerProductSpace 𝕜 H] → (coeCLM : H →L[𝕜] X → V) → Function.Injective ⇑coeCLM → RKHS 𝕜 H X V
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.merge.eq_def : ∀ {α : Type u_1} (xs ys : List α) (le : α → α → Bool),
  xs.merge ys le =
    match xs, ys with
    | [], ys => ys
    | xs, [] => xs
    | x :: xs, y :: ys => if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_image : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {s : Set M} [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂),
  Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        (hom₁ : T₁.obj₁ ⟶ T₂.obj₁) →
          (hom₂ : T₁.obj₂ ⟶ T₂.obj₂) →
            (hom₃ : T₁.obj₃ ⟶ T₂.obj₃) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ T₂.mor₁)
                  CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ T₂.mor₂)
                    CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
                        CategoryTheory.CategoryStruct.comp hom₃ T₂.mor₃)
                      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam →
                    CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp_map : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q),
  LinearMap.rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_add_isBoundedUnder_ge : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l g →
    Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.map_top_submodule : ∀ (A : Type u_3) (E : Type u_4) {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E],
  Submodule.map ↑(WithCStarModule.linearEquiv R A E).symm ⊤ = ⊤
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_nil : ∀ {α : Type u_1} {p : α → Bool} {acc : List α}, List.splitOnPPrepend p [] acc = [acc.reverse]
-- Mathlib.SetTheory.Ordinal.Basic
/-- Galois coinsertion between `Cardinal.ord` and `Ordinal.card`.  -/
Cardinal.gciOrdCard : GaloisCoinsertion Cardinal.ord Ordinal.card
-- Init.Data.Array.Nat
Array.prod_append_nat : ∀ {as₁ as₂ : Array ℕ}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Mathlib.Data.Set.Insert
Set.singleton_subset_iff : ∀ {α : Type u_1} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (|t| * |X ω|)` is
integrable.  -/
ProbabilityTheory.integrable_exp_abs_mul_abs : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (|t| * |X ω|)) μ
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.mk : {M N : SemiNormedGrp₁} → (hom' : NormedAddGroupHom M.carrier N.carrier) → hom'.NormNoninc → M.Hom N
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.toMulHom_eq_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), f.toMulHom = ↑f
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_pow : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] (a : R) (n : ℕ), abv (a ^ n) = abv a ^ n
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H)
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖₊ = ‖x‖₊
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.keysArray → k ∈ t
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremsArray.addTheorem : Lean.Meta.SimpTheoremsArray →
  Lean.Meta.Origin →
    Lean.Expr → optParam Lean.Meta.ConfigWithKey Lean.Meta.simpGlobalConfig → Lean.MetaM Lean.Meta.SimpTheoremsArray
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iInter₂_iInter₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α}
  {t : (i : ι) → κ i → Set β} {f : α → β},
  (∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) → Set.MapsTo f (⋂ i, ⋂ j, s i j) (⋂ i, ⋂ j, t i j)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_2.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_3 t ×' Lean.Elab.Term.Do.Code.below_2 t
-- Init.Data.Option.Lemmas
Option.isSome_dite' : ∀ {β : Type u_1} {p : Prop} {x : Decidable p} {b : ¬p → β}, (if h : p then none else some (b h)).isSome = true ↔ ¬p
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_sub : ∀ {α : Type u_1} (f g : α → ℝ), Complex.ofReal ∘ (f - g) = Complex.ofReal ∘ f - Complex.ofReal ∘ g
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateSort!Impl : Lean.Expr → Lean.Level → Lean.Expr
-- Lean.Setup
/-- Files containing data for a single module.  -/
Lean.ModuleArtifacts : Type
-- Mathlib.Order.JordanHolder
JordanHolderLattice.lt_of_isMaximal : ∀ {X : Type u} {inst : Lattice X} [self : JordanHolderLattice X] {x y : X}, JordanHolderLattice.IsMaximal x y → x < y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.range_getVert_eq_range_support_getElem : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), Set.range p.getVert = Set.range p.support.get
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.mk.inj : ∀ {R : Type u} {inst : CommSemiring R} {M : Type u_1} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} {N : Type u_2}
  {inst_3 : AddCommMonoid N} {inst_4 : Module R N}
  {toFun' :
    (S : Type u) → [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N}
  {isCompat' :
    autoParam
      (∀ {S : Type u} [inst_5 : CommSemiring S] [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S']
        [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun' S = toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
      PolynomialLaw.isCompat'._autoParam}
  {toFun'_1 :
    (S : Type u) → [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N}
  {isCompat'_1 :
    autoParam
      (∀ {S : Type u} [inst_5 : CommSemiring S] [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S']
        [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun'_1 S = toFun'_1 S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
      PolynomialLaw.isCompat'._autoParam},
  { toFun' := toFun', isCompat' := isCompat' } = { toFun' := toFun'_1, isCompat' := isCompat'_1 } → toFun' = toFun'_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), LawfulBEq (β k)], (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Mathlib.Order.Lattice
LinearOrder.toLattice : {α : Type u} → [LinearOrder α] → Lattice α
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.exprArgs : Lean.Elab.Term.MutualClosure.ClosureState → Array Lean.Expr
-- Init.System.IO
/-- Opens the file at `fn` with the given `mode`.

An exception is thrown if the file cannot be opened.
 -/
IO.FS.Handle.mk : System.FilePath → IO.FS.Mode → IO IO.FS.Handle