mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.coe_zeta_mul_comm : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R},
  ↑ArithmeticFunction.zeta * f = f * ↑ArithmeticFunction.zeta
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_mono_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s.mulEnergy t₁ ≤ s.mulEnergy t₂
-- Init.Meta.Defs
/-- If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
one inferred. The `congr` tactic sets this flag to false.
 -/
Lean.Meta.ApplyConfig.synthAssignedInstances : Lean.Meta.ApplyConfig → Bool
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.id_apply : ∀ {α : Type u_2} [inst : CompleteLattice α] (a : α), (FrameHom.id α) a = a
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion.0.IsCovariantDerivativeOn.torsion.eq_1 : ∀ {𝕜 : 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] [inst_6 : IsManifold I 2 M] [inst_7 : CompleteSpace E]
  {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [inst_8 : CompleteSpace 𝕜]
  [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) (x : M),
  hcov.torsion x = TensorialAt.mkHom₂ (fun x1 x2 => IsCovariantDerivativeOn.torsionAux✝ cov x1 x2 x) x ⋯ ⋯
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- `leadingCoeff p` gives the coefficient of the highest power of `X` in `p`.  -/
Polynomial.leadingCoeff : {R : Type u} → [inst : Semiring R] → Polynomial R → R
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), ↑I.support = ⋂ U, X.zeroLocus ↑(I.ideal U)
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `NNReal`-valued functions.  -/
NNReal.Lp_add_le : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
-- Mathlib.RingTheory.Finiteness.Finsupp
/-- The kernel of the composition of two linear maps is finitely generated if both kernels are and
the first morphism is surjective.  -/
Submodule.fg_ker_comp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  (f : M →ₗ[R] N) (g : N →ₗ[R] P), f.ker.FG → g.ker.FG → Function.Surjective ⇑f → (g ∘ₗ f).ker.FG
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map sending `∑ aᵢ·(gᵢ₁, gᵢ₂, gᵢ₃) : G × G × G →₀ A` to
`∑ φ(aᵢ)·(f(gᵢ₁), f(gᵢ₂), f(gᵢ₃)) : H × H × H →₀ B`.  -/
groupHomology.chainsMap₃ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k G} →
          {B : Rep.{u_1, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (ModuleCat.of k (G × G × G →₀ ↑A) ⟶ ModuleCat.of k (H × H × H →₀ ↑B))
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Integrate `f(x₁,…,xₙ)` over all variables `xᵢ` where `i ∈ s`. Return a function in the
remaining variables (it will be constant in the `xᵢ` for `i ∈ s`).
This is the marginal distribution of all variables not in `s` when the considered measure
is the product measure.  -/
MeasureTheory.«term∫⋯∫⁻__,_» : Lean.ParserDescr
-- Mathlib.Order.Birkhoff
OrderEmbedding.supIrredLowerSet_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), OrderEmbedding.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.norm_apply_le_self_mul_norm_one : ∀ {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [CompleteSpace A] [inst_4 : FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A),
  ‖f a‖ ≤ ‖a‖ * ‖1‖
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_iff_right : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {r : M₀}, r ∈ nonZeroDivisors M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapM.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List (List β) → Sort u_3) →
      (x : List α) →
        (x_1 : List (List β)) →
          ((bs : List (List β)) → motive [] bs) →
            ((a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs) → motive x x_1
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.mk.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [inst_5 : SizeOf ι]
  [inst_6 : SizeOf R] [inst_7 : SizeOf M] [inst_8 : SizeOf N] (form : LinearMap.BilinForm R M)
  (symm : LinearMap.IsSymm form) (ne_zero : ∀ (i : ι), (form (P.root i)) (P.root i) ≠ 0)
  (isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)),
  sizeOf { form := form, symm := symm, ne_zero := ne_zero, isOrthogonal_reflection := isOrthogonal_reflection } =
    1 + sizeOf form + sizeOf symm
-- Std.Data.TreeMap.Raw.Lemmas
_private.Std.Data.TreeMap.Raw.Lemmas.0.Std.TreeMap.Raw.ext : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t t' : Std.TreeMap.Raw α β cmp}, t.inner = t'.inner → t = t'
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.congr_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') {z : B} {g g' : y ⟶ z}
  (η : g ⟶ g'),
  CategoryTheory.Bicategory.whiskerLeft f η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f' η) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The forgetful functor from `SheafedSpace` to `Top`.  -/
AlgebraicGeometry.SheafedSpace.forget : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (AlgebraicGeometry.SheafedSpace C) TopCat
-- Mathlib.Topology.NhdsKer
nhdsKer_prod : ∀ {X : Type u_2} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
  nhdsKer (s ×ˢ t) = nhdsKer s ×ˢ nhdsKer t
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical_isUnit : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {u : E}, IsUnit u → IsUnit (EuclideanDomain.divRadical u)
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.mk : Lean.InductiveVal →
  Array Lean.Name →
    Lean.Name → Array Lean.Expr → Array Lean.Expr → Lean.NameMap Lean.Name → Lean.Meta.SizeOfSpecNested.Context
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instInhabitedMsgEmbed : Inhabited Lean.Widget.MsgEmbed
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.instMkAndCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkAndCached
-- Mathlib.Analysis.Calculus.Deriv.Abs
deriv_abs : ∀ (x : ℝ), deriv (fun x => |x|) x = ↑(SignType.sign x)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.checkNextPatternTypes : Lean.Meta.Match.Problem → Lean.MetaM Unit
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_div : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  Metric.ball x δ / s = x • Metric.thickening δ s⁻¹
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).iso.hom =
    CategoryTheory.CategoryStruct.id (X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.kernelBiprodFstIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.kernelBiprodFstIso.inv =
    CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0)
      (CategoryTheory.Limits.biprod.fstKernelFork X Y)
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.isProbabilityMeasure_gammaMeasure : ∀ {a r : ℝ}, 0 < a → 0 < r → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gammaMeasure a r)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.range_map_le : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d),
  SSet.Subcomplex.range c.map ≤ (SSet.skeletonOfMono i) (d + 1)
