mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.LeftHomotopyClass.whitehead : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsFibrant X]
  [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) [HomotopicalAlgebra.WeakEquivalence f],
  ∃ g,
    HomotopicalAlgebra.LeftHomotopyRel (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) ∧
      HomotopicalAlgebra.LeftHomotopyRel (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Logic.Nontrivial.Defs
nontrivial_iff : ∀ {α : Type u_1}, Nontrivial α ↔ ∃ x y, x ≠ y
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.Functor.FullyFaithful.homEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C},
  hF.homEquiv = { toFun := F.map, invFun := hF.preimage, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Order.Basic
IsLowerSet.isOpen : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α},
  IsLowerSet s → IsOpen s
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
/-- If `C` has strict initial objects and `X` is an initial object, the category
`Over X` is equivalent to a point.  -/
CategoryTheory.overEquivOfIsInitial : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      (X : C) → CategoryTheory.Limits.IsInitial X → (CategoryTheory.Over X ≌ CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.ae_comp_of_ae_ae : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {a : α} {p : γ → Prop},
  MeasurableSet {z | p z} → (∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z) → ∀ᵐ (z : γ) ∂(η.comp κ) a, p z
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSingletonClass α] {f : α → ENNReal} (a : α),
  ∫⁻ (a : α), f a ∂ProbabilityTheory.Kernel.id a = f a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X X_1 : C) (X_2 : D),
  (((CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso C D).hom.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso X X_1 X_2).hom
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.isoClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms], P.isoClosure = P
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a : Lean.Grind.CommRing.Expr),
  x = a.neg →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_7 a
-- Lean.Data.Lsp.Basic
Lean.Lsp.ApplyWorkspaceEditParams.mk.sizeOf_spec : ∀ (label? : Option String) (edit : Lean.Lsp.WorkspaceEdit),
  sizeOf { label? := label?, edit := edit } = 1 + sizeOf label? + sizeOf edit
-- Mathlib.Order.CompleteLattice.Defs
sInf_mem_lowerBounds : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α}, sInf s ∈ lowerBounds s
-- Mathlib.CategoryTheory.Category.PartialFun
PartialFun.instCoeSortType : CoeSort PartialFun (Type u_1)
-- Mathlib.Order.Filter.Pointwise
Filter.mem_zero : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, s ∈ 0 ↔ 0 ∈ s
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_comp_left : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {S₂ : Type u_2}
  [inst_2 : CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R),
  k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (k.comp f) (⇑k ∘ g) p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false →
    Std.DTreeMap.Internal.Impl.Const.get? (m₁.union m₂ ⋯ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get? m₂ k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.AddMon C} → (hom : M.X ⟶ N.X) → [isAddMonHom_hom : CategoryTheory.IsAddMonHom hom] → M.Hom N
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.finitenessRelation : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      [inst : String.Slice.Pattern.ForwardPattern pat] →
        [String.Slice.Pattern.StrictForwardPattern pat] →
          Std.Iterators.FinitenessRelation (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s) Id
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.EMatchTheoremIds : Type
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafify.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  J.sheafify P = J.plusObj (J.plusObj P)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKey_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} (hk : k ∈ t₁), t₁.getKey k hk = t₂.getKey k ⋯
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toWithBotNat_eq_bot_iff : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x : R),
  IsDiscreteValuationRing.toWithBotNat x = ⊥ ↔ x = 0
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_inj_iff : ∀ {R : Type u} (x y : R), Tropical.trop x = Tropical.trop y ↔ x = y
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_of_exists_eq_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β}, (∃ b, f b = 0) → ∀ [L.LeAtTop], Multipliable f L
-- Mathlib.Algebra.CharP.Two
CharTwo.add_cancel_right : ∀ {R : Type u_1} [inst : Semiring R] [CharP R 2] (a b : R), a + b + b = a
-- Mathlib.Tactic.Contrapose
/-- An option to turn off the feature that `contrapose` negates both sides of `↔` goals.
This may be useful for teaching.  -/
Mathlib.Tactic.Contrapose.contrapose.negate_iff : Lean.Option Bool
-- Init.Data.Order.PackageFactories
Std.OrientedCmp.of_gt_iff_lt : ∀ {α : Type u} {cmp : α → α → Ordering},
  (∀ (a b : α), cmp a b = Ordering.gt ↔ cmp b a = Ordering.lt) → Std.OrientedCmp cmp
-- Mathlib.Analysis.Convex.Basic
convex_halfSpace_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w | f w ≤ r}
-- Mathlib.Data.Sym.Sym2.Order
Sym2.sortEquiv_apply_coe : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Sym2 α), ↑(Sym2.sortEquiv s) = (s.inf, s.sup)
-- Lean.Meta.Tactic.Grind.CheckResult
/-- No progress  -/
Lean.Meta.Grind.CheckResult.none : Lean.Meta.Grind.CheckResult
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.map_zero_on_compl : ∀ {B : Type u_5} {E : outParam (Type u_6)} {F : outParam (Type u_7)} {inst : NormedAddCommGroup E}
  {inst_1 : NormedAddCommGroup F} {inst_2 : NormedSpace ℝ E} {inst_3 : NormedSpace ℝ F} {n : outParam ℕ∞}
  {K : outParam (TopologicalSpace.Compacts E)} [self : ContDiffMapSupportedInClass B E F n K] (f : B),
  Set.EqOn (⇑f) 0 (↑K)ᶜ
