mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_iff_exists_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ : P},
  p₁ ∈ s → (s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.preimage_units_mul_comm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a b : A),
  Units.val ⁻¹' spectrum R (a * b) = Units.val ⁻¹' spectrum R (b * a)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNormEssSup_piecewise : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f g : α → ε) [inst_2 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    MeasureTheory.eLpNormEssSup (s.piecewise f g) μ =
      max (MeasureTheory.eLpNormEssSup f (μ.restrict s)) (MeasureTheory.eLpNormEssSup g (μ.restrict sᶜ))
-- Mathlib.Analysis.Normed.Ring.Lemmas
Filter.comap_mul_right_cobounded : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [NormMulClass α] {a : α},
  a ≠ 0 → Filter.comap (fun x => x * a) (Bornology.cobounded α) = Bornology.cobounded α
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.symm_mapSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (e : G ≃* H),
  e.mapSubgroup.symm = e.symm.mapSubgroup
-- Mathlib.FieldTheory.Normal.Defs
/-- If `K₁/E/F` is a tower of fields with `E/F` normal then `AlgHom.restrictNormal'` is an
equivalence.  -/
Normal.algHomEquivAut : (F : Type u_1) →
  [inst : Field F] →
    (K₁ : Type u_3) →
      [inst_1 : Field K₁] →
        [inst_2 : Algebra F K₁] →
          (E : Type u_6) →
            [inst_3 : Field E] →
              [inst_4 : Algebra F E] →
                [inst_5 : Algebra E K₁] → [IsScalarTower F E K₁] → [Normal F E] → (E →ₐ[F] K₁) ≃ Gal(E/F)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i),
  HomologicalComplex.restrictionToTruncGE'.f K e i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (K.truncGE'XIso e hi' hi).inv
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one : ∀ {ε : ℝ}, 0 < ε → ∀ (x : ℝ), ε.mulExpNegMulSq x = (√ε)⁻¹ * Real.mulExpNegMulSq 1 (√ε * x)
-- Init.Data.Dyadic.Basic
Dyadic.toRat_pow : ∀ (x : Dyadic) (n : ℕ), (x ^ n).toRat = x.toRat ^ n
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_restrict_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {s : Set X},
  (μ.restrict s).variation ≤ μ.variation.restrict s
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The constant augmented cosimplicial object functor.  -/
CategoryTheory.CosimplicialObject.Augmented.const : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.CosimplicialObject.Augmented C)
-- Init.Data.UInt.Bitwise
UInt64.and_not_self : ∀ {a : UInt64}, a &&& ~~~a = 0
-- Mathlib.Data.List.MinMax
List.argmin_nil : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β), List.argmin f [] = none
-- Mathlib.Topology.Spectral.Hom
SpectralMap.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toFun : α → β) (spectral' : IsSpectralMap toFun),
  sizeOf { toFun := toFun, spectral' := spectral' } = 1 + sizeOf spectral'
-- Mathlib.Data.Finset.Fold
Finset.fold_insert : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {a : α} [inst : DecidableEq α],
  a ∉ s → Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [T1Space E] {y : E}, HasFDerivWithinAt f f' {x} y
-- Mathlib.Order.BoundedOrder.Basic
not_isMin_iff_bot_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, ¬IsMin a ↔ ⊥ < a
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.invariantCardinalRank_map : ∀ {α : Type u} {β : Type v} {f : α → β} (M : Matroid α) [M.InvariantCardinalRank] (hf : Set.InjOn f M.E),
  (M.map f hf).InvariantCardinalRank
-- Mathlib.Order.SuccPred.Basic
Order.Ici_subset_Ioi_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), Set.Ici a ⊆ Set.Ioi (Order.pred a)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Finsupp.weight.eq_1 : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], Finsupp.weight w = (Finsupp.linearCombination R w).toAddMonoidHom
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isAffine_of_isEmpty : ∀ {X : AlgebraicGeometry.Scheme} [IsEmpty ↥X], AlgebraicGeometry.IsAffine X
-- Mathlib.Data.ENat.Lattice
ENat.iSup_natCast_ne_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) ≠ ⊤ ↔ BddAbove (Set.range f)
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_lt_top : ∀ {a : ENNReal} {n : ℕ}, a < ⊤ → a ^ n < ⊤
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.mod_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Mod α] [Lean.Grind.ToInt.Mod α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a % b) = a' % b'
-- Mathlib.Analysis.Convex.Between
Wbtw.sameRay_vsub_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → SameRay R (z -ᵥ x) (z -ᵥ y)
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (projName : Lean.Name) (paramInfoOverrides : List (Option Lean.BinderInfo)),
  sizeOf { ref := ref, projName := projName, paramInfoOverrides := paramInfoOverrides } =
    1 + sizeOf ref + sizeOf projName + sizeOf paramInfoOverrides
