mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- Evaluation at a point gives rise to a `C^∞⟮I, M; 𝕜⟯`-linear map between `C^∞⟮I, M; 𝕜⟯` and `𝕜`.
 -/
ContMDiffFunction.evalAt : {𝕜 : 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] →
                      (x : M) → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤ →ₗ[PointedContMDiffMap 𝕜 I M (↑⊤) x] 𝕜
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.lift_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N₁ N₂ : CategoryTheory.Mon C} (f : M ⟶ N₁) (g : M ⟶ N₂),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Mathlib.Data.Finset.Sort
Fin.castLEOrderEmb.congr_simp : ∀ {m n : ℕ} (h : n ≤ m), Fin.castLEOrderEmb h = Fin.castLEOrderEmb h
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsNonloop.of_delete : ∀ {α : Type u_1} {M : Matroid α} {e : α} {D : Set α}, (M.delete D).IsNonloop e → M.IsNonloop e
-- Mathlib.Data.Holor
Holor.mul_right_distrib : ∀ {α : Type} {ds₁ ds₂ : List ℕ} [inst : Distrib α] (x y : Holor α ds₁) (z : Holor α ds₂),
  (x + y).mul z = x.mul z + y.mul z
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_inf_stabilizer_le_stabilizer_union : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α},
  AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∪ t)