-- Mathlib.Order.Antisymmetrization
Antisymmetrization.induction_on : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] {p : Antisymmetrization α r → Prop}
  (a : Antisymmetrization α r), (∀ (a : α), p (toAntisymmetrization r a)) → p a
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The isomorphism `(K.truncLE' e).X i ≅ K.X i'` when `e.f i = i'`
and `e.BoundaryLE i` does not hold.  -/
HomologicalComplex.truncLE'XIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      {i : ι} → {i' : ι'} → e.f i = i' → ¬e.BoundaryLE i → ((K.truncLE' e).X i ≅ K.X i')
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.trans : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SSameSide x y → s.SSameSide y z → s.SSameSide x z
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α),
  Inv.inv '' Set.Iio a = Set.Ioi a⁻¹
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- `sin π z` is non vanishing on the complement of the integers in `ℂ`.  -/
sin_pi_mul_ne_zero : ∀ {x : ℂ}, x ∈ Complex.integerComplement → Complex.sin (↑Real.pi * x) ≠ 0
-- Mathlib.Testing.Plausible.Functions
_private.Mathlib.Testing.Plausible.Functions.0.Plausible.TotalFunction.zeroDefault.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Plausible.TotalFunction α β → Sort u_3) →
      (x : Plausible.TotalFunction α β) →
        ((A : List ((_ : α) × β)) → (a : β) → motive (Plausible.TotalFunction.withDefault A a)) → motive x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_op : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸),
  NormedSpace.exp (MulOpposite.op x) = MulOpposite.op (NormedSpace.exp x)
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- The standard basis of the space linear maps between two modules
induced by a basis of the domain and codomain.

If `M₁` and `M₂` are modules with basis `b₁` and `b₂` respectively indexed
by finite types `ι₁` and `ι₂`,
then `Basis.linearMap b₁ b₂` is the basis of `M₁ →ₗ[R] M₂` indexed by `ι₂ × ι₁`
where `(i, j)` indexes the linear map that sends `b j` to `b i`
and sends all other basis vectors to `0`.  -/
Module.Basis.linearMap : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {ι₁ : Type u_6} →
        {ι₂ : Type u_7} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M₁] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : Module R M₁] →
                  [inst_4 : Module R M₂] →
                    [Fintype ι₁] →
                      [Fintype ι₂] →
                        [DecidableEq ι₁] →
                          Module.Basis ι₁ R M₁ → Module.Basis ι₂ R M₂ → Module.Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Ensure that `forget₂ CommMonCat MonCat` automatically reflects isomorphisms.  -/
CommMonCat.forget₂_full : (CategoryTheory.forget₂ CommMonCat MonCat).Full
-- Mathlib.Order.Category.Preord
Preord.ofHom_hom : ∀ {X Y : Preord} (f : X ⟶ Y), Preord.ofHom (Preord.Hom.hom f) = f
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.tendsto_nhds_iff_not_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {β : Type u_3} {f : β → α}
  {l : Filter β} {x : α}, Filter.Tendsto f l (nhds x) ↔ ∀ (y : α), ¬y ≤ x → ∀ᶠ (z : β) in l, ¬y ≤ f z
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_add : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : ContinuousAdd M] (v w : MeasureTheory.VectorMeasure α M) (i : Set α),
  (v + w).restrict i = v.restrict i + w.restrict i
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Applying a continuous alternating map to a vector is continuous
in the pair (map, vector).

Continuity in the vector holds by definition
and continuity in the map holds if both the domain and the codomain are topological vector spaces.
However, continuity in the pair (map, vector) needs the domain to be a locally bounded TVS.
We have no typeclass for a locally bounded TVS,
so we require it to be a seminormed space instead.  -/
ContinuousAlternatingMap.instContinuousEval : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F]
  [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F], ContinuousEval (E [⋀^ι]→L[𝕜] F) (ι → E) F
-- Mathlib.Data.Finite.Defs
Equiv.finite_iff : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ≃ β), Finite α ↔ Finite β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.setIntegral_abs_condExp_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] {s : Set α},
  MeasurableSet s → ∀ (f : α → E), ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
