mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Disjoint
Multiset.disjoint_toFinset : ∀ {α : Type u_2} [inst : DecidableEq α] {m1 m2 : Multiset α}, Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2
-- Init.Data.BitVec.Bitblast
BitVec.bit_not_eq_not : ∀ {w : ℕ} (x : BitVec w), (BitVec.iunfoldr (fun i c => (c, !x[i])) ()).2 = ~~~x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Iic_eq_integral_Iio : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsuppIso_apply : ∀ (R : Type u) [inst : Semiring R] (self : Polynomial R), (Polynomial.toFinsuppIso R) self = self.toFinsupp
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- Let `e` be an open partial homeomorphism of `B × F`.  Suppose that at every point `p` in the
source of `e`, there is some neighbourhood `s` of `p` on which `e` is equal to a bi-`C^n` fiberwise
linear open partial homeomorphism.
Then the source of `e` is of the form `U ×ˢ univ`, for some set `U` in `B`, and, at any point `x` in
`U`, admits a neighbourhood `u` of `x` such that `e` is equal on `u ×ˢ univ` to some bi-`C^n`
fiberwise linear open partial homeomorphism.  -/
ContMDiffFiberwiseLinear.locality_aux₁ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB]
  [inst_5 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B]
  {IB : ModelWithCorners 𝕜 EB HB} (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)),
  (∀ p ∈ e.source,
      ∃ s,
        IsOpen s ∧
          p ∈ s ∧
            ∃ φ u,
              ∃ (hu : IsOpen u) (hφ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) u) (h2φ :
                ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) u),
                (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)) →
    ∃ U,
      e.source = U ×ˢ Set.univ ∧
        ∀ x ∈ U,
          ∃ φ u,
            ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
              ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) u) (h2φ :
              ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) u),
              (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
isEmpty_algebraicIndependent : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  ¬Function.Injective ⇑(algebraMap R A) → IsEmpty { s // AlgebraicIndepOn R id s }
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The range of the inclusion map is a normal additive subgroup.  -/
AddGroupExtension.normal_inl_range : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G), S.inl.range.Normal
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_setWidth_eq_self : ∀ {w : ℕ} {a : BitVec w} {w' : ℕ}, a < BitVec.twoPow w w' → BitVec.setWidth w (BitVec.setWidth w' a) = a
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.starMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Mul β] → [inst_3 : ContinuousMul β] → [inst_4 : StarMul β] → [ContinuousStar β] → StarMul C(α, β)
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.isMinor : ∀ {α : Type u_1} {M N : Matroid α}, N <m M → N ≤m M
-- Init.Data.String.Termination
String.Slice.Pos.Splits.remainingBytes_eq : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.remainingBytes = t₂.utf8ByteSize
-- Mathlib.Topology.Bases
Set.Finite.isSeparable : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α}, s.Finite → TopologicalSpace.IsSeparable s
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.algEquivResidueFieldOfField_apply : ∀ {k : Type u_5} [inst : Field k] (p : Ideal k) [inst_1 : p.IsPrime] (x : k),
  p.algEquivResidueFieldOfField x = (algebraMap k p.ResidueField) x
-- Mathlib.Algebra.Order.Group.Nat
Nat.instIsOrderedAddMonoid : IsOrderedAddMonoid ℕ
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The logarithm as an equivalence between `(Gᵐ⁰)ˣ` and `G`.  -/
WithZero.logEquiv : {G : Type u_5} → [inst : AddGroup G] → (WithZero (Multiplicative G))ˣ ≃ G
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Any component `f : Y ⟶ X` of the sieve `S` induces a natural transformation from `yoneda.obj Y`
to the presheaf induced by `S`.  -/
CategoryTheory.Sieve.toFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Sieve X) → {Y : C} → (f : Y ⟶ X) → S.arrows f → (CategoryTheory.yoneda.obj Y ⟶ S.functor)
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f))
      (F.mapDerivedCategoryFactors.hom.app Y) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X)
      (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f))
-- Mathlib.Data.Seq.Computation
Computation.get_promises : ∀ {α : Type u} (s : Computation α) [h : s.Terminates], s.Promises s.get
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkRight_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ η : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.prodMkRight γ (κ + η) =
    ProbabilityTheory.Kernel.prodMkRight γ κ + ProbabilityTheory.Kernel.prodMkRight γ η
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_eq_nnrpow_prod : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {B : Type u_2} [inst_12 : PartialOrder B] [inst_13 : NonUnitalRing B]
  [inst_14 : TopologicalSpace B] [inst_15 : StarRing B] [inst_16 : Module ℝ B] [inst_17 : SMulCommClass ℝ B B]
  [inst_18 : IsScalarTower ℝ B B] [inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint]
  [inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsSemitopologicalRing B] [T2Space B]
  [inst_23 : NonnegSpectrumClass ℝ B] [inst_24 : NonnegSpectrumClass ℝ (A × B)] [inst_25 : StarOrderedRing B] {a : A}
  {b : B} {x : NNReal},
  autoParam (0 ≤ a) CFC.nnrpow_eq_nnrpow_prod._auto_1 →
    autoParam (0 ≤ b) CFC.nnrpow_eq_nnrpow_prod._auto_3 → CFC.nnrpow (a, b) x = (a, b) ^ x
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- `(U'Fη_X, otherMap X)` is a coreflexive pair: in particular if `C` has coreflexive equalizers
then this pair has an equalizer.
 -/
