mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Basic
AddLeftCancelMonoid.add_ne_zero : ∀ {α : Type u} [inst : AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear : ∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W] (p : W × (V →L[𝕜] W)),
  ((ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W).symm p).contLinear = p.2
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isRightRegular_op`. -/
IsRightRegular.op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsLeftRegular a → IsRightRegular (MulOpposite.op a)
-- Lean.Meta.Sym.Arith.Types
/-- Classification state for a type with a `Ring` instance.  -/
Lean.Meta.Sym.Arith.Ring : Type
-- Std.Http.Protocol.H1
/-- Advances writer-side state machine by one logical transition.

Depending on writer state, this may:
- request an application answer,
- serialize headers,
- flush fixed/chunked body bytes,
- finalize/close after completion.
 -/
Std.Http.Protocol.H1.Machine.processWrite : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Algebra.Group.Action.Defs
/-- Pushforward a multiplicative action along a surjective map respecting `•`.
See note [reducible non-instances].  -/
Function.Surjective.mulAction : {M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : Monoid M] →
        [inst_1 : MulAction M α] →
          [inst_2 : SMul M β] →
            (f : α → β) → Function.Surjective f → (∀ (c : M) (x : α), f (c • x) = c • f x) → MulAction M β
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.le_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : NonUnitalSubsemiring R), s ≤ s.topologicalClosure
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).minKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.ssubset_of_not_superset`.

---

Set notation form of `LE.le.lt_of_not_ge` -/
LE.le.ssubset_of_not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊆ a → a ⊂ b
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (N' : Submonoid N),
  f.submonoidComap N' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Level
Lean.Level.isMaxIMax : Lean.Level → Bool
-- Init.Data.Char.Ordinal
Char.ordinal_ofOrdinal : ∀ {f : Fin Char.numCodePoints}, (Char.ofOrdinal f).ordinal = f
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D) (c c' : C),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv =
    (CategoryTheory.Functor.LaxMonoidal.μ F c c').app d
-- Mathlib.Topology.Closure
IsOpen.subset_interior_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → s ⊆ interior (closure s)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The underlying set of a term of a `ZeroMemClass` is nonempty.  -/
ZeroMemClass.coe_nonempty : ∀ {S : Type u_3} {M : Type u_4} [inst : Zero M] [inst_1 : SetLike S M] [ZeroMemClass S M] (s : S), (↑s).Nonempty
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_of : ∀ {α : Type u} {p : α} {s : Set α}, (FreeCommRing.of p).IsSupported s ↔ p ∈ s
-- Init.Data.List.Lemmas
List.exists_of_mem_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {b : α_1}, b ∈ List.map f l → ∃ a ∈ l, f a = b
-- Mathlib.Analysis.CStarAlgebra.Classes
/-- The class of unital (complex) C⋆-algebras.  -/
CStarAlgebra : Type u_1 → Type u_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX
-- Mathlib.Algebra.Order.Module.Defs
PosSMulMono.toSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β], SMulPosMono α β
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.denseRange : ∀ (G : AddGrpCat), DenseRange (ProfiniteAddGrp.ProfiniteCompletion.etaFn G)
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.of_unique_nonzero_prime : ∀ {R : Type u_1} [inst : CommSemiring R], (∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsLocalRing R
-- Mathlib.Topology.Path
Path.extend_cast : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y x' y' : X} (γ : Path x y) (hx : x' = x) (hy : y' = y),
  (γ.cast hx hy).extend = γ.extend
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofList_equiv_foldl : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)},
  (Std.DHashMap.Raw.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.continuousOn_toFun : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (e e' : PartialEquiv M H),
  e ∈ self.atlas → e' ∈ self.atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedMutVar.default : Lean.Elab.Do.MutVar
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.extendRCLikeL.congr_simp : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F],
  WeakDual.extendRCLikeL = WeakDual.extendRCLikeL
-- Init.Data.List.Lex
_private.Init.Data.List.Lex.0.List.lex.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α)
  (h_1 : (head : α) → (tail : List α) → motive [] (head :: tail)) (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match x, [] with
    | [], head :: tail => h_1 head tail
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_2 x
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- Auxiliary `OrderIso` with a product type used to lift a `BoundedOrder` structure.  -/
BoxIntegral.IntegrationParams.isoProd : BoxIntegral.IntegrationParams ≃o Bool × Boolᵒᵈ × Boolᵒᵈ
-- Lean.Server.Requests
/-- Finds the info tree of the first snapshot task containing `pos`, asynchronously.
The info tree may be from a nested snapshot, such as a single tactic.

See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done.
 -/
Lean.Server.RequestM.findInfoTreeAtPos : Lean.Server.FileWorker.EditableDocument → String.Pos.Raw → Bool → Lean.Server.ServerTask (Option Lean.Elab.InfoTree)
-- Init.Data.UInt.Lemmas
USize.toNat_lt_two_pow_numBits : ∀ (n : USize), n.toNat < 2 ^ System.Platform.numBits
-- Batteries.Data.MLList.Basic
/-- Lift a monadic lazy list inside the monad to a monadic lazy list.  -/
MLList.squash : {m : Type u_1 → Type u_1} → {α : Type u_1} → (Unit → m (MLList m α)) → MLList m α
-- Mathlib.Data.Sum.Order
/-- Lexicographical `Sum.inl`. Only used for pattern matching.  -/
Sum.inlₗ : {α : Type u_1} → {β : Type u_2} → α → α ⊕ₗ β
-- Mathlib.LinearAlgebra.Basis.Defs
/-- A module over a finite ring that admits a finite basis is finite.  -/
Module.fintypeOfFintype : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Fintype ι] → Module.Basis ι R M → [Fintype R] → Fintype M
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.continuous_setToFun : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  Continuous fun f => MeasureTheory.setToFun μ T hT ↑↑f
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.instIsEquivalenceRev : SimplexCategory.rev.IsEquivalence
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeMinOrder.liftRight : {𝕆 : Type u_1} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [GradeMinOrder 𝕆 β] →
              (f : α → β) →
                StrictMono f → (∀ (a b : α), a ⋖ b → f a ⋖ f b) → (∀ (a : α), IsMin a → IsMin (f a)) → GradeMinOrder 𝕆 α
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrict_eqOn_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {V : Set X}
  (D : Function.locallyFinsuppWithin U Y) (h : V ⊆ U), Set.EqOn (⇑(D.restrict h)) 0 Vᶜ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_even : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  normEDS b c d (2 * m) * b =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_star : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K},
  (CategoryTheory.WithTerminal.coneEquiv.functor.obj t).π.app CategoryTheory.WithTerminal.star = t.pt.hom
