mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X_i)_{i \in \iota}$ are jointly Gaussian, then they are independent if for all $i \ne j$,
$\mathrm{Cov}(X_i, X_j) = 0$.  -/
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {X : ι → Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P →
    (∀ (i j : ι), i ≠ j → ProbabilityTheory.covariance (X i) (X j) P = 0) → ProbabilityTheory.iIndepFun X P
-- Mathlib.RingTheory.AdicCompletion.Topology
/-- `IsHausdorff I R` is equivalent to being Hausdorff in the adic topology.  -/
IsAdic.isHausdorff_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] {I : Ideal R},
  IsAdic I → (IsHausdorff I R ↔ T2Space R)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowRight_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  (sq : f₂ ⟶ f₂'),
  (sq₁₂.mapArrowRight sq₁₂' sq).left =
    ⋯.desc (CategoryTheory.CategoryStruct.comp ((F.obj f₁.right).map (CategoryTheory.Arrow.Hom.left sq)) sq₁₂'.inl)
      (CategoryTheory.CategoryStruct.comp ((F.obj f₁.left).map (CategoryTheory.Arrow.Hom.right sq)) sq₁₂'.inr) ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYonedaEquiv_symm_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (X : C) (x : ↑(M.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom ((PresheafOfModules.freeYonedaEquiv.symm x).app (Opposite.op X)))
      (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))) =
    x
-- Mathlib.Logic.Encodable.Basic
Directed.sequence_mono_nat : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r : β → β → Prop} {f : α → β}
  (hf : Directed r f) (n : ℕ), r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Construct a isomorphism between parallel pairs.  -/
CategoryTheory.Limits.parallelPairIso : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X' Y' : C} →
        (f g : X ⟶ Y) →
          (f' g' : X' ⟶ Y') →
            (p : X ≅ X') →
              (q : Y ≅ Y') →
                CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f' →
                  CategoryTheory.CategoryStruct.comp g q.hom = CategoryTheory.CategoryStruct.comp p.hom g' →
                    (CategoryTheory.Limits.parallelPair f g ≅ CategoryTheory.Limits.parallelPair f' g')
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_continuous_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X}, Continuous (⇑h ∘ f) ↔ Continuous f
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_chartAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → writtenInExtChartAt I I x (↑(chartAt H x)) y = y
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  {X : CategoryTheory.SimplicialObject A}, CategoryTheory.Mono (AlgebraicTopology.inclusionOfMooreComplexMap X)
-- Mathlib.Analysis.Normed.Algebra.Exponential
Commute.exp_right : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸] {x y : 𝔸},
  Commute x y → Commute x (NormedSpace.exp y)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_cons_cons' : ∀ {G : Type u_7} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (a b : G) (l : List G),
  (a :: b :: l).alternatingSum = a + -b + l.alternatingSum
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_left_inj : ∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit a → (b + a = c + a ↔ b = c)
-- Batteries.Data.List.Lemmas
List.extractP.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (l a : List α) (a_1 : Array α),
  List.extractP.go p l a a_1 =
    match a, a_1 with
    | [], x => (none, l)
    | a :: l_1, acc => bif p a then (some a, acc.toListAppend l_1) else List.extractP.go p l l_1 (acc.push a)
-- Init.Data.List.Attach
List.getElem?_unattach : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} (i : ℕ), l.unattach[i]? = Option.map Subtype.val l[i]?
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a))
  (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.filterMap f t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k v l r, hl =>
      match f k v with
      | none =>
        match Std.DTreeMap.Internal.Impl.filterMap f l ⋯ with
        | { impl := l', balanced_impl := hl' } =>
          match Std.DTreeMap.Internal.Impl.filterMap f r ⋯ with
          | { impl := r', balanced_impl := hr' } => { impl := (l'.link2 r' ⋯ ⋯).impl, balanced_impl := ⋯ }
      | some v' =>
        match Std.DTreeMap.Internal.Impl.filterMap f l ⋯ with
        | { impl := l', balanced_impl := hl' } =>
          match Std.DTreeMap.Internal.Impl.filterMap f r ⋯ with
          | { impl := r', balanced_impl := hr' } =>
            { impl := (Std.DTreeMap.Internal.Impl.link k v' l' r' ⋯ ⋯).impl, balanced_impl := ⋯ }
-- Aesop.RuleSet
Aesop.instInhabitedBaseRuleSet : Inhabited Aesop.BaseRuleSet
-- Mathlib.Order.ModularLattice
sup_inf_assoc_of_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z = x ⊔ y ⊓ z
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The simple reflection of the Coxeter group `M.Group` at the index `i`.  -/
CoxeterMatrix.simple : {B : Type u_1} → (M : CoxeterMatrix B) → B → M.Group
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_neg_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R (-1) = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
            k ∈ l → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey! k' = k
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_sSup_apply : ∀ {E : Type u_3} [inst : Group E] {s : Set (GroupSeminorm E)}, BddAbove s → ∀ {x : E}, (sSup s) x = ⨆ p, ↑p x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_right_monotone : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α}, 1 ∈ s → Monotone fun x => s ^ x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `X` represents a presheaf of additive monoids `F`, then `Hom(-, X)` is isomorphic
to `F` as a presheaf of additive monoids.  -/
CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) →
          (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X) → CategoryTheory.yonedaAddMonObj X ≅ F
-- Mathlib.Topology.MetricSpace.Closeds
/-- The edistance to a closed set depends continuously on the point and the set  -/
TopologicalSpace.Closeds.continuous_infEDist : ∀ {α : Type u_1} [inst : EMetricSpace α], Continuous fun p => Metric.infEDist p.1 ↑p.2
-- Mathlib.Data.Ineq
Mathlib.Ineq.eq.sizeOf_spec : sizeOf Mathlib.Ineq.eq = 1
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_sub : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X Y : LeftInvariantDerivation I G), ⇑(X - Y) = ⇑X - ⇑Y
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.Bicategory.rightUnitor (F.map f) ≪≫ (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm
-- Mathlib.Algebra.Group.Finsupp
Finsupp.uniqueAddEquiv_symm_apply_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (i : ι) [inst_1 : Subsingleton ι] (m : M) (j : ι),
  ((Finsupp.uniqueAddEquiv i).symm m) j = m
-- Lean.Meta.Tactic.Grind.Types
/-- Number of delayed theorem instances generated so far. We track them to decide whether E-match made progress or not.  -/
Lean.Meta.Grind.EMatch.State.numDelayedInstances : Lean.Meta.Grind.EMatch.State → ℕ
-- Mathlib.Algebra.Polynomial.CoeffMem
_private.Mathlib.Algebra.Polynomial.CoeffMem.0.Polynomial.«termSpanCoeffs(_)» : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux_adjointAux : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F),
  ContinuousLinearMap.adjointAux✝ (ContinuousLinearMap.adjointAux✝ A) = A
-- Init.Data.SInt.Bitwise
ISize.not_eq_comm : ∀ {a b : ISize}, ~~~a = b ↔ a = ~~~b
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.mk : Lean.Name → Aesop.BuilderName → Aesop.PhaseName → Aesop.ScopeName → String → Aesop.RuleName.Json✝
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M) (m : M),
  (j.endHom f) (α m) = α (f m)
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → PartialOrder (FrameHom α β)
-- Init.Data.SInt.Bitwise
ISize.shiftRight_and : ∀ {a b c : ISize}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {s : V}
  (h : G.IsTuranMaximal r) [inst_2 : DecidableEq V], G.degree s = Fintype.card V - (h.finpartition.part s).card
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivAt.csinh : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasDerivAt f f' x → HasDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Raw.Const.maxEntryD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α × β → α × β
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜),
  DifferentiableWithinAt 𝕜 (fun x => Polynomial.eval x p) s x
