mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_inf_atTop : ∀ {α : Type u_6} {β : Type u_7} [inst : SemilatticeInf α] {f g : β → α} (F : Filter β),
  Filter.Tendsto f F Filter.atTop → Filter.Tendsto g F Filter.atTop → Filter.Tendsto (fun x => f x ⊓ g x) F Filter.atTop
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- If `q ≠ 0`, then `padicNorm p q ≠ 0`.  -/
padicNorm.nonzero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ}, q ≠ 0 → padicNorm p q ≠ 0
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_const_smul_left`. -/
Asymptotics.IsTheta.of_const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
  c ≠ 0 → (fun x => c • f' x) =Θ[l] g → f' =Θ[l] g
-- Mathlib.Topology.UniformSpace.Basic
Filter.HasBasis.mem_uniformity_iff : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {p : β → Prop} {s : β → SetRel α α},
  (uniformity α).HasBasis p s → ∀ {t : SetRel α α}, t ∈ uniformity α ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instZero : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Zero (E →ₛₗ.[σ] F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y} (φ : S ⟶ S')
  (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).map φ).snd.app X_1 =
    φ.snd.app (U.obj X_1)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_sub_goldenConj : Real.goldenRatio - Real.goldenConj = √5
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivAt.comp_hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {s : Set E}
  {g : F → G} {g' : F →L[𝕜] G},
  HasFDerivAt g g' (f x) → HasFDerivWithinAt f f' s x → HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.View.mk : {α : Type u} →
  {β : α → Type v} →
    {size : ℕ} → (k : α) → β k → Std.DTreeMap.Internal.Impl.Tree α β size → Std.DTreeMap.Internal.Impl.View α β size
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_bot : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, x ∈ ⊥ ↔ x = 0
-- Mathlib.Tactic.Module
/-- Given a goal which is an equality in a type `M` (with `M` an `AddCommMonoid`), parse the LHS and
RHS of the goal as linear combinations of `M`-atoms over some semiring `R`, and reduce the goal to
the respective equalities of the `R`-coefficients of each atom.  -/
Mathlib.Tactic.Module.matchScalars : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Std.Http.Server
Std.Http.Server.mk : Std.CancellationContext →
  Std.Mutex ℕ →
    Option Std.Semaphore → Std.Channel Unit → Std.Http.Config → Option Std.Net.SocketAddress → Std.Http.Server
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.X : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → {c : ComplexShape ι} → HomologicalComplex V c → ι → V
-- Mathlib.Data.Fin.VecNotation
Matrix.vecCons.eq_1 : ∀ {α : Type u} {n : ℕ} (h : α) (t : Fin n → α), Matrix.vecCons h t = Fin.cons h t
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)) {δ : ι → Type u_5}
  (φ : (i : ι) → δ i → α) (𝔗 : (i : ι) → Set (Set (δ i))),
  (∀ (i : ι), Set.MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖) →
    (∀ (i : ι), Set.MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)) →
      (∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, Set.range (φ i)) →
        UniformOnFun.uniformSpace α β 𝔖 =
          ⨅ i,
            UniformSpace.comap (⇑(UniformOnFun.ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(UniformOnFun.toFun 𝔖))
              (UniformOnFun.uniformSpace (δ i) β (𝔗 i))
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal], CategoryTheory.NatTrans.IsMonoidal e.unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {he : t.isEmpty = false}, t.getKey! (t.maxKey he) = t.maxKey he
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l)[k]? = none
-- Mathlib.Data.Set.Finite.Basic
Finset.finite_toSet_toFinset : ∀ {α : Type u} (s : Finset α), ⋯.toFinset = s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_of_natDegree_lt_card_of_eval_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (p q : Polynomial R) {ι : Type u_2} [inst_2 : Fintype ι] {f : ι → R},
  Function.Injective f →
    (∀ (i : ι), Polynomial.eval (f i) p = Polynomial.eval (f i) q) →
      max p.natDegree q.natDegree < Fintype.card ι → p = q
-- Init.Data.SInt.Lemmas
Int64.le_antisymm : ∀ {a b : Int64}, a ≤ b → b ≤ a → a = b
-- Mathlib.Algebra.Group.Action.Defs
AddCommute.vadd_left : ∀ {M : Type u_1} {α : Type u_5} [inst : VAdd M α] [inst_1 : Add α] [VAddCommClass M α α] [VAddAssocClass M α α]
  {a b : α}, AddCommute a b → ∀ (r : M), AddCommute (r +ᵥ a) b
-- Init.Data.List.Lemmas
List.cons_eq_append_iff : ∀ {α : Type u_1} {x : α} {cs as bs : List α},
  x :: cs = as ++ bs ↔ as = [] ∧ bs = x :: cs ∨ ∃ as', as = x :: as' ∧ cs = as' ++ bs
-- Mathlib.Data.Set.Basic
Subsingleton.mem_iff_nonempty : ∀ {α : Type u_2} [Subsingleton α] {s : Set α} {x : α}, x ∈ s ↔ s.Nonempty
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instZero : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Zero (TruncatedWittVector p n R)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedGoal : Inhabited Lean.Meta.Grind.Goal
-- Init.Data.Option.Lemmas
Option.pbind_some' : ∀ {α : Type u_1} {x : Option α} {a : α} {α_1 : Type u_2} {f : (a : α) → x = some a → Option α_1} (h : x = some a),
  x.pbind f = f a h
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.loop : (n : ℕ) → ((i : ℕ) → i < n → Bool) → (i : ℕ) → i ≤ n → Bool
-- Mathlib.Data.List.Rotate
/-- A version of `List.get_rotate` that represents `List.get l` in terms of
`List.get (List.rotate l n)`, not vice versa. Can be used instead of rewriting `List.get_rotate`
from right to left.  -/
List.get_eq_get_rotate : ∀ {α : Type u} (l : List α) (n : ℕ) (k : Fin l.length),
  l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩
-- Mathlib.Algebra.Group.Action.Defs
AddSemiconjBy.vadd_right : ∀ {M : Type u_1} {α : Type u_5} [inst : VAdd M α] [inst_1 : Add α] [VAddCommClass M α α] [VAddAssocClass M α α]
  {x a b : α}, AddSemiconjBy x a b → ∀ (r : M), AddSemiconjBy x (r +ᵥ a) (r +ᵥ b)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.Cache.get?.match_1.eq_1 : ∀ {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w)
  (motive : Option (Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → Sort u_1)
  (refs : Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w)
  (h_1 :
    (refs_1 : Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → some refs = some refs_1 → motive (some refs_1))
  (h_2 : some refs = none → motive none),
  (match h : some refs with
    | some refs_1 => h_1 refs_1 h
    | none => h_2 h) =
    h_1 refs ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_inf_iSup : ∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α},
  (⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.post : Lean.Meta.Sym.DSimp.DSimproc
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- The free locus of a module, i.e. the set of primes `p` such that `Mₚ` is free over `Rₚ`.  -/
Module.freeLocus : (R : Type uR) → (M : Type uM) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Set (PrimeSpectrum R)
-- Lean.CoreM
Lean.Core.Cache.instLevelValue : Lean.Core.Cache → Lean.Core.InstantiateLevelCache
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
_private.Mathlib.MeasureTheory.VectorMeasure.SetIntegral.0.MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnion_nat : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {s : ℕ → Set X},
  (∀ (i : ℕ), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      μ.IntegrableOn f (⋃ i, s i) → HasSum (fun n => ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensorHom_def : ∀ {R : Type u} [inst : CommRing R] {X₁ Y₁ X₂ Y₂ : ModuleCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    ModuleCat.ofHom (TensorProduct.map (ModuleCat.Hom.hom f) (ModuleCat.Hom.hom g))
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.symm_mulRight_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u : ↥(unitary A)) (x : A),
  (Unitary.mulRight R u).symm x = x * star ↑u
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.r.setoid : {R : Type u} →
  [inst : CommSemiring R] →
    (S : Submonoid R) → (M : Type v) → [inst_1 : AddCommMonoid M] → [Module R M] → Setoid (M × ↥S)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_comap : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : AddGroup N]
  [inst_3 : TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f),
  ↑(OpenAddSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H
-- Mathlib.Order.Concept
Concept.intent_sSup : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)), (sSup S).intent = ⋂ i ∈ S, i.intent
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.Hom.ext_iff : ∀ {A B : ProfiniteGrp.{u}} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_biUnion_of_pairwise_eq_one : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {s : Finset κ}
  {t : κ → Finset ι},
  ((↑s).Pairwise fun i j => ∀ k ∈ t i ∩ t j, f k = 1) → ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A monoid homomorphism `M →* N` can equivalently be viewed as a monoid homomorphism
`Mᵐᵒᵖ →* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
MonoidHom.op : {M : Type u_3} → {N : Type u_4} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ)
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_succ : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → Option α}, Fin.findSome? f = (f 0).or (Fin.findSome? fun x => f x.succ)
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_add_rank_le_rank_prod : ∀ (R : Type u) (M : Type v) {M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M] [inst_4 : Module R M₁] [Nontrivial R],
  Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G),
  Finite (DoubleCoset.Quotient ↑H ↑K) ↔ ∃ I, ⋃ i ∈ I, DoubleCoset.quotToDoubleCoset H K i = Set.univ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances.0.termσ : Lean.ParserDescr