-- Lean.Elab.Do.Basic
Lean.Elab.Do.map1TermElabM : {β : Sort u_1} →
  ({α : Type} → (β → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α) →
    {α : Type} → (β → Lean.Elab.Do.DoElabM α) → Lean.Elab.Do.DoElabM α
-- Mathlib.Topology.ExtremallyDisconnected
/-- The assertion `CompactT2.Projective` states that given continuous maps
`f : X → Z` and `g : Y → Z` with `g` surjective between `t_2`, compact topological spaces,
there exists a continuous lift `h : X → Y`, such that `f = g ∘ h`.  -/
CompactT2.Projective : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_smul : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a : ℂ) (f : F) [ModularFormClass F Γ k],
        UpperHalfPlane.qExpansion h (a • ⇑f) = a • UpperHalfPlane.qExpansion h ⇑f
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.zero_mono : ∀ {α : Type u_5} {β : Type u_6} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Zero β], Monotone 0
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- For a unary operation (e.g. `x ↦ -x`) defined at each stalk, if a prelocal predicate is closed
under the operation on each open set (possibly by refinement), then the sheafified predicate is
also closed under the operation. See `sheafify_inductionOn'` for the version without refinement.  -/
TopCat.PrelocalPredicate.sheafify_inductionOn : ∀ {X : TopCat} {T : ↑X → Type u_2} (P : TopCat.PrelocalPredicate T) (op : {x : ↑X} → T x → T x),
  (∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T ↑x},
      P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x => op (a (i x))) →
    ∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T ↑x}, P.sheafify.pred a → P.sheafify.pred fun x => op (a x)
-- Init.Data.SInt.Lemmas
instLawfulIdentityInt32HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorEqLocus_coe : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) (x : TensorProduct R M ↥(f.eqLocus g)),
  ↑((LinearMap.tensorEqLocus S M f g) x) = (LinearMap.lTensor M (f.eqLocus g).subtype) x
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup is closed under inverse.  -/
Subgroup.inv_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G}, x ∈ H → x⁻¹ ∈ H
-- Mathlib.Algebra.RingQuot
RingQuot.mkRingHom_def : ∀ {R : Type u_1} [inst : Semiring R] (r : R → R → Prop),
  RingQuot.mkRingHom r =
    { toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ }
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- `S n` is the `n`th rescaled Chebyshev polynomial of the second kind (also known as a
Vieta–Fibonacci polynomial), given by $S_n(2x) = U_n(x)$. See
`Polynomial.Chebyshev.S_comp_two_mul_X`.  -/
Polynomial.Chebyshev.S : (R : Type u_1) → [inst : CommRing R] → ℤ → Polynomial R
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_roo : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LT α] [inst_3 : DecidableLT α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roo α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiplicative.ofAdd.eq_1 : ∀ {α : Type u}, Multiplicative.ofAdd = { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.mem_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M}, x ∈ Subsemigroup.closure s ↔ ∀ (S : Subsemigroup M), s ⊆ ↑S → x ∈ S
-- Init.Grind.Offset
Lean.Grind.Nat.lo_lo : ∀ (u w v k₁ k₂ : ℕ), u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  (CategoryTheory.Limits.PreservesPullback.iso G f g).hom = CategoryTheory.Limits.pullbackComparison G f g
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_two : ∀ {c : Char} (h : c.utf8Size = 2), (String.utf8EncodeChar c)[0].toBitVec = 6#3 ++ BitVec.extractLsb' 6 5 c.val.toBitVec
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- A version of the **direct comparison test** for conditionally convergent series.
See `cauchySeq_finset_of_norm_bounded` for the same statement about absolutely convergent ones.  -/
cauchySeq_range_of_norm_bounded : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ℕ → E} {g : ℕ → ℝ},
  (CauchySeq fun n => ∑ i ∈ Finset.range n, g i) →
    (∀ (i : ℕ), ‖f i‖ ≤ g i) → CauchySeq fun n => ∑ i ∈ Finset.range n, f i
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_eq_card_dsupport : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E 0)), ‖f‖ = ↑⋯.toFinset.card
-- Mathlib.Data.List.Shortlex
/-- If a list `s` is shorter than a list `t`, then `s` is smaller than `t` under any shortlex
order.  -/
List.Shortlex.of_length_lt : ∀ {α : Type u_1} {r : α → α → Prop} {s t : List α}, s.length < t.length → List.Shortlex r s t
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `Equiv.cast (congrArg _ h)` as a linear equiv.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
LinearEquiv.cast : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_14} →
      {M : ι → Type u_15} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → {i j : ι} → i = j → M i ≃ₗ[R] M j
-- Mathlib.Order.Filter.Tendsto
Filter.map_mapsTo_Iic_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β},
  Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ Filter.Tendsto m F G
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_eq_quotient_center_plus_one`.

---

The nilpotency class of a non-trivial group is one more than its quotient by the center  -/
nilpotencyClass_eq_quotient_center_plus_one : ∀ {G : Type u_1} [inst : Group G] [hH : Group.IsNilpotent G] [Nontrivial G],
  Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ Subgroup.center G) + 1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : CommGroup A] [inst_12 : LieGroup I (↑⊤) A],
  smoothSheafCommGroup IM I M A = { obj := smoothPresheafCommGroup IM I M A, property := ⋯ }