CategoryTheory.LiftRightAdjoint.instIsCoreflexivePairMapAppUnitOtherMap : ∀ {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]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B)
  (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') (X : B),
  CategoryTheory.IsCoreflexivePair (U'.map (F.map (adj₁.unit.app X)))
    (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X)
-- Mathlib.Data.Seq.Computation
Computation.mem_pure_iff : ∀ {α : Type u} (a b : α), a ∈ Computation.pure b ↔ a = b
-- Mathlib.Data.Prod.Lex
Prod.Lex.compare_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β],
  compare = compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.addGrpObj_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] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddGrpObj (F.obj X)], CategoryTheory.AddGrpObj.neg = hF.preimage CategoryTheory.AddGrpObj.neg
-- Mathlib.Topology.Bases
/-- Let `s` be a dense set in a topological space `α` with partial order structure. If `s` is a
separable space (e.g., if `α` has a second countable topology), then there exists a countable
dense subset `t ⊆ s` such that `t` contains bottom/top element of `α` when they exist and belong
to `s`. For a dense subset containing neither bot nor top elements, see
`Dense.exists_countable_dense_subset_no_bot_top`.  -/
Dense.exists_countable_dense_subset_bot_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s],
  Dense s → ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
-- Init.Data.Vector.Lemmas
Vector.foldr_eq_foldl : ∀ {α : Type u_1} {n : ℕ} {init : α} {xs : Vector α n} {f : α → α → α} [Std.Associative f] [Std.LawfulIdentity f init],
  Vector.foldr f init xs = Vector.foldl f init xs
-- Mathlib.Order.WellFoundedSet
Set.isPWO_univ_iff : ∀ {α : Type u_2} [inst : Preorder α], Set.univ.IsPWO ↔ WellQuasiOrderedLE α
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_add_sub_factorThru_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g)) (wf : P.Factors f),
  P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.coeff_cert.eq_1 : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly) (k : ℕ),
  Lean.Grind.Linarith.coeff_cert p₁ p₂ k = (decide (k > 0) && p₁ == p₂.mul ↑k)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The constant map of simplicial sets `X ⟶ Y` induced by a simplex `y : Y _[0]`.  -/
SSet.const : {X Y : SSet} → Y.obj (Opposite.op { len := 0 }) → (X ⟶ Y)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul : ∀ {A : Type u} [inst : CommRing A] [IsNoetherianRing A] {I : Ideal A} [FaithfulSMul A ↥I],
  (↑I ∩ ↑(nonZeroDivisors A)).Nonempty
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
ContDiffOn.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {s : Set E} {n : ℕ∞},
  ContDiffOn ℝ (↑n) c s →
    ContDiffOn ℝ (↑n) R s →
      ContDiffOn ℝ (↑n) x s →
        (∀ a ∈ s, x a ≠ c a) → ContDiffOn ℝ (↑n) (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.isGLB_sInf : ∀ {K : Type u} [inst : DivisionRing K] (S : Set (Subfield K)), IsGLB S (sInf S)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List α} {k : α},
      k ∉ m → l.contains k = false → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey! k = default
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.toPresheaf_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections],
  CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.toPresheaf R)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_le_iff_forall : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {x : ℝ},
  schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < x + ε
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (b : M), ContinuousOn (fun x => b * f x) s
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.antilipschitz : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), AntilipschitzWith 1 ⇑f
-- Mathlib.NumberTheory.NumberField.House
NumberField.norm_norm_le_norm_mul_house_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K) (σ : K →+* ℂ),
  ‖(Algebra.norm ℚ) α‖ ≤ ‖σ α‖ * NumberField.house α ^ (Module.finrank ℚ K - 1)