-- Init.Core
Std.Antisymm.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a b : α), r a b → r b a → a = b) → Std.Antisymm r
-- Mathlib.Topology.Maps.Basic
IsClosedMap.comap_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → Continuous f → ∀ (y : Y), Filter.comap f (nhds y) = nhdsSet (f ⁻¹' {y})
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u},
  p.IsCycle → p.toSubgraph.neighborSet u = {p.snd, p.penultimate}
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nfBelow_iff_topBelow : ∀ {b : ONote} [b.NF] {o : ONote}, o.NFBelow b.repr ↔ o.NF ∧ b.TopBelow o
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_mono_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → μ s₁ = ⊤ → μ s₂ = ⊤
-- Mathlib.SetTheory.Ordinal.Veblen
/-- The Feferman-Schütte ordinal `Γ₀` is the smallest fixed point of `veblen · 0`, i.e. the supremum
of `veblen ε₀ 0`, `veblen (veblen ε₀ 0) 0`, etc. 

Conventions for notations in identifiers:

 * The recommended spelling of `Γ₀` in identifiers is `gamma_zero`. -/
Ordinal.termΓ₀ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_le_one : ∀ {α : Type u} [inst : One α] {a : α} [inst_1 : LE α], ↑a ≤ 1 ↔ a ≤ 1
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P → ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasGaussianLaw (X - Y) P
-- Batteries.Data.DList.Lemmas
Batteries.DList.singleton.eq_1 : ∀ {α : Type u} (a : α), Batteries.DList.singleton a = { apply := fun t => a :: t, invariant := ⋯ }
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)
      (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv =
    AlgebraicGeometry.Scheme.Hom.app f U
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The homogeneous differential as a linear map, denoted as `𝒅` within the `Manifold` namespace.  -/
Manifold.«term𝒅» : Lean.ParserDescr
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
compactly-supported function `u` on `ℝⁿ`, for `n ≥ 2`.  (More literally we encode `ℝⁿ` as
`ι → ℝ` where `n := #ι` is finite and at least 2.)  Then the Lebesgue integral of the pointwise
expression `|u x| ^ (n / (n - 1))` is bounded above by the `n / (n - 1)`-th power of the Lebesgue
integral of the Fréchet derivative of `u`.

For a basis-free version, see `lintegral_pow_le_pow_lintegral_fderiv`.  -/
MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : Fintype ι] {p : ℝ},
  (↑(Fintype.card ι)).HolderConjugate p →
    ∀ {u : (ι → ℝ) → F},
      ContDiff ℝ 1 u → HasCompactSupport u → ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤ (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- The head term of the sequence with head of `v` is just the integer part of `v`.  -/
GenContFract.IntFractPair.seq1_fst_eq_of : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  (GenContFract.IntFractPair.seq1 v).1 = GenContFract.IntFractPair.of v
-- Mathlib.Algebra.Star.Conjneg
conjneg_injective : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R],
  Function.Injective conjneg
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Let `p` be a predicate on `Box ι`, let `I` be a box. Suppose that the following two properties
hold true.