-- Mathlib.Order.Filter.Basic
Filter.mkOfClosure_sets : ∀ {α : Type u} {s : Set (Set α)} {hs : (Filter.generate s).sets = s}, Filter.mkOfClosure s hs = Filter.generate s
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {Φ₁ Φ₂ : S₁.Hom S₂}, Φ₁ = Φ₂ ↔ ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
-- Lean.Meta.Tactic.Grind.Types
/-- If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
Otherwise, it pushes `lhs ≍ rhs`.
 -/
Lean.Meta.Grind.pushEqCore : Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Unit
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.below : {motive : (a : Lean.Grind.Linarith.Poly) → a.NonnegCoeffs → Prop} →
  {a : Lean.Grind.Linarith.Poly} → a.NonnegCoeffs → Prop
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.one : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃Functor_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {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_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X Y : C₃} (h : X ⟶ Y)
  (X_1 : C₂) (Y_1 : C₁),
  (((CategoryTheory.Functor.flip₁₃Functor.obj F).map h).app X_1).app Y_1 = ((F.obj Y_1).obj X_1).map h
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- Presentation of the proximity function as iterated circle averages.
 -/
ValueDistribution.circleAverage_circleAverage_eq_proximity_top : ∀ {f : ℂ → ℂ},
  Meromorphic f →
    (fun R => Real.circleAverage (fun a => Real.circleAverage (fun x => Real.log ‖f x - a‖) 0 R) 0 1) =
      ValueDistribution.proximity f ⊤
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Coefficients of a product of power series  -/
MvPowerSeries.coeff_prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : DecidableEq σ]
  (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι),
  (MvPowerSeries.coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff (l i)) (f i)
