mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_inter_self : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' ∩ t = s ∩ t
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects limits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_leftOp : ∀ {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.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Mathlib.Analysis.ODE.PicardLindelof
/-- If the time-dependent vector field `f` and the curve `α` are continuous, then `f t (α t)` is the
derivative of `picard f t₀ x₀ α`.  -/
ODE.hasDerivWithinAt_picard_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {t₀ tmin tmax : ℝ},
  t₀ ∈ Set.Icc tmin tmax →
    ContinuousOn (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
      ContinuousOn α (Set.Icc tmin tmax) →
        (∀ t ∈ Set.Icc tmin tmax, α t ∈ u) →
          ∀ (x₀ : E) {t : ℝ},
            t ∈ Set.Icc tmin tmax → HasDerivWithinAt (ODE.picard f t₀ x₀ α) (f t (α t)) (Set.Icc tmin tmax) t
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.mkExtension : autoParam Lean.Name Lean.Meta.Grind.mkExtension._auto_1 → IO Lean.Meta.Grind.Extension
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_inj : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R},
  0 ≤ a → 0 ≤ b → (a * a = b * b ↔ a = b)
-- Mathlib.Analysis.Complex.Harmonic.Analytic
/-- If `f : ℂ → ℝ` is harmonic at `x`, then `∂f/∂1 - I • ∂f/∂I` is complex analytic at `x`.
 -/
HarmonicAt.analyticAt_complex_partial : ∀ {f : ℂ → ℝ} {x : ℂ},
  InnerProductSpace.HarmonicAt f x →
    AnalyticAt ℂ (fun z => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x
-- Mathlib.Algebra.Order.Group.Abs
div_le_of_mabs_div_le_right : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G}, |a / b|ₘ ≤ c → a / c ≤ b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.evalTactic : Lean.Meta.Grind.Goal → Lean.TSyntax `grind → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal)
-- Mathlib.RepresentationTheory.Invariants
/-- The invariants of the representation `linHom X.ρ Y.ρ` correspond to the representation
homomorphisms from `X` to `Y`.  -/
Representation.linHom.invariantsEquivFDRepHom : {k : Type u} →
  [inst : Field k] →
    {G : Type v} → [inst_1 : Group G] → (X Y : FDRep k G) → ↥(Representation.linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y
-- Init.Data.SInt.Bitwise
Int32.xor_not : ∀ {a b : Int32}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Mathlib.Logic.Function.Basic
Function.Injective.extend_comp : ∀ {γ : Sort u_3} {α₁ : Sort u_4} {α₂ : Sort u_5} {α₃ : Sort u_6} {f₁₂ : α₁ → α₂},
  Function.Injective f₁₂ →
    ∀ {f₂₃ : α₂ → α₃},
      Function.Injective f₂₃ →
        ∀ (g : α₁ → γ) (e' : α₃ → γ),
          Function.extend (f₂₃ ∘ f₁₂) g e' = Function.extend f₂₃ (Function.extend f₁₂ g (e' ∘ f₂₃)) e'
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.Const.IteratedSlowUnitInsertionInto : {α : Type u} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Type (max 0 u)
-- Lean.Parser.Command
Lean.Parser.Command.unsafe : Lean.Parser.Parser
-- Mathlib.Analysis.Analytic.Constructions
/-- A function is analytic at a point iff it is analytic after scalar
multiplication with a non-vanishing analytic function.  -/
analyticAt_iff_analytic_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕝 : Type u_8}
  [inst_5 : NormedDivisionRing 𝕝] [inst_6 : NormedAlgebra 𝕜 𝕝] [inst_7 : Module 𝕝 F] [IsBoundedSMul 𝕝 F]
  [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E},
  AnalyticAt 𝕜 f z → f z ≠ 0 → (AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z)
-- Mathlib.Topology.Constructible
IsRetrocompact.inter_isOpen : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  IsRetrocompact s → IsRetrocompact t → IsOpen t → IsRetrocompact (s ∩ t)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- This is an auxiliary lemma used to prove `RelCWComplex.eq_of_eq_union_iUnion`.  -/
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.RelCWComplex.subset_of_eq_union_iUnion : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (I J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)),
  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j →
    ∀ (n : ℕ), I n ⊆ J n
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instOrderTop : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → OrderTop (ClosedSubmodule R M)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasLimit_equivalence_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J)
  [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasLimit (e.functor.comp F)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {s : Set E}
  {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G},
  HasFPowerSeriesWithinAt f p s e →
    HasFPowerSeriesWithinAt g q s e → HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_le_log_iff : ∀ {x y : ℝ}, 0 < x → 0 < y → (Real.log x ≤ Real.log y ↔ x ≤ y)
-- Mathlib.Algebra.Category.CommBialgCat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommBialgCat.Hom.Simps.hom : {R : Type u} → [inst : CommRing R] → (A B : CommBialgCat R) → A.Hom B → ↑A →ₐc[R] ↑B
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `MakesOverArrow η s` in `s`.  -/
CategoryTheory.OverPresheafAux.MakesOverArrow.map₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {X Y : C} (f : X ⟶ Y) {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s →
    ∀ {u : F.obj (Opposite.op Y)},
      CategoryTheory.OverPresheafAux.MakesOverArrow η t u →
        CategoryTheory.OverPresheafAux.MakesOverArrow η s ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) u)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_sub_pi_div_two : ∀ (θ : Real.Angle), (θ - ↑(Real.pi / 2)).sin = -θ.cos
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
CategoryTheory.Limits.WalkingMultispan.instFintype : {J : CategoryTheory.Limits.MultispanShape} →
  [Fintype J.L] → [Fintype J.R] → Fintype (CategoryTheory.Limits.WalkingMultispan J)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → Option (γ a)} (h : t.WF), (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.size ≤ t.size
-- Init.Prelude
/-- Adds the ability to access a read-only value of type `ρ` to a monad. The value can be locally
overridden by `withReader`, but it cannot be mutated.

Actions in the resulting monad are functions that take the local value as a parameter, returning
ordinary actions in `m`.
 -/
ReaderT : Type u → (Type u → Type v) → Type u → Type (max u v)
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.classifySingleNumber : ℕ → Option Std.Time.Number
-- Init.Data.SInt.Lemmas
ISize.toInt_minValue : ISize.minValue.toInt = -2 ^ (System.Platform.numBits - 1)
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- verschiebung is a natural transformation  -/
WittVector.map_verschiebung : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [hp : Fact (Nat.Prime p)]
  (f : R →+* S) (x : WittVector p R),
  (WittVector.map f) (WittVector.verschiebung x) = WittVector.verschiebung ((WittVector.map f) x)
-- Mathlib.Order.SupClosed
supClosed_empty : ∀ {α : Type u_3} [inst : SemilatticeSup α], SupClosed ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexCellsEquiv_symm_apply_j : ∀ {X : SSet} (s : X.N), (SSet.relativeCellComplexCellsEquiv.symm s).j = s.dim
-- Mathlib.Analysis.Seminorm
/-- Let `p` be a seminorm on a vector space over a `NormedField`.
If there is a scalar `c` with `‖c‖>1`, then any `x` such that `p x ≠ 0` can be
moved by scalar multiplication to any `p`-shell of width `‖c‖`. Also recap information on the
value of `p` on the rescaling element that shows up in applications.  -/
Seminorm.rescale_to_shell_zpow : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {x : E}, p x ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ ε / ‖c‖ ≤ p (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
-- Mathlib.Order.Filter.Map
Filter.mem_comap'' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α}, s ∈ Filter.comap f l ↔ Set.kernImage f s ∈ l
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Two spheres intersect in at most two points in two-dimensional space; this is a version of
`eq_of_dist_eq_of_dist_eq_of_finrank_eq_two` for bundled spheres.  -/
EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] [FiniteDimensional ℝ V],
  Module.finrank ℝ V = 2 →
    ∀ {s₁ s₂ : EuclideanGeometry.Sphere P} {p₁ p₂ p : P},
      s₁ ≠ s₂ → p₁ ≠ p₂ → p₁ ∈ s₁ → p₂ ∈ s₁ → p ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → p ∈ s₂ → p = p₁ ∨ p = p₂
-- Mathlib.Data.Set.Image
Function.Injective.image_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (Set.image f)
-- Mathlib.SetTheory.Lists
/-- `Finsets` are defined via equivalence classes of `Lists`  -/
Finsets : Type u_2 → Type u_2
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffMulOfNatWithTopENatOfContinuousMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContinuousMul G], ContMDiffMul I 0 G
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s g → StrictConcaveOn 𝕜 s (f - g)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.op_X₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.RightResolution X₂), L.op.X₁ = Opposite.op L.X₁
-- Mathlib.Data.Set.Function
Set.EqOn.mapsTo_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ s → (Set.MapsTo f₁ s t ↔ Set.MapsTo f₂ s t)
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_zero_measure : ∀ {α : Type u_1} {mα : MeasurableSpace α} (f : α → ℝ), MeasureTheory.Measure.tilted 0 f = 0
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.toBddDistLat : FinBddDistLat → BddDistLat
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a nonempty preorder with no minimal elements, then there exists a strictly antitone
function `ℕ → α`.  -/
Nat.exists_strictAnti : ∀ (α : Type u) [inst : Preorder α] [Nonempty α] [NoMinOrder α], ∃ f, StrictAnti f
-- Init.Data.UInt.Bitwise
USize.toBitVec_shiftRight : ∀ (a b : USize), (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.simp : Lean.Elab.Tactic.SimpKind
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.responseError : Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option Lean.Json → Lean.JsonRpc.MessageMetaData
-- Mathlib.Data.Quot
Setoid.ext : ∀ {α : Sort u_3} {s t : Setoid α}, (∀ (a b : α), s a b ↔ t a b) → s = t
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_inf : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G}, ↑(U ⊓ V) = ↑U ∩ ↑V
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- If `f: M → N` and `g: M' × N'` are smooth embeddings, respectively,
then so is `f × g: M × M' → N × N'`.  -/
Manifold.IsSmoothEmbedding.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} {E₄ : Type u_5}
  [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₂]
  [inst_4 : NormedSpace 𝕜 E₂] [inst_5 : NormedAddCommGroup E₃] [inst_6 : NormedSpace 𝕜 E₃]
  [inst_7 : NormedAddCommGroup E₄] [inst_8 : NormedSpace 𝕜 E₄] {H : Type u_6} {H' : Type u_7} {G : Type u_8}
  {G' : Type u_9} [inst_9 : TopologicalSpace H] [inst_10 : TopologicalSpace H'] [inst_11 : TopologicalSpace G]
  [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E₁ H} {I' : ModelWithCorners 𝕜 E₂ H'}
  {J : ModelWithCorners 𝕜 E₃ G} {J' : ModelWithCorners 𝕜 E₄ G'} {M : Type u_10} {M' : Type u_11} {N : Type u_12}
  {N' : Type u_13} [inst_13 : TopologicalSpace M] [inst_14 : ChartedSpace H M] [inst_15 : TopologicalSpace M']
  [inst_16 : ChartedSpace H' M'] [inst_17 : TopologicalSpace N] [inst_18 : ChartedSpace G N]
  [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'}
  [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'],
  Manifold.IsSmoothEmbedding I J n f →
    Manifold.IsSmoothEmbedding I' J' n g → Manifold.IsSmoothEmbedding (I.prod I') (J.prod J') n (Prod.map f g)
-- Init.Data.List.Lemmas
List.prod_eq_foldl : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {xs : List α}, xs.prod = List.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Init.Data.List.Basic
List.foldr_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1}, List.foldr f b [] = b
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.dfinsupp : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Flat R (M i)], Module.Flat R (Π₀ (i : ι), M i)
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The Lie algebra of type Cₙ, isomorphic to sp(2n).  -/
CartanMatrix.cₙ : (R : Type u_1) → [CommRing R] → ℕ → Type u_1
-- ProofWidgets.Util
/-- Collapse adjacent `inl (_ : α)`s into a `β` using `f`.
For example, `#[.inl a₁, .inl a₂, .inr b, .inl a₃] ↦ #[← f #[a₁, a₂], b, ← f #[a₃]]`.  -/
ProofWidgets.Util.foldInlsM : {α β : Type u_1} → {m : Type u_1 → Type u_2} → [Monad m] → Array (α ⊕ β) → (Array α → m β) → m (Array β)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.tensorProductComm_eq_refl : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], TensorProduct.comm R M M = LinearEquiv.refl R (TensorProduct R M M)
-- Mathlib.Analysis.Analytic.Order
analyticOrderNatAt_of_not_analyticAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, ¬AnalyticAt 𝕜 f z₀ → analyticOrderNatAt f z₀ = 0
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processUnicode : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.RingTheory.Discriminant
/-- Two (finite) ℤ-bases have the same discriminant.  -/
Algebra.discr_eq_discr : ∀ (A : Type u) {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : Fintype ι]
  (b b' : Module.Basis ι ℤ A), Algebra.discr ℤ ⇑b = Algebra.discr ℤ ⇑b'
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeRightOp_id : ∀ {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.NatTrans.removeRightOp (CategoryTheory.CategoryStruct.id F.rightOp) =
    CategoryTheory.CategoryStruct.id F
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.smul` -/
AEMeasurable.fun_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableSMul₂ M X] {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i • g i) μ
-- Mathlib.Dynamics.Minimal
IsCompact.exists_finite_cover_vadd : ∀ (G : Type u_2) {α : Type u_3} [inst : AddGroup G] [inst_1 : TopologicalSpace α] [inst_2 : AddAction G α]
  [AddAction.IsMinimal G α] [ContinuousConstVAdd G α] {K U : Set α},
  IsCompact K → IsOpen U → U.Nonempty → ∃ I, K ⊆ ⋃ g ∈ I, g +ᵥ U
-- Mathlib.Data.Nat.Factorial.Basic
Nat.succ_descFactorial : ∀ (n k : ℕ), (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α × β → α × β
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.epi_iff_surjective : ∀ {A B : CommGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp inl (hP.desc h k w) = h
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHavePatDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.FiberBundle.Basic
/-- Core data defining a locally trivial bundle with fiber `F` over a topological
space `B`. Note that "bundle" is used in its mathematical sense. This is the (computer science)
bundled version, i.e., all the relevant data is contained in the following structure. A family of
local trivializations is indexed by a type `ι`, on open subsets `baseSet i` for each `i : ι`.
Trivialization changes from `i` to `j` are given by continuous maps `coordChange i j` from
`baseSet i ∩ baseSet j` to the set of homeomorphisms of `F`, but we express them as maps
`B → F → F` and require continuity on `(baseSet i ∩ baseSet j) × F` to avoid the topology on the
space of continuous maps on `F`.  -/
FiberBundleCore : Type u_5 → (B : Type u_6) → [TopologicalSpace B] → (F : Type u_7) → [TopologicalSpace F] → Type (max (max u_5 u_6) u_7)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_obj_addGrp_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddGrpObj.neg = F.map CategoryTheory.AddGrpObj.neg
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.coe_vanishingIdeal : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
  ↑(PrimeSpectrum.vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asIdeal}
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Constructor for `wp`  -/
MvPFunctor.wpMk : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} → (a : P.A) → (f : P.last.B a → P.last.W) → TypeVec.Arrow (P.WPath (WType.mk a f)) α → P.W α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Util.0.Lean.Grind.Linarith.Poly.eval?.go : Lean.PArray ℚ → ℚ → Lean.Grind.Linarith.Poly → Option ℚ
-- Mathlib.Data.Complex.Basic
Complex.instMul : Mul ℂ
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instOne.eq_1 : ∀ (M : Type u_4) [inst : AddZero M], AddMonoid.End.instOne M = { one := AddMonoidHom.id M }
-- Mathlib.Order.JordanHolder
/-- Given a `CompositionSeries`, `s`, and an element `x`
such that `x` is maximal inside `s.last` there is a series, `t`,
such that `t.last = x`, `t.head = s.head`
and `snoc t s.last _` is equivalent to `s`.  -/
CompositionSeries.exists_last_eq_snoc_equivalent : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) (x : X)
  (hm : JordanHolderLattice.IsMaximal x (RelSeries.last s)),
  RelSeries.head s ≤ x →
    ∃ t,
      RelSeries.head t = RelSeries.head s ∧
        t.length + 1 = s.length ∧ ∃ (htx : RelSeries.last t = x), s.Equivalent (RelSeries.snoc t (RelSeries.last s) ⋯)
-- Mathlib.Data.List.Cycle
Cycle.card_toMultiset : ∀ {α : Type u_1} (s : Cycle α), s.toMultiset.card = s.length
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- The logarithmic counting function of a singleton is big-O of `log`. This is the qualitative
consequence of `logCounting_single_eq_log_sub_const`.
 -/
Function.locallyFinsuppWithin.logCounting_single_isBigO_log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : DecidableEq E] [inst_2 : ProperSpace E] {e : E} {n : ℤ},
  Function.locallyFinsuppWithin.logCounting (Function.locallyFinsuppWithin.single e n) =O[Filter.atTop] Real.log
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃ObjProdComp_hom_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {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_6, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_7, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_8, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_9, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E)
  (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F₁.curry₃ObjProdComp F₂ F₃ G).hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Functor.curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X_1).obj X_2)
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ico_coe_top : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ico ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ici a)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.prec : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g → Nat.Primrec (Nat.unpaired fun z n => Nat.rec (f z) (fun y IH => g (Nat.pair z (Nat.pair y IH))) n)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.differentiableAt_Gamma_one : DifferentiableAt ℂ Complex.Gamma 1