mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).contains k = (f t[k]?).isSome
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_right_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.ι = h.right.ι
-- Mathlib.Topology.DiscreteSubset
/-- If a subset of a topological space has no accumulation points,
then it carries the discrete topology.  -/
discreteTopology_of_noAccPts : ∀ {X : Type u_3} [inst : TopologicalSpace X] {E : Set X}, (∀ x ∈ E, ¬AccPt x (Filter.principal E)) → DiscreteTopology ↑E
-- Init.Guard
/-- Command to check equality of two expressions.
* `#guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency.
* `#guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency.
* `#guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal.
* `#guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent.

This is a command version of the `guard_expr` tactic.  -/
Lean.Parser.Command.guardExprCmd : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_inf : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N),
  Function.Injective ⇑f → AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieAddGroup I' n G],
  ContMDiffMap.addGroup =
    { toAddMonoid := ContMDiffMap.addMonoid, neg := fun f => ⟨fun x => -f x, ⋯⟩, sub := fun f g => ⟨⇑f - ⇑g, ⋯⟩,
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult : Inhabited Std.Tactic.BVDecide.LRAT.Internal.Result
-- Lean.Language.Basic
Lean.Language.DynamicSnapshot.mk.injEq : ∀ (val : Dynamic) (toSnapshotTreeM : Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree) (val_1 : Dynamic)
  (toSnapshotTreeM_1 : Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree),
  ({ val := val, toSnapshotTreeM := toSnapshotTreeM } = { val := val_1, toSnapshotTreeM := toSnapshotTreeM_1 }) =
    (val = val_1 ∧ toSnapshotTreeM = toSnapshotTreeM_1)
-- Mathlib.Util.Export
Lean.Export.Entry.level.inj : ∀ {n n_1 : Lean.Level}, Lean.Export.Entry.level n = Lean.Export.Entry.level n_1 → n = n_1
-- Mathlib.Control.Traversable.Instances
Option.id_traverse : ∀ {α : Type u_1} (x : Option α), Option.traverse pure x = pure x
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a b : α i),
  Pi.single i '' Set.Icc a b = Set.Icc (Pi.single i a) (Pi.single i b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.equivOfInverse.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f₁ f₁_1 : M₁ →SL[σ₁₂] M₂) (e_f₁ : f₁ = f₁_1)
  (f₂ f₂_1 : M₂ →SL[σ₂₁] M₁) (e_f₂ : f₂ = f₂_1) (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁)
  (h₂ : Function.RightInverse ⇑f₂ ⇑f₁),
  ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂ = ContinuousLinearEquiv.equivOfInverse f₁_1 f₂_1 ⋯ ⋯
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- Strong recursion principle for a normalised EDS: if we have
* `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,

then we have `P n` for all `n : ℕ`.
 -/
normEDSRec' : {P : ℕ → Sort u_4} →
  P 0 →
    P 1 →
      P 2 →
        P 3 →
          P 4 →
            ((m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))) →
              ((m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)) → (n : ℕ) → P n
-- Mathlib.Data.ENNReal.Operations
ENNReal.Finiteness.add_ne_top : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → a + b ≠ ⊤
-- Mathlib.Geometry.Manifold.Notation
/-- `UniqueMDiffAt[s] x` elaborates to `UniqueMDiffWithinAt I s x`
trying to determine `I` from the local context.
The argument `x` can be omitted.  -/
Manifold.«termUniqueMDiffAt[_]» : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instInhabited : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → Inhabited (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instVAdd'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], Lex.instVAdd' = inst
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it₁ : Std.IterM m β} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β) →
                (b : β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩) →
              ((it₁' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ : {α : Type u} →
  [BEq α] →
    [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → List α → Std.DHashMap.Internal.Raw₀ α fun x => Unit
-- Mathlib.Topology.UniformSpace.Compact
lebesgue_number_lemma_nhds' : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {U : (x : α) → x ∈ K → Set α},
  IsCompact K →
    (∀ (x : α) (hx : x ∈ K), U x hx ∈ nhds x) → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ y, UniformSpace.ball x V ⊆ U ↑y ⋯
-- Init.Data.Array.Zip
Array.zip_map_left : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {as : Array α} {bs : Array β},
  (Array.map f as).zip bs = Array.map (Prod.map f id) (as.zip bs)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_nonpos : ∀ {a : ℤ}, a ≤ 0 → ∀ (b : ℕ), mkRat a b ≤ 0
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_eq_clzAuxRec_of_getLsbD_false : ∀ {w n k : ℕ} {x : BitVec w}, (∀ (i : ℕ), n < i → x.getLsbD i = false) → x.clzAuxRec n = x.clzAuxRec (n + k)
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.currying₃.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E],
  CategoryTheory.Functor.currying₃ =
    CategoryTheory.Functor.currying.trans
      (CategoryTheory.Functor.currying.trans (CategoryTheory.prod.associativity C₁ C₂ C₃).congrLeft)
-- Mathlib.Algebra.Order.Group.PosPart
inf_eq_div_oneLePart_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), a ⊓ b = a / (a / b)⁺ᵐ
-- Init.Data.BitVec.Lemmas
/-- Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
accessing bits `x` in the range `[r, w)`.

Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

(x.rotateLeft 2).getLsbD ⟨i, i ≤ 7 - 2⟩
= <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩
= <6 5 4 3 2>.getLsbD i
= <6 5 4 3 2 | 1 0>[i + 2]
 -/
BitVec.getLsbD_rotateRightAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i < w - r → (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i)
-- Mathlib.NumberTheory.FactorisationProperties
/-- A positive natural number is either deficient, perfect, or abundant  -/
Nat.deficient_or_perfect_or_abundant : ∀ {n : ℕ}, 0 ≠ n → n.Deficient ∨ n.Abundant ∨ n.Perfect
-- Mathlib.Data.Finset.Sym
Finset.symInsertEquiv_apply_fst : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α] {n : ℕ} (h : a ∉ s) (m : ↥((insert a s).sym n)),
  ((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.tensorObj.instTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {M N : C} →
          [CategoryTheory.MonObj M] →
            [CategoryTheory.MonObj N] → CategoryTheory.MonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.trans_sSameSide : ∀ {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 z : P}, s.WSameSide x y → s.SSameSide y z → s.WSameSide x z
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
instContMDiffVectorBundleOfNatWithTopENat : ∀ {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 2 F E IB], ContMDiffVectorBundle 1 F E IB
-- Mathlib.Topology.Instances.Matrix
summable_matrix_conjTranspose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R},
  Summable (fun x => (f x).conjTranspose) L ↔ Summable f L
-- Mathlib.RingTheory.Jacobson.Radical
Submodule.FG.jacobson_smul_lt : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  N ≠ ⊥ → N.FG → Ring.jacobson R • N < N
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `s`-factored
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p ∈ s`. At the same time,
we show that the sum involved converges absolutely.  -/
EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →* F},
  (∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1) →
    ∀ (s : Finset ℕ), (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  Std.DTreeMap.Raw.Const.get (m₁ ∩ m₂) k h_mem = Std.DTreeMap.Raw.Const.get m₁ k ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_3 : ∀ (fuel_2 : ℕ) (k₁ k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁)
      (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2) =
    (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2).addConst k₁
-- Mathlib.Logic.Function.Basic
Function.forall_update_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop),
  (∀ (x : α), p x (Function.update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeInterpStrLit.loop : String → String.Pos.Raw → String → Option String
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The (identity) equivalence between `C` and its monoidal opposite.  -/
CategoryTheory.MonoidalOpposite.mopEquiv : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → C ≌ Cᴹᵒᵖ
-- Mathlib.Topology.Defs.Filter
WeaklyLocallyCompactSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X], (∀ (x : X), ∃ s, IsCompact s ∧ s ∈ nhds x) → WeaklyLocallyCompactSpace X
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`.  -/
SimpleGraph.Embedding.complEquiv : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {H : SimpleGraph W} → G ↪g H ≃ Gᶜ ↪g Hᶜ
-- Init.Data.Fin.Basic
Fin.instMod : {n : ℕ} → Mod (Fin n)
-- Init.Data.Ord.UInt
UInt32.instLawfulEqOrd : Std.LawfulEqOrd UInt32
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, m.WF → (k ∈ Std.HashMap.Raw.map f m ↔ k ∈ m)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `Part.seq` as a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.seq : {α : Type u_2} →
  [inst : OmegaCompletePartialOrder α] → {β γ : Type v} → (α →𝒄 Part (β → γ)) → (α →𝒄 Part β) → α →𝒄 Part γ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C =
    { obj := fun F => F.mapMon.obj (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1})),
      map := fun {X Y} α =>
        ((CategoryTheory.Functor.mapMonFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C).map α).app
          (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1})),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Submonoid.Primal
/-- The submonoid of primal elements in a cancellative commutative monoid with zero.  -/
Submonoid.isPrimal : (M₀ : Type u_1) → [inst : CommMonoidWithZero M₀] → [IsCancelMulZero M₀] → Submonoid M₀
-- Init.Data.Array.Erase
Array.size_erase_le : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, (xs.erase a).size ≤ xs.size
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Pi.instMeasurableSingletonClass : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [Countable δ]
  [∀ (a : δ), MeasurableSingletonClass (X a)], MeasurableSingletonClass ((a : δ) → X a)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift_obj_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} (t : CategoryTheory.Limits.Cone K)
  (x : CategoryTheory.WithTerminal J),
  (CategoryTheory.WithTerminal.coneLift✝.obj t).π.app x =
    match x with
    | CategoryTheory.WithTerminal.of a => CategoryTheory.Over.Hom.left (t.π.app a)
    | CategoryTheory.WithTerminal.star => t.pt.hom
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonpos : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → ℝ} {a b : ℝ} {g : ℝ → F},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, f' x ≤ 0) →
        a ≤ b → ∫ (x : ℝ) in Set.Icc a b, f' x • g (f x) = -∫ (u : ℝ) in Set.Icc (f b) (f a), g u
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos : ∀ {n i : ℕ}, i ≤ n → 0 < (-1) ^ i * Polynomial.Chebyshev.leadingCoeffC✝ n i
-- Lean.Message
Lean.MessageData.withNamingContext : Lean.NamingContext → Lean.MessageData → Lean.MessageData
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.le_iff : ∀ {α : Type u_5} {t₁ t₂ : TopologicalSpace α} {Us : Set (TopologicalSpace.Opens α)},
  TopologicalSpace.Opens.IsBasis Us → (t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen ↑U)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ F).hom.app X =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.isClosedEmbedding_coe : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [DiscreteTopology A] [ContinuousMul B] [T2Space B],
  Topology.IsClosedEmbedding DFunLike.coe
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instAddCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → AddCommGroup (ContMDiffSection I F n V)
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.integralCLM.congr_simp : ∀ (𝕜 : Type u_2) {D : Type u_4} {V : Type u_9} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace ℝ D] [inst_3 : NormedAddCommGroup V] [inst_4 : NormedSpace ℝ V] [inst_5 : NormedSpace 𝕜 V]
  [inst_6 : MeasurableSpace D] (μ μ_1 : MeasureTheory.Measure D) (e_μ : μ = μ_1) [hμ : μ.HasTemperateGrowth]
  [inst_7 : BorelSpace D] [inst_8 : SecondCountableTopology D],
  SchwartzMap.integralCLM 𝕜 μ = SchwartzMap.integralCLM 𝕜 μ_1
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isLUB : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α] {s : Set α},
  IsCompact s → s.Nonempty → ∃ x ∈ s, IsLUB s x
-- Mathlib.Topology.Continuous
Continuous.tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (x : X), Filter.Tendsto f (nhds x) (nhds (f x))
-- Init.Data.Array.Subarray
/-- Extracts an element from the subarray, or returns a default value `v₀` when the index is out of
bounds.

The index is relative to the start and end of the subarray, rather than the underlying array.
 -/
Subarray.getD : {α : Type u_1} → Subarray α → ℕ → α → α
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Given a continuous bilinear map `G → E → F`, construct the associated bilinear map
`G → Lp E p μ → Lp F p μ`.  -/
ContinuousLinearMap.compLpₗ₂ : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : NormedAddCommGroup E] →
            {𝕜 : Type u_6} →
              [inst_1 : NontriviallyNormedField 𝕜] →
                [inst_2 : NormedSpace 𝕜 E] →
                  {F : Type u_8} →
                    {G : Type u_9} →
                      [inst_3 : NormedAddCommGroup F] →
                        [inst_4 : NormedSpace 𝕜 F] →
                          [inst_5 : NormedAddCommGroup G] →
                            [inst_6 : NormedSpace 𝕜 G] →
                              (G →L[𝕜] E →L[𝕜] F) → G →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ) →ₗ[𝕜] ↥(MeasureTheory.Lp F p μ)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.directed_distinctConstantsTheory : ∀ {L : FirstOrder.Language} {α : Type u'}, Directed (fun x1 x2 => x1 ⊆ x2) L.distinctConstantsTheory
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a}.erase a = 0
-- Mathlib.Logic.Equiv.Fintype
Function.Embedding.toEquivRange_eq_ofInjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β),
  f.toEquivRange = Equiv.ofInjective ⇑f ⋯
-- Lean.Elab.ConfigEval.Types
/-- Direct evaluation of `Term` syntax, avoiding term elaboration.
Instances should use `throwUnsupportedSyntax` to signal that the syntax is not recognized.
Instances shouldn't generally throw other exceptions.

Evaluation is allowed to imagine that certain coercions are implicitly inserted.
For example, the `Option Int` instance is allowed to recognize `1` as an `Option Int`
even though term elaboration would fail here. This allowance should be used lightly,
since generally `EvalTerm` is used as the fast path, and when using the `EvalExpr`
backup, such expressions will no longer be recognized.

Implementations should add `TermInfo` when the info is enabled.
The `Expr` return value is to support constructing such expressions in combinators.
 -/
Lean.Elab.ConfigEval.EvalTerm.evalTerm : {α : Type} → [self : Lean.Elab.ConfigEval.EvalTerm α] → Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_cases : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)] {i : ι}
  (p : π i → Prop), p (f i) → p (g i) → p (s.piecewise f g i)
-- Mathlib.NumberTheory.Pell
Pell.IsFundamental.x_mul_y_le_y_mul_x : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
  Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → a.x * a₁.y ≤ a.y * a₁.x
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom_sliceTo : ∀ {s : String.Slice} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos},
  (s.sliceTo pos).sliceFrom pos' = s.slice (String.Slice.Pos.ofSliceTo pos') pos ⋯
-- Mathlib.NumberTheory.ModularForms.Basic
/-- `mcast` does not change the pointwise values of a modular form.  -/
ModularForm.mcast_apply : ∀ {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a)
  (hΓ : autoParam (Γ' = Γ) ModularForm.mcast_apply._auto_1) (z : UpperHalfPlane), (ModularForm.mcast h f hΓ) z = f z
-- Mathlib.Analysis.Complex.Norm
Complex.norm_int_of_nonneg : ∀ {n : ℤ}, 0 ≤ n → ‖↑n‖ = ↑n