mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.match_2.eq_1 : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u_2}
  (motive : (x : ℕ) → x ≤ n → α (n - x) ⋯ → Sort u_1) (h : 0 ≤ n) (a : α (n - 0) ⋯)
  (h_1 : (h : 0 ≤ n) → (a : α (n - 0) ⋯) → motive 0 h a)
  (h_2 : (m : ℕ) → (h : m.succ ≤ n) → (a : α (n - m.succ) ⋯) → motive m.succ h a),
  (match 0, h, a with
    | 0, h, a => h_1 h a
    | m.succ, h, a => h_2 m h a) =
    h_1 h a
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure.  -/
AddSubmonoidClass.toAddZeroClass : {M : Type u_4} →
  [inst : AddZeroClass M] →
    {A : Type u_5} → [inst_1 : SetLike A M] → [AddSubmonoidClass A M] → (S : A) → AddZeroClass ↥S
-- Lean.DocString.Syntax
/-- Bold emphasis.

A single `*` suffices to make text bold. Using `_` for emphasis.

Bold text may be nested by using longer sequences of `*` for the outer delimiters.
 -/
Lean.Doc.Syntax.bold : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
infEDist_thickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ},
  0 < δ → ∀ (s : Set E) (x : E), Metric.infEDist x (Metric.thickening δ s) = Metric.infEDist x s - ENNReal.ofReal δ
-- Mathlib.Algebra.BigOperators.WithTop
/-- A product is infinite iff each factor is nonzero and some factor is infinite  -/
WithTop.prod_eq_top_iff : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀},
  ∏ j ∈ s, f j = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_zero : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β), Multiset.foldr f b 0 = b
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.intCast_hadamard_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : IntCast α] (a : ℤ), (↑a).hadamard (SimpleGraph.adjMatrix α G) = 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivalence of `fixingSubgroup M t` with `fixingSubgroup M s`
when `s` is a translate of `t`.  -/
SubMulAction.fixingSubgroupEquivFixingSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] → {s t : Set α} → {g : M} → g • t = s → ↥(fixingSubgroup M t) ≃* ↥(fixingSubgroup M s)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The distributional inverse Fourier transform and the classical inverse Fourier transform
coincide on `𝓢(E, F)`.  -/
TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap E F),
  FourierTransformInv.fourierInv ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (FourierTransformInv.fourierInv f)
-- Mathlib.Order.Cover
CovBy.exists_set_sdiff_singleton : ∀ {α : Type u_1} {s t : Set α}, s ⋖ t → ∃ a ∈ t, t \ {a} = s
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isConnected_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 ≤ r → IsConnected (Metric.closedBall x r)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.addAction : {R : Type u} → {M : Type v} → [inst : AddMonoid R] → [inst_1 : AddAction R M] → (p : SubAddAction R M) → AddAction R ↥p
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} [inst_3 : SizeOf C]
  (hom : R₁.X ⟶ R₂.X) [isRingHom : CategoryTheory.IsRingHom hom],
  sizeOf { hom := hom, isRingHom := isRingHom } = 1 + sizeOf hom + sizeOf isRingHom
-- Lean.Environment
/-- Exceptions that can be raised by the kernel when type checking new declarations.  -/
Lean.Kernel.Exception : Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.rfl : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β}, m.Equiv m
-- Mathlib.RingTheory.Valuation.Basic
Valuation.unit_map_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (u : Rˣ), ↑((Units.map ↑v) u) = v ↑u
-- Std.Time.DateTime.Timestamp
/-- Creates a `Timestamp` from a `Second.Offset`.
 -/
Std.Time.Timestamp.ofSecondsSinceUnixEpoch : Std.Time.Second.Offset → Std.Time.Timestamp
-- Mathlib.Algebra.Group.Even
Even.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] {a : α} (f : F), Even a → Even (f a)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.instCoeTCConstants : {L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → CoeTC L.Constants M
-- Mathlib.Analysis.Normed.Group.Uniform
Real.isClosed_range_intCast : IsClosed (Set.range Int.cast)
-- Mathlib.Topology.NhdsWithin
inter_mem_nhdsWithin_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a b c d : Set α} {x : α},
  a ∈ nhdsWithin x b → c ∈ nhdsWithin x d → a ∩ c ∈ nhdsWithin x (b ∩ d)