-- Lean.ErrorExplanation
Lean.getErrorExplanationRaw? : Lean.Environment → Lean.Name → Option Lean.ErrorExplanation
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`.  -/
QuotientGroup.map : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        (N : Subgroup G) →
          [nN : N.Normal] →
            (M : Subgroup H) → [inst_2 : M.Normal] → (f : G →* H) → N ≤ Subgroup.comap f M → G ⧸ N →* H ⧸ M
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.compTendsto'_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : l.Germ β) {lc : Filter γ} {g : γ → α}
  (hg : Filter.Tendsto g lc l), f.compTendsto' ↑g ⋯ = f.compTendsto g hg
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.match_1.splitter : {s : String.Slice} →
  (motive : List (String.Slice.Pattern.SearchStep s) → Sort u_1) →
    (l : List (String.Slice.Pattern.SearchStep s)) →
      (Unit → motive []) →
        ((startPos endPos : s.Pos) →
            (l : List (String.Slice.Pattern.SearchStep s)) →
              motive (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)) →
          ((p q : s.Pos) →
              (l : List (String.Slice.Pattern.SearchStep s)) →
                motive (String.Slice.Pattern.SearchStep.matched p q :: l)) →
            motive l
-- Mathlib.Topology.IsLocalHomeomorph
/-- A local homeomorphism is an open map.  -/
IsLocalHomeomorph.isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → IsOpenMap f
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} {a : M}
  (f : CategoryTheory.ShiftedHom X Y a) (F : CategoryTheory.Functor C D) [inst_5 : F.CommShift M],
  f.map F = CategoryTheory.CategoryStruct.comp (F.map f) ((CategoryTheory.Functor.commShiftIso F a).hom.app Y)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.any_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.any p it =
    forIn it { down := false } fun x x_1 =>
      if p x = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_a₄ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (S : Type s) [inst_1 : CommRing S]
  [inst_2 : Algebra R S], (W.baseChange S).a₄ = (algebraMap R S) W.a₄
-- Mathlib.Topology.NhdsWithin
preimage_nhds_within_coinduced : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α},
  a ∈ t → IsOpen t → s ∈ nhds (X a) → X ⁻¹' s ∈ nhds a
-- Init.Data.Vector.Lemmas
Vector.eq_replicate_of_mem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, (∀ b ∈ xs, b = a) → xs = Vector.replicate n a
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.instIsStableUnderRetractsOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderRetracts], P.op.IsStableUnderRetracts
-- Lean.CoreM
Lean.Core.Context.options : Lean.Core.Context → Lean.Options
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_zero_le : ∀ {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]
  (self : CategoryTheory.Triangulated.TStructure C), self.le 0 ≤ self.le 1
-- Mathlib.RingTheory.Extension.Basic
/-- The composition of two homs.  -/
Algebra.Extension.Hom.comp : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        {R'' : Type u_4} →
                          {S'' : Type u_5} →
                            [inst_6 : CommRing R''] →
                              [inst_7 : CommRing S''] →
                                [inst_8 : Algebra R'' S''] →
                                  {P'' : Algebra.Extension R'' S''} →
                                    [inst_9 : Algebra R R'] →
                                      [inst_10 : Algebra R' R''] →
                                        [inst_11 : Algebra R R''] →
                                          [inst_12 : Algebra S S'] →
                                            [inst_13 : Algebra S' S''] →
                                              [inst_14 : Algebra S S''] →
                                                [IsScalarTower R R' R''] →
                                                  [IsScalarTower S S' S''] → P'.Hom P'' → P.Hom P' → P.Hom P''
-- Mathlib.Order.Antichain
isAntichain_insert_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.eq_bot_iff_forall : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ↔ ∀ x ∈ S, x = 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.freeAddMonoidCongr_symm_of : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β) (b : β),
  (FreeAddMonoid.freeAddMonoidCongr e.symm) (FreeAddMonoid.of b) = FreeAddMonoid.of (e.symm b)
-- Mathlib.Order.Monotone.Defs
StrictAntiOn.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, StrictAntiOn g t → StrictAntiOn f s → Set.MapsTo f s t → StrictMonoOn (g ∘ f) s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i},
  (∀ (i : ι), HasFDerivAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') x) → HasFDerivAt Φ Φ' x
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.bddBelow_range : ∀ {β : Type u_2} [inst : Preorder β] [IsCodirectedOrder β] {f : ℕ → β},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) Filter.atTop f → BddBelow (Set.range f)
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.isIso_lanBaseChange_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [inst_5 : ∀ (F : CategoryTheory.Functor C₁ D), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor C₂ D), R.HasLeftKanExtension F] (F : CategoryTheory.Functor C₂ D)
  [R.HasPointwiseLeftKanExtension F] [w.GuitartExact], CategoryTheory.IsIso (w.lanBaseChange.app F)
-- Mathlib.Data.Bool.Basic
Bool.and_elim_left : ∀ {a b : Bool}, (a && b) = true → a = true
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindDomain.toIsDedekindRing : ∀ {A : Type u_2} {inst : CommRing A} [self : IsDedekindDomain A], IsDedekindRing A
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
CategoryTheory.coherentTopology.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C],
  CategoryTheory.coherentTopology C = (CategoryTheory.coherentCoverage C).toGrothendieck
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then
`F.mapAddGrp : AddGrp C ⥤ AddGrp D` is fully faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapAddGrp : {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] → F.FullyFaithful → F.mapAddGrp.FullyFaithful
-- Init.Data.Vector.Extract
Vector.map_extract : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : α → α_1} {xs : Vector α n} {i j : ℕ},
  Vector.map f (xs.extract i j) = (Vector.map f xs).extract i j
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves the action.  -/
AddActionSemiHomClass.map_vaddₛₗ : ∀ {F : Type u_8} {M : outParam (Type u_9)} {N : outParam (Type u_10)} {φ : outParam (M → N)} {X : outParam (Type u_11)}
  {Y : outParam (Type u_12)} {inst : VAdd M X} {inst_1 : VAdd N Y} {inst_2 : FunLike F X Y}
  [self : AddActionSemiHomClass F φ X Y] (f : F) (c : M) (x : X), f (c +ᵥ x) = φ c +ᵥ f x
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] {g₁ g₂ : β →*₀ γ} {f : α →*₀ β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Init.Data.Sum.Basic
Sum.swap_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β}, (Sum.inr x).swap = Sum.inl x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.finTwoArrow_apply : ∀ (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M], ⇑(ContinuousLinearEquiv.finTwoArrow R M) = fun f => (f 0, f 1)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] {f' : ι → β → α},
  HasSumUniformly f g →
    (∀ᶠ (n : Finset ι) in Filter.atTop, ∀ (b : β), ∑ i ∈ n, f i b = ∑ i ∈ n, f' i b) → HasSumUniformly f' g
-- Lean.Server.Requests
/-- Finds the first (in pre-order) snapshot task in `tree` that contains `hoverPos`
(including whitespace) and which contains an info tree, and then returns that info tree,
waiting for any snapshot tasks on the way.
Subtrees that do not contain the position are skipped without forcing their tasks.
If the caller of this function needs the correct snapshot when the cursor is on whitespace,
then this function is likely the wrong one to call, as it simply yields the first snapshot
that contains `hoverPos` in its whitespace, which is not necessarily the correct one
(e.g. it may be indentation-sensitive).
 -/
Lean.Language.SnapshotTree.findInfoTreeAtPos : Lean.FileMap → Lean.Language.SnapshotTree → String.Pos.Raw → Bool → Lean.Server.ServerTask (Option Lean.Elab.InfoTree)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.isRightAdjoint_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C]
  [inst_7 : Fact κ.IsRegular],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    W.isLocal.ι.IsRightAdjoint
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- Constructor for natural transformations to a left derived functor.  -/
CategoryTheory.Functor.leftDerivedLift : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (LF : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : L.comp LF ⟶ F) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [inst_3 : L.IsLocalization W] →
                        [LF.IsLeftDerivedFunctor α W] → (G : CategoryTheory.Functor D H) → (L.comp G ⟶ F) → (G ⟶ LF)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.tacticEval_simp : Lean.ParserDescr
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_single_mul : ∀ {Γ' : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder Γ']
  [inst_2 : AddCommGroup Γ'] [inst_3 : IsOrderedAddMonoid Γ'] {r : R} {x : HahnSeries Γ' R} {a b : Γ'},
  ((HahnSeries.single b) r * x).coeff a = r * x.coeff (a - b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.DTreeMap.Const.unitOfList l cmp).getKeyD k fallback = fallback
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
IsUniformInducing.isUniformAddGroup : ∀ {G : Type u_1} {H : Type u_2} {hom : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : UniformSpace G]
  [inst_3 : UniformSpace H] [IsUniformAddGroup H] [inst_5 : FunLike hom G H] [AddMonoidHomClass hom G H] (f : hom),
  IsUniformInducing ⇑f → IsUniformAddGroup G
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_boundary : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), Coheyting.boundary (Coheyting.boundary a) = Coheyting.boundary a
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveAt.eventually_hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [inst_5 : IsManifold I 1 M],
  IsMIntegralCurveAt γ v t₀ →
    ∀ᶠ (t : ℝ) in nhds t₀,
      HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
-- Lean.Parser.Basic
/-- Push `(Syntax.node tk <new-atom>)` onto syntax stack if parse was successful.

If `includeWhitespace` is `false`, trailing whitespace is left behind.
 -/
Lean.Parser.mkNodeToken : Lean.SyntaxNodeKind → String.Pos.Raw → optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.Birational.Dominant
/-- Dominance of the underlying morphism is invariant under equivalence of partial maps.  -/
AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_iff_of_equiv : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y),
  f.equiv g → (AlgebraicGeometry.IsDominant f.hom ↔ AlgebraicGeometry.IsDominant g.hom)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {a : α} [inst : Inhabited α],
  Std.DTreeMap.Internal.Impl.empty.getKey! a = default
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.errors : {α : Type} → Lean.Meta.RefinedDiscrTree.InitResults✝ α → Array Lean.Meta.RefinedDiscrTree.ImportFailure✝
-- Mathlib.Algebra.Ring.Ext
_private.Mathlib.Algebra.Ring.Ext.0.«termLocal_hAdd[_,_]» : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt8.toUSize_sub : ∀ (a b : UInt8), (a - b).toUSize = (a.toUSize - b.toUSize) % 256
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonMessageType : Lean.FromJson Lean.Lsp.MessageType
-- Lean.Widget.UserWidget
Lean.Widget.ToModule.mk : {α : Type u} → (α → Lean.Widget.Module) → Lean.Widget.ToModule α
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The morphism `X.normalizedChainComplex R ⟶ Y.normalizedChainComplex R` induced
by a morphism a simplicial sets `X ⟶ Y`.  -/
SSet.normalizedChainComplexMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X Y : SSet} → (X ⟶ Y) → (R : C) → X.normalizedChainComplex R ⟶ Y.normalizedChainComplex R
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.subset_pointwise_smul_iff : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S T : Submonoid M}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Init.Data.Vector.MapIdx
Vector.exists_of_mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {b : β} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β},
  b ∈ xs.mapFinIdx f → ∃ i, ∃ (h : i < n), f i xs[i] h = b
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination with `affineCombinationLineMapWeights` gives the result of
`line_map`.  -/
Finset.affineCombination_affineCombinationLineMapWeights : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i j : ι},
  i ∈ s →
    j ∈ s →
      ∀ (c : k),
        (Finset.affineCombination k s p) (Finset.affineCombinationLineMapWeights i j c) =
          (AffineMap.lineMap (p i) (p j)) c
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
Then the `Lᵖ'` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
the Fréchet derivative of `u`.