-- Mathlib.MeasureTheory.Measure.Real
/-- If two sets `s` and `t` are included in a set `u` of finite measure,
and `μ.real s + μ.real t > μ.real u`, then `s` intersects `t`.
Version assuming that `t` is measurable.  -/
MeasureTheory.nonempty_inter_of_measureReal_lt_add : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasurableSet t →
    s ⊆ u →
      t ⊆ u →
        μ.real u < μ.real s + μ.real t →
          autoParam (μ u ≠ ⊤) MeasureTheory.nonempty_inter_of_measureReal_lt_add._auto_1 → (s ∩ t).Nonempty
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A CW complex of a topological space `X` relative to another subspace `D` is the data of its
*`n`-cells* `cell n i` for each `n : ℕ` along with *attaching maps* that satisfy a number of
properties with the most important being closure-finiteness (`mapsTo`) and weak topology
(`closed'`). Note that this definition requires `C` and `D` to be closed subspaces.
If `C` is not closed choose `X` to be `C`.  -/
Topology.RelCWComplex : {X : Type u} → [TopologicalSpace X] → Set X → outParam (Set X) → Type (u + 1)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by
`(Lp.memLp f).restrict s).toLp f`. This map is additive.  -/
MeasureTheory.Lp_toLp_restrict_add : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (f g : ↥(MeasureTheory.Lp E p μ)) (s : Set X),
  MeasureTheory.MemLp.toLp ↑↑(f + g) ⋯ = MeasureTheory.MemLp.toLp ↑↑f ⋯ + MeasureTheory.MemLp.toLp ↑↑g ⋯
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep_of_forall_dist_le : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ},
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) → ENNReal.ofReal d ≤ s.einfsep
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  m.WF → (Std.DHashMap.Raw.filterMap f m).contains k = true → m.contains k = true
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Lsp.RefInfo.findReferenceLocation?.contains : Bool → Lean.Lsp.Range → Lean.Lsp.Position → Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.mk : BigOperators.FinsetResult✝ → Option Lean.Term → BigOperators.FinsetFilterResult✝
-- Mathlib.Topology.Neighborhoods
IsOpen.eventually_mem : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsOpen s → x ∈ s → ∀ᶠ (x : X) in nhds x, x ∈ s
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerived_fac_assoc : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} 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]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F)
  {Z : CategoryTheory.Functor C H} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (LF.leftDerivedLift α W G β))
      (CategoryTheory.CategoryStruct.comp α h) =
    CategoryTheory.CategoryStruct.comp β h
-- Batteries.Tactic.NoMatch
/-- The syntax `fun.` has been deprecated in favor of `nofun`.  -/
Batteries.Tactic.funDot : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Prod
LieHom.prodMap_one : ∀ {R : Type u_1} {L₁ : Type u_2} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L], LieHom.prodMap 1 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) {c c' : C}
  (f : c ⟶ c') {Z : D'} (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)) h)
-- Mathlib.Analysis.Analytic.Constructions
/-- If `A` is a normed algebra over `𝕜` with summable geometric series, then inversion on `A` is
analytic at any unit.  -/
analyticAt_inverse : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_7} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] (z : Aˣ), AnalyticAt 𝕜 Ring.inverse ↑z
-- Mathlib.Order.Filter.Basic
Filter.generate_empty : ∀ {α : Type u}, Filter.generate ∅ = ⊤
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State.mk.inj : ∀ {patternVars patternVars_1 : Array Lean.Expr},
  { patternVars := patternVars } = { patternVars := patternVars_1 } → patternVars = patternVars_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
/-- If `cons (exp, coef) tl` is trimmed, then `coef` is trimmed and is not zero.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.elim_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).Trimmed → coef.Trimmed ∧ ¬coef.IsZero
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instIsPreimmersionAsFiberHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Scheme.Hom.asFiberHom f x)
-- Lean.Meta.Basic
/-- Modify the array of postponed universe level constraints.  -/
Lean.Meta.modifyPostponed : (Lean.PersistentArray Lean.Meta.PostponedEntry → Lean.PersistentArray Lean.Meta.PostponedEntry) → Lean.MetaM Unit
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A block matrix `A.from_blocks B C D` is Hermitian,
if `A` and `D` are Hermitian and `Bᴴ = C`.  -/
Matrix.IsHermitian.fromBlocks : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α}
  {C : Matrix n m α} {D : Matrix n n α},
  A.IsHermitian → B.conjTranspose = C → D.IsHermitian → (Matrix.fromBlocks A B C D).IsHermitian
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.length_eq_one_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → s(u, v) ∈ p.edges → p.length = 1
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddGrpCat)
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.smul_some_eq_ite : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K} {k : K},
  g • ↑k = if ↑g 1 0 * k + ↑g 1 1 = 0 then OnePoint.infty else ↑((↑g 0 0 * k + ↑g 0 1) / (↑g 1 0 * k + ↑g 1 1))
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks] [CategoryTheory.Limits.HasFiniteWidePullbacks C]
  [P.HasOfPostcompProperty P] [P.IsStableUnderBaseChange] [P.ContainsIdentities],
  K ≤ P.precoverage →
    (CategoryTheory.Precoverage.comap
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck =
      (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).inducedTopology (K.toGrothendieck.over S)
-- Mathlib.Algebra.Polynomial.Basic
/-- `C a` is the constant polynomial `a`.
`C` is provided as a ring homomorphism.
 -/
Polynomial.C : {R : Type u} → [inst : Semiring R] → R →+* Polynomial R
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.mem_conjugatesOfSet_iff : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {x : G}, x ∈ Group.conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.goal : Aesop.GoalWithMVars → Lean.MVarId
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`.
Version using `fderiv`.  -/
norm_fderiv_le_of_lipschitzOn : ∀ (𝕜 : 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] {f : E → F}
  {x₀ : E} {s : Set E}, s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖fderiv 𝕜 f x₀‖ ≤ ↑C