-- Aesop.ElabM
Aesop.ElabM.Context.mk.sizeOf_spec : ∀ (parsePriorities : Bool) (goal : Lean.MVarId),
  sizeOf { parsePriorities := parsePriorities, goal := goal } = 1 + sizeOf parsePriorities + sizeOf goal
-- Mathlib.Algebra.DirectSum.Module
DirectSum.ext_component_iff : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {f g : DirectSum ι fun i => M i},
  f = g ↔ ∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g
-- Init.Notation
/-- `a ∉ b` is negated elementhood. It is notation for `¬ (a ∈ b)`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∉` in identifiers is `notMem`. -/
«term_∉_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.OfSurjective.dividedPowers_unique : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {f : A →+* B} {J : Ideal B} (hf : Function.Surjective ⇑f) (hIJ : J = Ideal.map f I)
  (hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)) (hquot : DividedPowers J),
  hI.IsDPMorphism hquot f → hquot = DividedPowers.Quotient.OfSurjective.dividedPowers hI hf hIJ hIf
-- Aesop.Tree.Data
Aesop.GoalData.normalizationState : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.NormalizationState
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ihom_adjunction_counit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A], (CategoryTheory.ihom.adjunction A).counit = CategoryTheory.ihom.ev A
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [inst_2 : CategoryTheory.Limits.HasEnd F] {i j : J}
  (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F i)
      (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j)
      (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
-- Std.Internal.Do.Triple.Basic
/-- Ascribe the program so its monad can be recovered during elaboration. An explicit `(m := …)`
ascribes the program to `… _`, supplying the monad head directly. Otherwise a `match`/`if`/`do`
program gets the monadic-application hint `(_ : _ → _) _`, recovering its monad by first-order
unification. Other programs are untouched.  -/
_private.Std.Internal.Do.Triple.Basic.0.Std.Internal.Do.hintProgram : Lean.Term → Option Lean.Term → Lean.MacroM Lean.Term
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  compare ((Std.ExtDTreeMap.Const.modify t k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (π π' : Y ⟶ P)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
  (w' : CategoryTheory.CategoryStruct.comp π'.unop f.unop = CategoryTheory.CategoryStruct.comp π'.unop g.unop)
  (h : π = π'),
  CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop π π' w w' h =
    CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop π π' w w' h
-- Mathlib.Topology.Constructions.SumProd
isQuotientMap_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty X],
  Topology.IsQuotientMap Prod.snd
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_lt_add_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ↑⌈a⌉₊ < a + 1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_not_isDiag : ∀ {V : Type u}, SimpleGraph.fromEdgeSet Sym2.diagSetᶜ = ⊤
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_compLinearMap_lsingle : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] [inst_5 : Fintype ι] [inst_6 : (i : ι) → DecidableEq (κ i)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (p : (i : ι) → κ i),
  ((MultilinearMap.piFamily f).compLinearMap fun i => LinearMap.single R (M i) (p i)) =
    (LinearMap.single R N p).compMultilinearMap (f p)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.params : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Expr
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that `grind? +suggestions` suggestions actually work.  -/
linter.tacticAnalysis.verifyGrindSuggestions : Lean.Option Bool
-- Mathlib.Analysis.Convex.EGauge
/-- The Minkowski functional for vector spaces over normed fields.
Given a set `s` in a vector space over a normed field `𝕜`,
`egauge s` is the functional which sends `x : E`
to the infimum of `‖c‖ₑ` over `c` such that `x` belongs to `s` scaled by `c`.

The definition only requires `𝕜` to have a `ENorm` instance
and `(· • ·) : 𝕜 → E → E` to be defined.
This way the definition applies, e.g., to `𝕜 = ℝ≥0`.
For `𝕜 = ℝ≥0`, the function is equal (up to conversion to `ℝ`)
to the usual Minkowski functional defined in `gauge`.  -/
egauge : (𝕜 : Type u_1) → [ENorm 𝕜] → {E : Type u_2} → [SMul 𝕜 E] → Set E → E → ENNReal
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.isLeftDerivedFunctor_iff_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  {F : CategoryTheory.Functor C H} (LF : CategoryTheory.Functor D H) (α : L.comp LF ⟶ F),
  W.IsInvertedBy F → (LF.IsLeftDerivedFunctor α W ↔ CategoryTheory.IsIso α)
-- Init.Data.Sum.Basic
/-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`.  -/
Sum.LiftRel.inr : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {d : δ},
  s b d → Sum.LiftRel r s (Sum.inr b) (Sum.inr d)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.toFreeAddMonoid_injective : ∀ {α : Type u_1}, Function.Injective ⇑FreeAddSemigroup.toFreeAddMonoid