Note: The codomain of `u` needs to be a Hilbert space.
 -/
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
  {F' : Type u_5} [inst_6 : NormedAddCommGroup F'] [inst_7 : InnerProductSpace ℝ F'] {u : E → F'},
  ContDiff ℝ 1 u →
    HasCompactSupport u →
      ∀ {p p' : NNReal},
        1 ≤ p →
          0 < Module.finrank ℝ E →
            (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹ →
              MeasureTheory.eLpNorm u (↑p') μ ≤
                ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_le_right_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → ∀ {B' : Subalgebra R S}, B' ≤ B → ∀ [Module.Flat R ↥A], A.LinearDisjoint B'
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  {h : d.mid ⟶ e.mid}
  {ι_h : autoParam (CategoryTheory.CategoryStruct.comp d.ι h = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam}
  {h_π : autoParam (CategoryTheory.CategoryStruct.comp h e.π = d.π) CategoryTheory.Factorisation.Hom.h_π._autoParam}
  {h_1 : d.mid ⟶ e.mid}
  {ι_h_1 : autoParam (CategoryTheory.CategoryStruct.comp d.ι h_1 = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam}
  {h_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 e.π = d.π) CategoryTheory.Factorisation.Hom.h_π._autoParam},
  { h := h, ι_h := ι_h, h_π := h_π } = { h := h_1, ι_h := ι_h_1, h_π := h_π_1 } → h = h_1
-- Mathlib.Data.Set.Insert
Set.insert_sdiff_eq_singleton : ∀ {α : Type u_1} {a : α} {s : Set α}, a ∉ s → insert a s \ s = {a}
-- Mathlib.LinearAlgebra.Projectivization.Constructions
/-- Orthogonality on the projective plane.  -/
Projectivization.orthogonal : {F : Type u_1} →
  [inst : Field F] → {m : Type u_2} → [Fintype m] → Projectivization F (m → F) → Projectivization F (m → F) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.CategoryStruct.comp (h.descQ k ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Topology.GDelta.Basic
/-- Dense Gδ sets are residual.  -/
residual_of_dense_Gδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsGδ s → Dense s → s ∈ residual X
-- Mathlib.Algebra.Group.Basic
neg_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a + b) = -a + -b
-- Mathlib.NumberTheory.NumberField.House
/-- Let `α` be a non-zero algebraic integer. Then `α` has a conjugate `σ α` with `‖σ α‖ ≥ 1`.  -/
NumberField.exists_conjugate_one_le_norm : ∀ {K : Type u_1} [inst : Field K] [NumberField K] {α : NumberField.RingOfIntegers K}, α ≠ 0 → ∃ σ, 1 ≤ ‖σ ↑α‖