-- Init.Data.List.Sublist
List.subset_reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ ⊆ l₂.reverse ↔ l₁ ⊆ l₂
-- Mathlib.Data.Finset.Sym
/-- Lifts a finset to `Sym α n`. `s.sym n` is the finset of all unordered tuples of cardinality `n`
with elements in `s`.  -/
Finset.sym : {α : Type u_1} → [DecidableEq α] → Finset α → (n : ℕ) → Finset (Sym α n)
-- Mathlib.Topology.Separation.Basic
Ne.nhdsWithin_compl_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, x ≠ y → nhdsWithin x {y}ᶜ = nhds x
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Vertical composition of lax transformations.  -/
CategoryTheory.Lax.LaxTrans.vComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          CategoryTheory.Lax.LaxTrans F G → CategoryTheory.Lax.LaxTrans G H → CategoryTheory.Lax.LaxTrans F H
-- Init.Data.Array.Bootstrap
Array.foldr_toList : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) {init : β} {xs : Array α},
  List.foldr f init xs.toList = Array.foldr f init xs
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.add : Nat.Internal.SOM.Expr → Nat.Internal.SOM.Expr → Nat.Internal.SOM.Expr
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_ext : ∀ {X Y : LinOrd} {f g : X ⟶ Y}, LinOrd.Hom.hom f = LinOrd.Hom.hom g → f = g
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.conjTranspose_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : StarRing R] (A : Matrix n' n' R) (n : ℤ), (A ^ n).conjTranspose = A.conjTranspose ^ n
-- Init.Data.SInt.Lemmas
Int64.zero_ne_one : 0 ≠ 1
-- Init.Data.UInt.Lemmas
USize.toUInt8_lt : ∀ {a b : USize}, a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.unop_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.LeftHomologyData), h.unop.Q = Opposite.unop h.K
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.ofHom_sub : ∀ {k : Type u} {G : Type v} {X Y : Type w} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] [inst_8 : AddCommGroup Y] [inst_9 : Module k Y] [inst_10 : TopologicalSpace Y]
  [inst_11 : IsTopologicalAddGroup Y] [inst_12 : ContinuousSMul k Y] {ρ : ContRepresentation k G X}
  {σ : ContRepresentation k G Y} (f g : ContIntertwiningMap ρ σ), TopRep.ofHom (f - g) = TopRep.ofHom f - TopRep.ofHom g
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.selfEquivSigmaOrbits'.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.selfEquivSigmaOrbits' G α =
    Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun x => Equiv.subtypeEquivRight ⋯)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.IsRightContinuous.eq : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {𝓕 : MeasureTheory.Filtration ι m}
  [h : 𝓕.IsRightContinuous], 𝓕.rightCont = 𝓕
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rco : ∀ {m n fallback : ℤ} {i : ℕ}, (m...n).toArray.getD i fallback = if i < (n - m).toNat then m + ↑i else fallback
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instIsCodirectedOrderElemOpensOpenRcNhdsOfT2Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] (K : TopologicalSpace.Compacts α),
  IsCodirectedOrder ↑K.openRcNhds
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sum_sin : ∀ (n : ℕ) {a : ℝ},
  (∀ (k : ℤ), a ≠ ↑k * (2 * Real.pi)) →
    ∀ (b : ℝ),
      ∑ i ∈ Finset.range n, Real.sin (a * ↑i + b) =
        Real.sin (↑n * a / 2) * Real.sin ((↑n - 1) * a / 2 + b) / Real.sin (a / 2)
-- Init.Data.SInt.Bitwise
Int16.toBitVec_not : ∀ {a : Int16}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M)
  (x : ↥M'), ↑((f.addSubmonoidMap M') x) = f ↑x
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleObjXIsoOfEq.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V) (i : ι) (hi : i = j), HomologicalComplex.singleObjXIsoOfEq c j A i hi = CategoryTheory.eqToIso ⋯
-- Batteries.Data.List.Basic
/-- Auxiliary for `takeListTR`: `takeListTR.go as as' acc = acc.toList ++ takeList as as'`.  -/
List.takeListTR.go : {α : Type u_1} → List ℕ → List α → Array (List α) → List (List α) × List α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ext_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.toList.Perm t₂.toList → t₁ = t₂
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone.inl φ =
    CochainComplex.HomComplex.Cochain.mk fun p q hpq => HomologicalComplex.homotopyCofiber.inlX φ p q ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
instAddCommMonoidDegLex : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid (DegLex α)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux.match_1.eq_2 : ∀ (motive : Option Char → Sort u_1) (cₙ : Char) (h_1 : Unit → motive none) (h_2 : (cₙ : Char) → motive (some cₙ)),
  (match some cₙ with
    | none => h_1 ()
    | some cₙ => h_2 cₙ) =
    h_2 cₙ
-- Mathlib.Data.PEquiv
PEquiv.ofSet_univ : ∀ {α : Type u}, PEquiv.ofSet Set.univ = PEquiv.refl α
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Span.repr_def : ∀ (R : Type u_4) {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (w : Set M)
  (x : ↥(Submodule.span R w)), Span.repr R w x = ⋯.choose
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- Every maximal ideal in a commutative complex Banach algebra gives rise to a character on that
algebra. In particular, the character, which may be identified as an algebra homomorphism due to
`WeakDual.CharacterSpace.equivAlgHom`, is given by the composition of the quotient map and
the Gelfand-Mazur isomorphism `NormedRing.algEquivComplexOfComplete`.  -/
Ideal.toCharacterSpace : {A : Type u_1} →
  [inst : NormedCommRing A] →
    [inst_1 : NormedAlgebra ℂ A] → [CompleteSpace A] → (I : Ideal A) → [I.IsMaximal] → ↑(WeakDual.characterSpace ℂ A)
-- Mathlib.Order.LatticeIntervals
Set.Ici.coe_bot : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑⊥ = a
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.zero_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι), HomologicalComplex.Hom.f 0 i = 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instDistribMulAction : {k : Type u_1} →
  {G : Type u_2} →
    {S : Type u_3} →
      [inst : Monoid S] → [inst_1 : AddMonoid k] → [DistribMulAction S k] → DistribMulAction S (SkewMonoidAlgebra k G)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.support_eq_verts : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph}, M.IsMatching → M.support = M.verts
-- Mathlib.Order.FixedPoints
fixedPoints.instBoundedOrderElemFixedPointsCoeOrderHom : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → BoundedOrder ↑(Function.fixedPoints ⇑f)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If a function f has a derivative f' at x, a rescaled version of f around x converges to f',
i.e., `n (f (x + (1/n) v) - f x)` converges to `f' v`. More generally, if `d n` tends to zero
and `c n * d n` tends to `v`, then `c n * (f (x + d n) - f x)` tends to `f' v`. This lemma expresses
this fact, for functions having a derivative within a set. Its specific formulation is useful for
tangent cone related discussions.  -/
HasFDerivWithinAt.lim : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    ∀ {α : Type u_4} {l : Filter α} {c : α → 𝕜} {d : α → E} {v : E},
      Filter.Tendsto d l (nhds 0) →
        (∀ᶠ (n : α) in l, x + d n ∈ s) →
          Filter.Tendsto (fun n => c n • d n) l (nhds v) →
            Filter.Tendsto (fun n => c n • (f (x + d n) - f x)) l (nhds (f' v))
-- Aesop.Script.Step
_private.Aesop.Script.Step.0.Aesop.Script.Step.validate.fmtGoals : Lean.Meta.SavedState → Array Lean.MVarId → Lean.MetaM Lean.MessageData
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst : ℤ →
  ℤ →
    Lean.Meta.Grind.Arith.Linear.EqCnstr →
      Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.eq_one_iff_eq_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, v₁ x = 1 ↔ v₂ x = 1
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.toOrderBot : {α : Type u_5} → [self : IdemCommSemiring α] → OrderBot α
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instBEq : BEq Std.Http.Header.Name
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero.  -/
IsLocalMax.fderiv_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
  IsLocalMax f a → fderiv ℝ f a = 0
-- Mathlib.Topology.Compactness.Compact
compactSpace_of_finite_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, ⋂ i ∈ u, t i = ∅) → CompactSpace X
-- Mathlib.LinearAlgebra.Pi
LinearMap.vecCons_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {n : ℕ} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) (m : M),
  (f.vecCons g) m = Matrix.vecCons (f m) (g m)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.lift_symm_apply_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] (φ : Unitization R A →ₐ[R] C) (a : A), (Unitization.lift.symm φ) a = φ ↑a
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
average of `‖f y - f x‖` on `a` tends to `0` as `a` shrinks to `x` along a Vitali family.  -/
VitaliFamily.ae_tendsto_average_norm_sub : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (nhds 0)
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- Let `f : X x Y → Z`. If as `y` tends to `l`, `f(x, y) = O(g(y))` uniformly on `s : Set X`
of finite measure, then f is eventually (as `y` tends to `l`) integrable along `s`.  -/
Asymptotics.IsBigO.eventually_integrableOn : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {g : α → F} {l : Filter α} {ι : Type u_4}
  [inst_1 : MeasurableSpace ι] {f : ι × α → E} {s : Set ι} {μ : MeasureTheory.Measure ι} [inst_2 : Norm F],
  f =O[Filter.principal s ×ˢ l] (g ∘ Prod.snd) →
    (∀ᶠ (x : α) in l, MeasureTheory.AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)) →
      MeasurableSet s → μ s < ⊤ → ∀ᶠ (x : α) in l, MeasureTheory.IntegrableOn (fun i => f (i, x)) s μ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.leftExactFunctor_iff : ∀ {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.leftExactFunctor C D F ↔ CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.submoduleOf.eq_1 : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p q : Submodule R M), p.submoduleOf q = Submodule.comap q.subtype p
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_le_one`.  -/
Right.mul_le_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Any element in the fiber of an object `X` is the evaluation of a morphism from a
Galois object.  -/
CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (x : (F.obj X).obj),
  ∃ A f a, CategoryTheory.PreGaloisCategory.IsGalois A ∧ (CategoryTheory.ConcreteCategory.hom (F.map f)) a = x
-- Mathlib.Topology.MetricSpace.BundledFun
/-- A pseudometric must be symmetric.  -/
PseudoMetric.symm' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (self : PseudoMetric X R) (x y : X),
  self.toFun x y = self.toFun y x
-- Init.Core
/-- `RightIdentity op o` indicates `o` is a right identity `o` of `op`.

This class does not require a proof that `o` is an identity, and is used
primarily for inferring the identity using class resolution.
 -/
Std.RightIdentity : {α : Sort u} → {β : Sort u_1} → (α → β → α) → outParam β → Prop
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_univ : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R], MvPolynomial.restrictSupport R Set.univ = ⊤
-- Mathlib.Analysis.Convex.Jensen
/-- Convex **strict Jensen inequality**.

If the function is strictly convex, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.

See also `StrictConvexOn.map_sum_eq_iff`.  -/
StrictConvexOn.map_sum_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) → f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
-- Mathlib.Analysis.Convex.Basic
Convex.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : SMul 𝕜 E] [inst_5 : SMul 𝕜 F] {s : Set E} {t : Set F},
  Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ×ˢ t)
-- Mathlib.Topology.Order.OrderClosed
not_tendsto_atBot_of_tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [NoBotOrder α] [inst_2 : TopologicalSpace α] [ClosedIicTopology α]
  {a : α} {l : Filter β} [l.NeBot] {f : β → α}, Filter.Tendsto f l (nhds a) → ¬Filter.Tendsto f l Filter.atBot
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_toArray_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → (t₁.Equiv t₂ ↔ Std.DTreeMap.Internal.Impl.Const.toArray t₁ = Std.DTreeMap.Internal.Impl.Const.toArray t₂)
-- Lean.MetavarContext
/-- Similar to `exprDependsOn`, but `x` can be a free variable or an unassigned metavariable.  -/
Lean.exprDependsOn' : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → Lean.Expr → m Bool