-- Mathlib.Data.Nat.Factorization.Root
/-- Galois connection between `ceilRoot n : ℕ → ℕ` and `a ↦ a ^ n : ℕ → ℕ` where `ℕ` is ordered
by divisibility.

Note that this cannot possibly hold for `n = 0`, regardless of the value of `ceilRoot 0 a`, because
the statement reduces to `a = 1 ↔ ceilRoot 0 a ∣ b`, which is false for e.g. `a = 0`,
`b = ceilRoot 0 a`.  -/
Nat.dvd_pow_iff_ceilRoot_dvd : ∀ {a b n : ℕ}, n ≠ 0 → (a ∣ b ^ n ↔ n.ceilRoot a ∣ b)
-- Mathlib.RingTheory.LocalRing.ResidueField.Defs
IsLocalRing.instCommRingResidueField : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsLocalRing R] → CommRing (IsLocalRing.ResidueField R)
-- Lean.Meta.Sym.Simp.SimpM
/-- Size of the local context when simplification started.
Used to determine which free variables were introduced during simplification.  -/
Lean.Meta.Sym.Simp.Context.initialLCtxSize : Lean.Meta.Sym.Simp.Context → ℕ
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.add_one_eq_succ : ∀ (o : Ordinal.{u_1}), o + 1 = Order.succ o
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  s.addEnergy t = {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 + x.2.1 = x.1.2 + x.2.2}.card
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Lp space  -/
MeasureTheory.Lp : {α : Type u_7} →
  (E : Type u_6) →
    {m : MeasurableSpace α} →
      [inst : NormedAddCommGroup E] →
        ENNReal → (μ : autoParam (MeasureTheory.Measure α) MeasureTheory.Lp._auto_1) → AddSubgroup (α →ₘ[μ] E)
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_eq_top : ∀ {a b : ENNReal}, a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddOpposite.opUniformEquivLeft.eq_1 : ∀ (G : Type u_2) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  AddOpposite.opUniformEquivLeft G =
    { toEquiv := AddOpposite.opEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Mathlib.Analysis.Normed.Affine.AddTorsor
DilationEquiv.smulTorsor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] {P : Type u_3} [inst_4 : PseudoMetricSpace P] [inst_5 : NormedAddTorsor E P] (c : P)
  {k : 𝕜} (hk : k ≠ 0) (x : E), (DilationEquiv.smulTorsor c hk) x = k • x +ᵥ c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' fallback : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKeyD k' fallback = k
-- Mathlib.Analysis.Real.Spectrum
QuasispectrumRestricts.nnreal_of_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A]
  [inst_4 : PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A},
  0 ≤ a → QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
-- Init.Meta.Defs
Lean.version.minor : ℕ
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.const : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {y : Y},
  HolderWith C r (Function.const X y)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.ofList l cmp).getKey? k' = some k
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}, CongruenceSubgroup.IsCongruenceSubgroup Γ → Γ.FiniteIndex
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE!_eq_get!_getEntryGE? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α}
  [inst_1 : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.getEntryGE! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t).get!
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.funLike : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.insert k).get? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.get? a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_singleton_iff : ∀ {k m n : ℕ}, (m<...=n).toList = [k] ↔ n = m + 1 ∧ m + 1 = k
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf K A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).inv.app X).hom.app X_1 =
    X.obj.map (e.counitIso.hom.app (Opposite.unop X_1)).op
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0.inj : ∀ {p : Lean.Grind.CommRing.Poly} {d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation}
  {c : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {p_1 : Lean.Grind.CommRing.Poly}
  {d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation} {c_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p d c =
      Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p_1 d_1 c_1 →
    p = p_1 ∧ d = d_1 ∧ c = c_1
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.comp_rightInv_aux1 : ∀ {𝕜 : 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] {n : ℕ},
  0 < n →
    ∀ (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 F E) (v : Fin n → F),
      (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v