* Consider a smaller box `J ≤ I`. The hyperplanes passing through the center of `J` split it into
  `2 ^ n` boxes. If `p` holds true on each of these boxes, then it true on `J`.
* For each `z` in the closed box `I.Icc` there exists a neighborhood `U` of `z` within `I.Icc` such
  that for every box `J ≤ I` such that `z ∈ J.Icc ⊆ U`, if `J` is homothetic to `I` with a
  coefficient of the form `1 / 2 ^ m`, then `p` is true on `J`.

Then `p I` is true. See also `BoxIntegral.Box.subbox_induction_on'` for a version using
`BoxIntegral.Box.splitCenterBox` instead of `BoxIntegral.Prepartition.splitCenter`.  -/
BoxIntegral.Box.subbox_induction_on : ∀ {ι : Type u_1} [inst : Fintype ι] {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι),
  (∀ J ≤ I, (∀ J' ∈ BoxIntegral.Prepartition.splitCenter J, p J') → p J) →
    (∀ z ∈ BoxIntegral.Box.Icc I,
        ∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I),
          ∀ J ≤ I,
            ∀ (m : ℕ),
              z ∈ BoxIntegral.Box.Icc J →
                BoxIntegral.Box.Icc J ⊆ U →
                  (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) →
      p I
-- Mathlib.Computability.Reduce
_private.Mathlib.Computability.Reduce.0.ManyOneDegree.le_antisymm : ∀ {d₁ d₂ : ManyOneDegree}, d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, m.isEmpty = true → m[a]! = default
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.not_matchesAt_skipPrefixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] (s : String.Slice),
  ¬String.Slice.Pattern.Model.MatchesAt pat (s.skipPrefixWhile pat)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableSub₂ G], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f - g) μ
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.ι_f_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  I.ι.f (n + 1) = 0
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.const_smul_section : ∀ {𝕜 : 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] {a : 𝕜} {s : (x : M) → V x} {u : Set M},
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (a • s) x⟩) u
-- Mathlib.GroupTheory.Perm.Cycle.Factors
_private.Mathlib.GroupTheory.Perm.Cycle.Factors.0.Equiv.Perm.mem_support_cycleOf_iff_aux : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [inst : DecidableRel f.SameCycle] [inst_1 : DecidableEq α]
  [inst_2 : Fintype α], y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.IsFunc.eq_1 : ∀ (x y f : ZFSet.{u}), x.IsFunc y f = (f ⊆ x.prod y ∧ ∀ z ∈ x, ∃! w, z.pair w ∈ f)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey.mk.inj : ∀ {constName constName_1 : Lean.Name},
  { constName := constName } = { constName := constName_1 } → constName = constName_1