-- Mathlib.Condensed.Light.Explicit
LightCondensed.ofSheafLightProfinite_obj : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (F : CategoryTheory.Functor LightProfiniteᵒᵖ A)
  [inst_1 : CategoryTheory.Limits.PreservesFiniteProducts F] (hF : CategoryTheory.regularTopology.EqualizerCondition F),
  (LightCondensed.ofSheafLightProfinite F hF).obj = F
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_comp_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (-f) (CategoryTheory.CategoryStruct.comp (-g) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {f : β → n (Option β')} [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n] [inst_4 : MonadLiftT m n],
  (Std.IterM.filterMapM f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← MonadAttach.attach (f out)
        match __do_lift with
          | ⟨none, hf⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMapM f it') ⋯))
          | ⟨some out', hf⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filterMapM f it') out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMapM f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.LinearAlgebra.Countable
Finsupp.Countable.of_moduleFinite : ∀ {M : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Countable R]
  [Module.Finite R M], Countable M
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.mem_supp_congr_adj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (c : G.ConnectedComponent), G.Adj v w → (v ∈ c.supp ↔ w ∈ c.supp)
-- Plausible.Functions
Plausible.TotalFunction.withDefault.inj : ∀ {α : Type u} {β : Type v} {a : List ((_ : α) × β)} {a_1 : β} {a_2 : List ((_ : α) × β)} {a_3 : β},
  Plausible.TotalFunction.withDefault a a_1 = Plausible.TotalFunction.withDefault a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M}
  (g : CategoryTheory.ShiftedHom Y Z a),
  (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f).comp g ⋯ = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.cardinalMk_le_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {ι : Type w} {b : ι → M}, LinearIndependent R b → Cardinal.mk ι ≤ ↑(Module.finrank R M)
-- Mathlib.Algebra.Algebra.ZMod
ZMod.instSubsingletonAlgebra : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ), Subsingleton (Algebra (ZMod p) R)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
/-- `ExteriorAlgebra.GradedAlgebra.ι` lifted to exterior algebra. This is
primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`.  -/
ExteriorAlgebra.GradedAlgebra.liftι : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ExteriorAlgebra R M →ₐ[R] DirectSum ℕ fun i => ↥(⋀[R]^i M)
-- Mathlib.LinearAlgebra.Projection
LinearMap.surjective_comp_projectionOnto : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  {M : Type u_6} [inst_3 : AddCommMonoid M] (h : IsCompl p q) [inst_4 : Module R M],
  Function.Surjective (p.projectionOnto q h).comp
-- Mathlib.Algebra.Order.GroupWithZero.Defs
le_mul_of_le_mul_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [MulPosMono α],
  a ≤ b * c → b ≤ d → 0 ≤ c → a ≤ d * c
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.output.sizeOf_spec : ∀ (indent ticks : ℕ),
  sizeOf (Lean.Server.FileWorker.Hover.RWState.output✝ indent ticks) = 1 + sizeOf indent + sizeOf ticks
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_eq_fmod : ∀ {a b : ℤ},
  a.tmod b =
    a.fmod b - if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else b else if 0 ≤ b then ↑b.natAbs else 2 * ↑b.toNat
-- Std.Time.Time.PlainTime
/-- `Millisecond` component of the `PlainTime`
 -/
Std.Time.PlainTime.millisecond : Std.Time.PlainTime → Std.Time.Millisecond.Ordinal
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.num_X : ∀ {K : Type u} [inst : Field K], RatFunc.X.num = Polynomial.X
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedLetRecToLift : Inhabited Lean.Elab.Term.LetRecToLift
-- Batteries.Data.Array.Basic
/-- Find the first minimal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.minI : {α : Type u_1} → [ord : Ord α] → [Inhabited α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableAt_neg_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x}
  {x₀ : B}, MDiffAt (T% s) x₀ → (MDiffAt fun x => ⟨x, (-s) x⟩) x₀
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.normalizer_singleton : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), AddSubgroup.normalizer {g} = AddSubgroup.centralizer {g}
-- Lean.Data.Json.Basic
Lean.Json.Structured.obj : Std.TreeMap.Raw String Lean.Json compare → Lean.Json.Structured
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradientWithin_univ : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜}, gradientWithin f Set.univ = gradient f
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular] (X : C),
  CategoryTheory.isCardinalPresentable C κ X ↔ CategoryTheory.IsCardinalPresentable X κ
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.val_one : ∀ {R : Type u_1} [inst : NonUnitalSemiring R], PreQuasiregular.val 1 = 0
-- Batteries.CodeAction.Attr
/-- An extension which collects all the tactic code actions.  -/
Batteries.CodeAction.tacticCodeActionExt : Lean.PersistentEnvExtension Batteries.CodeAction.TacticCodeActionEntry
  (Batteries.CodeAction.TacticCodeActionEntry × Batteries.CodeAction.TacticCodeAction)
  (Array Batteries.CodeAction.TacticCodeActionEntry × Batteries.CodeAction.TacticCodeActions)
-- Batteries.Tactic.Lint.Simp
/-- This note gives you some tips to debug any errors that the simp-normal form linter raises.

The reason that a lemma was considered faulty is because its left-hand side is not in simp-normal
form.
These lemmas are hence never used by the simplifier.

This linter gives you a list of other simp lemmas: look at them!

Here are some tips depending on the error raised by the linter:

  1. 'the left-hand side reduces to XYZ':
     you should probably use XYZ as the left-hand side.

  2. 'simp can prove this':
     This typically means that lemma is a duplicate, or is shadowed by another lemma:

     2a. Always put more general lemmas after specific ones:
      ```
      @[simp] lemma zero_add_zero : 0 + 0 = 0 := rfl
      @[simp] lemma add_zero : x + 0 = x := rfl
      ```

      And not the other way around!  The simplifier always picks the last matching lemma.

     2b. You can also use `@[priority]` instead of moving simp-lemmas around in the file.

      Tip: the default priority is 1000.
      Use `@[priority 1100]` instead of moving a lemma down,
      and `@[priority 900]` instead of moving a lemma up.

     2c. Conditional simp lemmas are tried last. If they are shadowed
         just remove the `simp` attribute.

     2d. If two lemmas are duplicates, the linter will complain about the first one.
         Try to fix the second one instead!
         (You can find it among the other simp lemmas the linter prints out!)

  3. 'try_for tactic failed, timeout':
     This typically means that there is a loop of simp lemmas.
     Try to apply squeeze_simp to the right-hand side (removing this lemma from the simp set) to see
     what lemmas might be causing the loop.

     Another trick is to `set_option trace.simplify.rewrite true` and
     then apply `try_for 10000 { simp }` to the right-hand side.  You will
     see a periodic sequence of lemma applications in the trace message.
 -/
LibraryNote.«simp-normal_form» : Batteries.Util.LibraryNote
-- Std.Http.Data.Method
/-- Describe communication options for a resource.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.7
 -/
Std.Http.Method.options : Std.Http.Method
-- Std.Data.TreeSet.Basic
/-- Returns the `n`-th smallest element.  -/
Std.TreeSet.atIdx : {α : Type u} → {cmp : α → α → Ordering} → (t : Std.TreeSet α cmp) → (n : ℕ) → n < t.size → α
-- Mathlib.Data.Sigma.Order
Sigma.lt_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LT (α i)] {a b : (i : ι) × α i},
  a < b ↔ ∃ (h : a.fst = b.fst), h ▸ a.snd < b.snd
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getD.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (fallback : β) (x : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.getD a fallback x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => fallback
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      bif k == a then v else Std.DHashMap.Internal.AssocList.getD a fallback es
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `map` function for `Chain`  -/
OmegaCompletePartialOrder.Chain.map : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → OmegaCompletePartialOrder.Chain α → (α →o β) → OmegaCompletePartialOrder.Chain β
-- Init.Data.Int.Order
Int.lt_add_of_neg_lt_sub_left : ∀ {a b c : ℤ}, -a < b - c → c < a + b