-- Init.Data.Fin.Lemmas
Fin.lt_iff_le_and_ne : ∀ {n : ℕ} {a b : Fin n}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : αᵒᵈ),
  Finset.Ici (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iic a)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.find?_prop_eq_find?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  pos.find? p = pos.find? fun x => decide (p x)
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.mk.injEq : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (size_1 : ℕ)
  (buckets_1 : Array (Std.DHashMap.Internal.AssocList α β)),
  ({ size := size, buckets := buckets } = { size := size_1, buckets := buckets_1 }) =
    (size = size_1 ∧ buckets = buckets_1)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instSetLike : {M : Type u_1} → [inst : AddZeroClass M] → SetLike (AddSubmonoid M) M
-- Init.Data.SInt.Bitwise
Int64.xor_assoc : ∀ (a b c : Int64), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Lean.Meta.Basic
Lean.Meta.resetUnfoldAxiom : Lean.MetaM Unit
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mk.injEq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (toList : List ((i : ι) × M i))
  (ne_one : ∀ l ∈ toList, l.snd ≠ 1) (chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList)
  (toList_1 : List ((i : ι) × M i)) (ne_one_1 : ∀ l ∈ toList_1, l.snd ≠ 1)
  (chain_ne_1 : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList_1),
  ({ toList := toList, ne_one := ne_one, chain_ne := chain_ne } =
      { toList := toList_1, ne_one := ne_one_1, chain_ne := chain_ne_1 }) =
    (toList = toList_1)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBasis'_iff_isBasis_restrict_univ : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X ↔ (M.restrict Set.univ).IsBasis I X
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
/-- An object `X` is fibrant if `X ⟶ ⊤_ C` is a fibration.  -/
HomotopicalAlgebra.IsFibrant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] → [CategoryTheory.Limits.HasTerminal C] → C → Prop
-- Mathlib.Order.Basic
eq_of_forall_le_iff : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, (∀ (c : α), c ≤ a ↔ c ≤ b) → a = b
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.mem_countablePartitionSet : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) (a : α),
  a ∈ MeasurableSpace.countablePartitionSet n a
-- Lean.Server.References
Lean.Server.TransientWorkerILean.mk.sizeOf_spec : ∀ (moduleUri : Lean.Lsp.DocumentUri) (version : ℕ) (directImports : Lean.Server.DirectImports)
  (isSetupFailure? : Option Bool) (refs : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls),
  sizeOf
      { moduleUri := moduleUri, version := version, directImports := directImports, isSetupFailure? := isSetupFailure?,
        refs := refs, decls := decls } =
    1 + sizeOf moduleUri + sizeOf version + sizeOf directImports + sizeOf isSetupFailure? + sizeOf refs + sizeOf decls
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapWithPostcondition_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : γ → Std.Iterators.PostconditionT o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapWithPostcondition g (Std.IterM.filterMapWithPostcondition f it)).toListRev =
    (Std.IterM.filterMapWithPostcondition
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toListRev
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_inv_triangular : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (v : ι → E)
  {i j : ι}, i < j → inner 𝕜 (InnerProductSpace.gramSchmidt 𝕜 v j) (v i) = 0
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  ∃ t, ⇑(f.toPartitionOfUnity i) =ᶠ[nhds x] ⇑(f i) * ⇑(∏ j ∈ t with WellOrderingRel j i, (1 - f j))
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_eball_self`. -/
EMetric.mem_ball_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, 0 < ε → x ∈ Metric.eball x ε
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.ofSub.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G) (hsn : s.Nonempty) (hs : ∀ x ∈ s, ∀ y ∈ s, x + -y ∈ s),
  AddSubgroup.ofSub s hsn hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Equiv.decidable.match_1.eq_4 : ∀ {α : Type u_1} (motive : Lists α → Lists α → Sort u_2) (l₁ l₂ : Lists' α true)
  (h_1 : (l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩)
  (h_2 : (l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩)
  (h_3 : (l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩)
  (h_4 : (l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩),
  (match ⟨true, l₁⟩, ⟨true, l₂⟩ with
    | ⟨false, l₁⟩, ⟨false, l₂⟩ => h_1 l₁ l₂
    | ⟨false, l₁⟩, ⟨true, l₂⟩ => h_2 l₁ l₂
    | ⟨true, l₁⟩, ⟨false, l₂⟩ => h_3 l₁ l₂
    | ⟨true, l₁⟩, ⟨true, l₂⟩ => h_4 l₁ l₂) =
    h_4 l₁ l₂
-- Mathlib.Order.Defs.Unbundled
instTransOfIsTrans : {α : Sort u_1} → {r : α → α → Prop} → [IsTrans α r] → Trans r r r
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- A left adjoint commutes with a left Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.isKanOfWhiskerLeftAdjoint : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {t : CategoryTheory.Bicategory.LeftExtension f g} →
            t.IsKan →
              {x : B} → {h : c ⟶ x} → {u : x ⟶ c} → CategoryTheory.Bicategory.Adjunction h u → (t.whisker h).IsKan
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertList_of_contains_eq_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
      Std.Internal.List.containsKey k toInsert = true →
        Std.Internal.List.getEntry? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getEntry? k toInsert
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_def : ∀ {u : ℕ → ENNReal}, ExpGrowth.expGrowthInf u = LinearGrowth.linearGrowthInf (ENNReal.log ∘ u)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionUnitIso`, the structural isomorphism `𝟙_ C ⊙ₗ - ≅ -`,
allowing one to specify the acting category.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«termλₗ[_]» : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Comp
derivWithin_comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'}
  {y : 𝕜'},
  DifferentiableWithinAt 𝕜' h₂ s' y →
    DifferentiableWithinAt 𝕜 h s x →
      Set.MapsTo h s s' → h x = y → derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instFaithfulSMulProdOfNonempty : ∀ (D : Type u_1) (Q : Type u_2) [inst : Group D] [inst_1 : Group Q] (Λ : Type u_3) [inst_2 : MulAction D Λ]
  [FaithfulSMul D Λ] [Nonempty Q] [Nonempty Λ], FaithfulSMul (D ≀ᵣ Q) (Λ × Q)
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_injective : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B], Function.Injective (FractionalIdeal.dual A K)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projection norms are bounded above in a complete space.  -/
UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X],
  BddAbove (Set.range fun A => ‖GeneralSchauderBasis.proj b A‖₊)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_add_inv_eq_inv : ∀ {p q r : NNReal}, p.HolderTriple q r → p⁻¹ + q⁻¹ = r⁻¹
-- Mathlib.Order.Minimal
maximal_maximal : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], Maximal (Maximal P) x ↔ Maximal P x
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.krullDimLE_of_coheight_le : ∀ {X : AlgebraicGeometry.Scheme} {z : ↥X} {n : ℕ}, Order.coheight z ≤ ↑n → Ring.KrullDimLE n ↑(X.presheaf.stalk z)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- `triangleRotateShortComplex φ` is a degreewise split short exact sequence of
cochain complexes.  -/
CochainComplex.mappingCone.triangleRotateShortComplexSplitting : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (n : ℤ) →
              ((CochainComplex.mappingCone.triangleRotateShortComplex φ).map
                  (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iio_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n),
  ∑ i < Fin.castAdd m a, f i = ∑ i < a, f (Fin.castAdd m i)
-- Mathlib.Order.LatticeIntervals
Set.Iic.orderBot : {α : Type u_1} → {a : α} → [inst : Preorder α] → [OrderBot α] → OrderBot ↑(Set.Iic a)
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.elim' : ∀ {α : Type u_1} {ι : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → f i ⊓ f j ≠ ⊥ → i = j
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_iff_dSmooth : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p ↔ Diffeology.DSmooth p
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.eval_zero_det_det : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] (k : m) [inst_4 : Fintype m] [inst_5 : Fintype n]
  (f : S →+* Matrix n n R),
  Polynomial.eval 0 (f.polyToMatrix (Algebra.Norm.Transitivity.cornerAddX M k).det).det = (f M.det).det
-- Mathlib.Data.Sym.Sym2
Sym2.lift_mk : ∀ {α : Type u_1} {β : Type u_2} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (a b : α), Sym2.lift f s(a, b) = ↑f a b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.not_isCycle_one : ∀ {α : Type u_2}, ¬Equiv.Perm.IsCycle 1
-- Mathlib.Analysis.Calculus.Deriv.ZPow
DifferentiableWithinAt.zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {m : ℤ} {f : E → 𝕜} {t : Set E} {a : E},
  DifferentiableWithinAt 𝕜 f t a → f a ≠ 0 ∨ 0 ≤ m → DifferentiableWithinAt 𝕜 (fun x => f x ^ m) t a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.ofNNReal_limsup : ∀ {ι : Type u_4} {f : Filter ι} {u : ι → NNReal},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → ↑(Filter.limsup u f) = Filter.limsup (fun i => ↑(u i)) f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr'_smul : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {Q : QuadraticForm R (n → R)} (a : R), (a • Q).discr' = a ^ Fintype.card n * Q.discr'
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.str.injEq : ∀ (s s_1 : String), (Lean.JsonRpc.RequestID.str s = Lean.JsonRpc.RequestID.str s_1) = (s = s_1)
-- Lean.Data.Lsp.Ipc
/-- Merges a new `textDocument/publishDiagnostics` notification into a previously accumulated one.

- If there is no previous notification, the new one is used as-is.
- If `isIncremental?` is `true`, the new diagnostics are appended.
- Otherwise the new notification replaces the previous one.

The returned params always have `isIncremental? := some false` since they represent the full
accumulated set.
 -/
Lean.Lsp.Ipc.mergePublishDiagnosticsParams : Option Lean.Lsp.PublishDiagnosticsParams → Lean.Lsp.PublishDiagnosticsParams → Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Algebra.Order.Sub.Basic
tsub_add_eq_max : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a - b + b = max a b
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  (Std.Do.wp (MonadFunctor.monadMap (fun {β} => f) x)).apply Q = fun s =>
    (Std.Do.wp (f (x.run s))).apply
      (fun x =>
        match x with
        | (a, s) => Q.1 a s,
        Q.2)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for
`WithLp.toLp 2 ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.

This also works for other subscripts.  -/
PiLp.vecNotation : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Quotient
/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `Submodule.Quotient.mk m = x`
and `‖m‖ < ‖x‖ + ε`.  -/
Submodule.Quotient.norm_mk_lt : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
  {S : Submodule R M} (x : M ⧸ S) {ε : ℝ}, 0 < ε → ∃ m, Submodule.Quotient.mk m = x ∧ ‖m‖ < ‖x‖ + ε
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Transitivity of addition-preserving order isomorphisms  -/
OrderAddMonoidIso.trans : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : Add α] → [inst_4 : Add β] → [inst_5 : Add γ] → (α ≃+o β) → (β ≃+o γ) → α ≃+o γ
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.peekIs : (UInt8 → Bool) → Std.Internal.Parsec.ByteArray.Parser Bool
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_apply_mem : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : M), (p.projectionL q h) x ∈ p
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_alter! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : Option (β a) → Option (β a)},
  t.Balanced →
    t.Ordered →
      (Std.DTreeMap.Internal.Impl.alter! a f t).toListModel.Perm (Std.Internal.List.alterKey a f t.toListModel)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive right
cancel semigroup, if it admits an injective map that preserves `+` to an additive right cancel
semigroup.  -/
Function.Injective.addRightCancelSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : AddRightCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddRightCancelSemigroup M₁
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.iUnion_countablyGeneratedAtom : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α],
  ⋃ p, MeasurableSpace.countablyGeneratedAtom α p = Set.univ
-- Mathlib.Probability.Process.Stopping
/-- **Alias** of `MeasureTheory.isStronglyProgressive_min_stopping_time`. -/
MeasureTheory.progMeasurable_min_stopping_time : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι]
  [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStronglyProgressive f fun i ω => (min (↑i) (τ ω)).untopA
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  m.WF → ((Std.HashMap.Raw.filterMap f m).size = m.size ↔ ∀ (a : α) (h : a ∈ m), (f (m.getKey a h) m[a]).isSome = true)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.eq_of_blt_false : ∀ {a b : ℕ}, a.blt b = false → b.blt a = false → a = b
-- Std.Http.Internal.LowerCase
Std.Http.Internal.IsLowerCase.isLowerCase_empty : Std.Http.Internal.IsLowerCase ""
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.smul_map_inv_sub_map_inv_of_isCocycle₂ : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : MulAction G A] {f : G × G → A},
  groupCohomology.IsCocycle₂ f → ∀ (g : G), g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
-- Mathlib.Analysis.Normed.Group.Basic
DiscreteTopology.of_forall_le_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {r : ℝ}, 0 < r → (∀ (x : E), x ≠ 0 → r ≤ ‖x‖) → DiscreteTopology E
-- Init.Data.Range.Polymorphic.IntLemmas
Int.length_toList_rcc : ∀ {a b : ℤ}, (a...=b).toList.length = (b + 1 - a).toNat