-- Aesop.EMap
Aesop.EMap.insertNew : {m : Type → Type u_1} →
  [Monad m] → [MonadLiftT Lean.MetaM m] → {α : Type} → Lean.Expr → α → Aesop.EMap α → m (Aesop.EMap α)
-- Aesop.RuleSet
Aesop.LocalRuleSet.modifyBase : (Aesop.BaseRuleSet → Aesop.BaseRuleSet) → Aesop.LocalRuleSet → Aesop.LocalRuleSet
-- Mathlib.Data.Nat.Fib.Basic
/-- Implementation of the Fibonacci sequence satisfying
`fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1)`.

*Note:* We use a stream iterator for better performance when compared to the naive recursive
implementation.
 -/
Nat.fib : ℕ → ℕ
-- Mathlib.Topology.Sets.Closeds
/-- The map on irreducible closed sets induced by a continuous map `f`.  -/
TopologicalSpace.IrreducibleCloseds.map : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : β → α) → Continuous f → TopologicalSpace.IrreducibleCloseds β → TopologicalSpace.IrreducibleCloseds α
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_inv : ∀ (R θ : ℝ), (circleMap 0 R θ)⁻¹ = circleMap 0 R⁻¹ (-θ)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.starRing : {R : Type v} → [inst : NonAssocSemiring R] → [inst_1 : StarRing R] → (s : StarSubsemiring R) → StarRing ↥s
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.TransversalPair.nonempty : ∀ (G : Type u_1) [inst : Group G] (A B : Subgroup G), Nonempty (HNNExtension.NormalWord.TransversalPair G A B)
-- Std.Http.Data.Method
/-- Check out a version-controlled resource for modification.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.8
 -/
Std.Http.Method.checkout : Std.Http.Method
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.dNext_succ_chainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (i : ℕ),
  (dNext (i + 1)) f = CategoryTheory.CategoryStruct.comp (P.d (i + 1) i) (f i (i + 1))
-- Init.Control.Except
ExceptT.instMonad : {ε : Type u} → {m : Type u → Type v} → [Monad m] → Monad (ExceptT ε m)
-- Mathlib.Data.ENNReal.Action
ENNReal.nnreal_smul_ne_top_iff : ∀ {x : NNReal} {y : ENNReal}, x ≠ 0 → (x • y ≠ ⊤ ↔ y ≠ ⊤)