-- Mathlib.SetTheory.Cardinal.Basic
Infinite.of_cardinalMk_le : ∀ {α β : Type u} [Infinite α], Cardinal.mk α ≤ Cardinal.mk β → Infinite β
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.ContainsPendingMVar.M : Type → Type
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isAddQuotientCoveringMap_coe : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜]
  [DiscreteTopology ↥(AddSubgroup.zmultiples p)],
  IsAddQuotientCoveringMap QuotientAddGroup.mk ↥(AddSubgroup.zmultiples p)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Reachable.coe_coeSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph) {u v : ↑G''.verts},
  G''.coe.Reachable u v →
    (SimpleGraph.Subgraph.coeSubgraph G'').coe.Reachable ((SimpleGraph.Subgraph.coeSubgraph G'').vert ↑↑u ⋯)
      ((SimpleGraph.Subgraph.coeSubgraph G'').vert ↑↑v ⋯)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_self_pow_mul : ∀ (n k : ℕ) {p : ℕ}, Nat.Prime p → p ^ k * n / p ^ (p ^ k * n).factorization p = n / p ^ n.factorization p
-- Init.Data.Float.Model.Unpacked.Round
/-- Shift the mantissa right by one, propagating information into the residual bits
as required.
 -/
Float.Model.UnpackedFloat.ExtendedMantissa.shiftRightOne : Float.Model.UnpackedFloat.ExtendedMantissa → Float.Model.UnpackedFloat.ExtendedMantissa
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.conjMap_ofFixingSubgroup_coe_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M} {hg : g • t = s}
  (x : ↥(SubMulAction.ofFixingSubgroup M t)), ↑((SubMulAction.conjMap_ofFixingSubgroup hg) x) = g • ↑x
-- Mathlib.Topology.Semicontinuity.Basic
upperSemiContinuous_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuous (-f) ↔ LowerSemicontinuous f
-- Std.Data.HashMap.Raw
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.HashMap.Raw.forM : {α : Type u} →
  {β : Type v} → {m : Type w → Type w'} → [Monad m] → (α → β → m PUnit.{w + 1}) → Std.HashMap.Raw α β → m PUnit.{w + 1}
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_le_one : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X),
  ∑ᶠ (i : ι), (f i) x ≤ 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool),
  Std.DTreeMap.Internal.Impl.filter! f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.fst_fst_mem : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G}, IsCorner A x₁ y₁ x₂ y₂ → (x₁, y₁) ∈ A
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_num_eq_h : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.nums 0 = g.h
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.aleph0_le_cof_iff : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 ≤ o.cof ↔ 1 < o.cof
-- Mathlib.Topology.ContinuousOn
continuousOn_iff_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.rightTriple_adj₁ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.rightTriple.adj₁ = q.adj₂
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.base : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ}, ∀ s ∈ S, M.εClosure S s
-- Mathlib.Analysis.Normed.Algebra.Ultra
/-- Let `K` be a normed field. If a normed division ring `L` is a normed `K`-algebra,
then `L` is ultrametric (i.e. the norm on `L` is nonarchimedean) if and only if `K` is.
 -/
IsUltrametricDist.normedAlgebra_iff : ∀ (K : Type u_1) (L : Type u_2) [inst : NormedField K] [inst_1 : NormedDivisionRing L] [NormedAlgebra K L],
  IsUltrametricDist L ↔ IsUltrametricDist K
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sSup_image_lieSpan_singleton : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M),
  sSup ((fun x => LieSubmodule.lieSpan R L {x}) '' ↑N) = N
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves colimits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesLimitsOfShape J F.leftOp
-- Mathlib.Analysis.Calculus.Deriv.Inv
/-- Eta-expanded form of `DifferentiableOn.div` -/
DifferentiableOn.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 d s → (∀ x ∈ s, d x ≠ 0) → DifferentiableOn 𝕜 (fun i => c i / d i) s
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_one : ∀ (n : ℕ), BitVec.ofNat 1 n = BitVec.ofBool (decide (n % 2 = 1))
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `s` is σ-compact and `f` is continuous on `s`, `f(s)` is σ-compact.  -/
IsSigmaCompact.image_of_continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsSigmaCompact s → ContinuousOn f s → IsSigmaCompact (f '' s)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_top : ExpGrowth.expGrowthSup ⊤ = ⊤
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_rpow_eq_tsum : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ (f : ↥(lp E p)), ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.mapEnd_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) (a : X ⟶ X),
  (CategoryTheory.Functor.mapEnd X f) a = f.map a
-- Mathlib.Order.Partition.Basic
Partition.Rel.left_mem : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, P.Rel x y → x ∈ u
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instMax.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instMax = { max := fun s t => { carrier := ↑s ∪ ↑t, smul_mem' := ⋯ } }
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.map_proj_nhds : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z},
  x ∈ e.source → Filter.map proj (nhds x) = nhds (proj x)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.zero_eq' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → ∀ {x : E}, x ∈ s → p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitAux_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (η : CategoryTheory.Over A),
  (CategoryTheory.OverPresheafAux.unitAux η).hom.left = (CategoryTheory.OverPresheafAux.unitAuxAux η.hom).hom
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.const_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} {t : N → ↑unitInterval}, GenLoop.const t = x
-- Mathlib.Algebra.Order.Ring.Synonym
toDual_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), OrderDual.toDual ↑n = ↑n
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_undef : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  ¬MeasureTheory.Integrable f μ → MeasureTheory.setToFun μ T hT f = 0
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (before : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α)
  (val : α) (node : Batteries.BinomialHeap.Imp.HeapNode α) (next : Batteries.BinomialHeap.Imp.Heap α),
  sizeOf { before := before, val := val, node := node, next := next } = 1 + sizeOf val + sizeOf node + sizeOf next
-- Mathlib.Order.Atoms
IsAtomic.Set.Iic.isAtomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomic α] {x : α}, IsAtomic ↑(Set.Iic x)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given two representable morphisms `f' : F.obj b ⟶ Y` and `g : F.obj a ⟶ Y`, we
obtain an isomorphism `hf'.pullback g ⟶ hg.pullback f'`.  -/
CategoryTheory.Functor.relativelyRepresentable.symmetry : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            {b : C} →
              {f' : F.obj b ⟶ Y} →
                (hf' : F.relativelyRepresentable f') →
                  {a : C} →
                    {g : F.obj a ⟶ Y} → (hg : F.relativelyRepresentable g) → [F.Full] → hf'.pullback g ⟶ hg.pullback f'
-- Mathlib.Topology.Order
eq_bot_of_singletons_open : ∀ {α : Type u_1} {t : TopologicalSpace α}, (∀ (x : α), IsOpen {x}) → t = ⊥
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_3 : ∀ (k : ℕ),
  Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.succ = fun n => do
    guard (n ≤ k)
    pure n.succ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The `L^p` norm of a Schwartz function is finite.  -/
SchwartzMap.eLpNorm_lt_top : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E] (f : SchwartzMap E F) (p : ENNReal)
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.eLpNorm_lt_top._auto_1) [hμ : μ.HasTemperateGrowth],
  MeasureTheory.eLpNorm (⇑f) p μ < ⊤
-- Lean.CoreM
Lean.Core.SavedState.mk.injEq : ∀ (toState : Lean.Core.State) (passedHeartbeats : ℕ) (toState_1 : Lean.Core.State) (passedHeartbeats_1 : ℕ),
  ({ toState := toState, passedHeartbeats := passedHeartbeats } =
      { toState := toState_1, passedHeartbeats := passedHeartbeats_1 }) =
    (toState = toState_1 ∧ passedHeartbeats = passedHeartbeats_1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_neg_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool