mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a diagram `CostructuredArrow F X`s, we may obtain a cocone with cone point `X`.  -/
CategoryTheory.Limits.Cocone.fromCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor C D) →
              {X : D} →
                (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)) →
                  CategoryTheory.Limits.Cocone (G.comp ((CategoryTheory.CostructuredArrow.proj F X).comp F))
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (rupHints : Array ℕ) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_2 id rupHints
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Finite.measurableSet_sInter : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)}, s.Finite → (∀ t ∈ s, MeasurableSet t) → MeasurableSet (⋂₀ s)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
/-- To show that two linear maps from the exterior algebra agree, it suffices to show they agree on
the exterior powers.

See note [partially-applied ext lemmas]  -/
ExteriorAlgebra.lhom_ext : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] ⦃f g : ExteriorAlgebra R M →ₗ[R] N⦄,
  (∀ (i : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (ExteriorAlgebra.ιMulti R i)) →
    f = g
-- Mathlib.Tactic.Linter.Header
/-- The main function to validate the copyright string.
The input is the copyright string, the output is an array of `Syntax × String` encoding:
* the `Syntax` factors are atoms whose ranges are "best guesses" for where the changes should
  take place; the embedded string is the current text that the linter flagged;
* the `String` factor is the linter message.

The linter checks that
* the first and last line of the copyright are a `("/-", "-/")` pair, each on its own line;
* the first line is begins with `Copyright (c) 20` and ends with `. All rights reserved.`;
* the second line equals `expectedLicense` (determined by the `linter.style.header.license` option,
  defaults to the Mathlib default);
* the remainder of the string begins with `Authors: `, does not end with `.` and
  contains no ` and ` nor a double space, except possibly after a line break.
 -/
Mathlib.Linter.copyrightHeaderChecks : String → String → Array (Lean.Syntax × String)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_div_neg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], 1 / a < 0 ↔ a < 0
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption.match_1.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : String.Slice.SplitIterator pat s → Sort u_1)
  (h_1 :
    (currPos : s.Pos) →
      (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) → motive (String.Slice.SplitIterator.operating currPos s_1))
  (h_2 : Unit → motive String.Slice.SplitIterator.atEnd),
  (match String.Slice.SplitIterator.atEnd with
    | String.Slice.SplitIterator.operating currPos s => h_1 currPos s
    | String.Slice.SplitIterator.atEnd => h_2 ()) =
    h_2 ()
-- Init.Tactics
/-- `mpure_intro` operates on a stateful `Std.Do.SPred` goal of the form `P ⊢ₛ ⌜φ⌝`.
It leaves the stateful proof mode (thereby discarding `P`), leaving the regular goal `φ`.
```lean
theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
  mpure_intro
  exact True.intro
```
 -/
Lean.Parser.Tactic.mpureIntroMacro : Lean.ParserDescr
-- Init.Data.Option.Array
Option.size_toArray_eq_one_iff : ∀ {α : Type u_1} {o : Option α}, o.toArray.size = 1 ↔ o.isSome = true
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhdsWithin_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhdsWithin x s) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.restrict_eq_codRestrict_domRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q), f.restrict hf = (f.domRestrict p).codRestrict q ⋯
-- Mathlib.Data.Fintype.Sets
Fintype.univ_Prop : Finset.univ = {True, False}
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.opNorm_le_of_lipschitz : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂} {K : NNReal}, LipschitzWith K ⇑f → ‖f‖ ≤ ↑K
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_rel_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f g : α → M} {a : α} {r : M → M → Prop},
  r 0 0 → (a ∈ s → r (f a) (g a)) → r (s.indicator f a) (s.indicator g a)
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.ι₀_h_assoc : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁) {Z : TopCat} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀ (CategoryTheory.CategoryStruct.comp F.h h) =
    CategoryTheory.CategoryStruct.comp f₀ h
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ofHom_comp : ∀ {X Y Z : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] [inst_2 : PartialOrder Z] (f : X ↪o Y)
  (g : Y ↪o Z),
  PartOrdEmb.ofHom (RelEmbedding.trans f g) =
    CategoryTheory.CategoryStruct.comp (PartOrdEmb.ofHom f) (PartOrdEmb.ofHom g)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.IsBigO.trans_tendsto_norm_atTop : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {α : Type u_2} {u v : α → 𝕜} {l : Filter α},
  u =O[l] v → Filter.Tendsto (fun x => ‖u x‖) l Filter.atTop → Filter.Tendsto (fun x => ‖v x‖) l Filter.atTop
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_filterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.filterₘ f)
-- Mathlib.Topology.Sets.VietorisTopology
/-- When `Set` is equipped with the Vietoris topology, the powerset of a closed set is closed.  -/
IsClosed.powerset_vietoris : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed (𝒫 F)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instCoeFunForall : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → CoeFun (M ≃+ N) fun x => M → N
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonUnit : Lean.ToJson Unit
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- The composition of a sheaf with a ULift functor is still a sheaf.  -/
CategoryTheory.Presieve.isSheaf_comp_uliftFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (J : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.Presieve.IsSheaf J P → CategoryTheory.Presieve.IsSheaf J (P.comp CategoryTheory.uliftFunctor.{w', w})
-- Mathlib.Data.Seq.Computation
Computation.equiv_of_mem : ∀ {α : Type u} {s t : Computation α} {a : α}, a ∈ s → a ∈ t → s.Equiv t
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpace.eq_1 : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R), LieModule.genWeightSpace M χ = ⨅ x, LieModule.genWeightSpaceOf M (χ x) x
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 0379](https://stacks.math.columbia.edu/tag/0379) -/
IsIrreducible.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsIrreducible s → ∀ (f : X → Y), ContinuousOn f s → IsIrreducible (f '' s)
-- Mathlib.Algebra.Tropical.Basic
Tropical.succ_nsmul : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : OrderTop R] (x : Tropical R) (n : ℕ), (n + 1) • x = x
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.comp_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z)
  (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ),
  (TopCat.Presheaf.Pushforward.comp f g ℱ).inv.app U =
    CategoryTheory.CategoryStruct.id
      (((TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)).obj U)
-- Mathlib.CategoryTheory.Monoidal.Arrow
/-- The monoidal closed instance induced by the pushout-product and pullback-hom.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instMonoidalClosedArrowOfHasPullbacks : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_4 : CategoryTheory.MonoidalClosed C] →
            [inst_5 : CategoryTheory.BraidedCategory C] →
              [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.MonoidalClosed (CategoryTheory.Arrow C)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- Given a morphism of presheaves of rings `φ : S ⟶ F.op ⋙ R`, this is the property
that the (partial) left adjoint functor of `pushforward φ` is defined
on a certain object `M : PresheafOfModules S`.  -/
PresheafOfModules.pullbackObjIsDefined : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
            {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
              (S ⟶ F.op.comp R) → CategoryTheory.ObjectProperty (PresheafOfModules S)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.instCategoryStructHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → CategoryTheory.CategoryStruct.{w, max v w} (a ⟶ b)
-- Mathlib.Dynamics.FixedPoints.Support
_private.Mathlib.Dynamics.FixedPoints.Support.0.Function.HasCompactFixedSupport.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : X → X),
  Function.HasCompactFixedSupport f = IsCompact (Function.fixedSupport f)
-- Mathlib.Combinatorics.Graph.Subgraph
/-- Two subgraphs of the same graph are compatible.  -/
Graph.Compatible.of_le_le : ∀ {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β}, H₁ ≤ G → H₂ ≤ G → H₁.Compatible H₂
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.surjective_of_iterate_surjective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M} {n : ℕ}, n ≠ 0 → Function.Surjective ⇑(f' ^ n) → Function.Surjective ⇑f'
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) ((t.truncGTIsoTruncGE a b h).inv.app X) =
    (t.truncGTπ a).app X
-- Lean.DocString.Types
/-- Genre-specific metadata  -/
Lean.Doc.Part.metadata : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p → Option p
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `K` be a field with an admissible family of absolute values (giving rise
to a multiplicative height).
Let `p` be a family (indexed by `ι'`) of homogeneous polynomials in variables indexed by
the finite type `ι` and of the same degree `N`. Then for any `x : ι →  K`,
the multiplicative height of `fun j : ι' ↦ eval x (p j)` is bounded by a positive constant
times `mulHeight x ^ N`.

The difference to `mulHeight_eval_le` is that the constant is not made explicit.  -/
Height.mulHeight_eval_le' : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∃ C > 0, ∀ (x : ι → K), (Height.mulHeight fun j => (MvPolynomial.eval x) (p j)) ≤ C * Height.mulHeight x ^ N
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_zero : Real.sinc 0 = 1
-- Mathlib.Data.Fintype.BigOperators
/-- The sum over a product type equals the sum of fiberwise
sums. For rewriting in the reverse direction, use `Fintype.sum_prod_type'`.  -/
Fintype.sum_prod_type : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid γ]
  (f : α₁ × α₂ → γ), ∑ x, f x = ∑ x, ∑ y, f (x, y)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_div_natCast : ∀ {x : ℝ} (m : ℕ), Irrational (x / ↑m) → Irrational x
-- Init.PropLemmas
exists_false : ∀ {α : Sort u_1}, ¬∃ _a, False
-- Mathlib.Analysis.Convex.Deriv
StrictMonoOn.exists_deriv_lt_slope_aux : ∀ {x y : ℝ} {f : ℝ → ℝ},
  ContinuousOn f (Set.Icc x y) →
    x < y →
      StrictMonoOn (deriv f) (Set.Ioo x y) →
        (∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) → ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Replacing the first point by one on the same line but the opposite ray adds π to the oriented
angle.  -/
Sbtw.oangle_eq_add_pi_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₁' p₂ p₃ : P},
  Sbtw ℝ p₁ p₂ p₁' → p₃ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃ + ↑Real.pi
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.exists_mem_span_nat_finset_of_ge : ∀ (s : Set ℕ), ∃ t n, ↑t ⊆ s ∧ ∀ m ≥ n, Nat.setGcd s ∣ m → m ∈ Ideal.span ↑t
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
conformal_id : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X], Conformal id
-- Lean.Server.Requests
Lean.Server.RequestError.rpcNeedsReconnect : Lean.Server.RequestError
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_leOfHom : ∀ {X : Type u} [inst : Preorder X] {x y : X} (h : x ⟶ y), ⋯.hom = h
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalNameExprCore : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- We say that an outer measure `μ` in an (e)metric space is *metric* if `μ (s ∪ t) = μ s + μ t`
for any two metric separated sets `s`, `t`.  -/
MeasureTheory.OuterMeasure.IsMetric : {X : Type u_2} → [EMetricSpace X] → MeasureTheory.OuterMeasure X → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α}, (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.willSaveWaitUntil : Lean.Lsp.TextDocumentSyncOptions → Bool
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_zero_of_not_differentiableAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, ¬DifferentiableAt 𝕜 f x → deriv f x = 0
-- Mathlib.Data.Set.Sups
Set.infs_subset_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
-- Plausible.Arbitrary
/-- Pick a simple ASCII character 2/3s of the time, and otherwise pick any random `Char` encoded by
the next `Nat` (or `\0` if there is no such character)  -/
Plausible.Char.arbitraryDefaultInstance : Plausible.Arbitrary Char
-- Lean.Parser.Term
Lean.Parser.Term.falseVal.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.BitVec.Lemmas
BitVec.ofFnLE.eq_1 : ∀ {n : ℕ} (f : Fin n → Bool), BitVec.ofFnLE f = BitVec.ofFnLEAux n f
-- Mathlib.Topology.Category.TopPair
/-- The embedding of the second into the first space  -/
TopPair.map : {X : TopPair} → TopPair.snd ⟶ TopPair.fst
-- Init.GetElem
List.get!Internal_eq_getElem! : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α} {i : ℕ}, l.get!Internal i = l[i]!
-- Mathlib.Logic.Embedding.Set
Set.embeddingOfSubset_apply_coe : ∀ {α : Type u_1} (s t : Set α) (h : s ⊆ t) (x : ↑s), ↑((s.embeddingOfSubset t h) x) = ↑x
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.of_map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] {x : S} {f : S →ₐ[R] T},
  Function.Injective ⇑f → IsStronglyTranscendental R (f x) → IsStronglyTranscendental R x
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_add_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'}
  {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {X : Ω → ℝ} {Y : Ω' → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 ν →
      ProbabilityTheory.variance (fun p => X p.1 + Y p.2) (μ.prod ν) =
        ProbabilityTheory.variance X μ + ProbabilityTheory.variance Y ν
-- Init.Core
/-- An equivalence relation is symmetric: `r x y` implies `r y x`  -/
Equivalence.symm : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ {x y : α}, r x y → r y x
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Typeclass saying that a subgroup of `GL(2, ℝ)` has determinant contained in `{±1}`. Necessary
so that the typeclass system can detect when the slash action is multiplicative.  -/
Subgroup.HasDetPlusMinusOne : {n : Type u_1} →
  [inst : Fintype n] → [inst_1 : DecidableEq n] → {R : Type u_2} → [inst_2 : CommRing R] → Subgroup (GL n R) → Prop
-- Mathlib.Algebra.Order.Group.Abs
abs_nsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (n : ℕ) (a : G),
  |n • a| = n • |a|
-- Init.Data.Order.MinMaxOn
instAssociativeMaxOnOfIsLinearPreorder : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β},
  Std.Associative (maxOn f)
-- Mathlib.Algebra.MvPolynomial.Monad
/-- `bind₂` is the "right-hand side" bind operation on `MvPolynomial`,
operating on the coefficient type.
Given a polynomial `p : MvPolynomial σ R` and
a map `f : R → MvPolynomial σ S` taking coefficients in `p` to polynomials over a new ring `S`,
`bind₂ f p` replaces each coefficient in `p` with its value under `f`,
producing a new polynomial over `S`.
The variable type remains the same. This operation is a ring hom.
 -/
MvPolynomial.bind₂ : {σ : Type u_1} →
  {R : Type u_3} →
    {S : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → (R →+* MvPolynomial σ S) → MvPolynomial σ R →+* MvPolynomial σ S
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelNF.Config.mk : Mathlib.Tactic.AtomM.Recurse.Config → Mathlib.Tactic.Abel.AbelMode → Mathlib.Tactic.Abel.AbelNF.Config
-- Batteries.Data.Nat.Lemmas
Nat.testBit_ofBits_ge : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ), n ≤ i → (Nat.ofBits f).testBit i = false
-- Mathlib.Algebra.Order.Group.Indicator
Set.iSup_indicator : ∀ {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : Zero M] {ι : Type u_4} [inst_2 : Preorder ι]
  [IsDirectedOrder ι] {f : ι → α → M} {s : ι → Set α},
  ⊥ = 0 → Monotone f → Monotone s → ⨆ i, (s i).indicator (f i) = (⋃ i, s i).indicator (⨆ i, f i)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit.coe_smul : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a : α} {m : M}
  {a' : ↑(MulAction.orbit M a)}, ↑(m • a') = m • ↑a'
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroup_map_conj_eq : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M},
  g • t = s → Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M t) = fixingSubgroup M s
-- Lean.Util.Trace
Lean.TraceElem.mk.injEq : ∀ (ref : Lean.Syntax) (msg : Lean.MessageData) (ref_1 : Lean.Syntax) (msg_1 : Lean.MessageData),
  ({ ref := ref, msg := msg } = { ref := ref_1, msg := msg_1 }) = (ref = ref_1 ∧ msg = msg_1)
-- Init.PropLemmas
ne_of_mem_of_not_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → b ∉ s → a ≠ b
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk''_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (S : CategoryTheory.StrictPseudofunctorPreCore B C) {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.StrictPseudofunctor.mk'' S).map₂ a_1 = S.map₂ a_1
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.subtype_injective : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M), Function.Injective ⇑S.subtype
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real
vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse
constant `C * K` where `C` only depends on `E'`. We record a working value for this constant `C`
as `lipschitzExtensionConstant E'`.  -/
lipschitzExtensionConstant : (E' : Type u_1) → [inst : NormedAddCommGroup E'] → [inst_1 : NormedSpace ℝ E'] → [FiniteDimensional ℝ E'] → NNReal
-- Mathlib.Probability.Distributions.Gaussian.Real
Homeomorph.mulLeft₀.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c : α)
  (hc : c ≠ 0),
  Homeomorph.mulLeft₀ c hc = { toEquiv := Equiv.mulLeft₀ c hc, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Topology.Constructions
isOpenMap_ofMul : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑Additive.ofMul