mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_himp_mp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R) →
    Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel P R
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel_not_iso_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f],
  f ≠ 0 → CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π f) → False
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insert_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).size ≤ t.size + 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context.mk : ℕ → Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk.sizeOf_spec : ∀ {𝕜 : Type u_7} {α : Type u_8} [inst : Zero 𝕜] [inst_1 : LE α] [inst_2 : SizeOf 𝕜] [inst_3 : SizeOf α]
  (toFun : α → α → 𝕜) (eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0),
  sizeOf { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' } = 1
-- Mathlib.Order.Interval.Set.Defs
Set.Ioc_def : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), {x | a < x ∧ x ≤ b} = Set.Ioc a b
-- Mathlib.Data.Set.Prod
/-- **Alias** of `Set.prod_mono_right`. -/
Set.prod_subset_prod_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → s ×ˢ t₁ ⊆ s ×ˢ t₂
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.push k a q with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_1 k a q
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add β] (f g : α → β),
  UniformFun.ofFun (f + g) = UniformFun.ofFun f + UniformFun.ofFun g
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_eq_sub_single : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type u_1} [inst_1 : (i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i)
  (i : ι), DFinsupp.erase i f = f - fun₀ | i => f i
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_forall_map_le' : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : Gal(L/F)), IntermediateField.map (↑σ) K ≤ K
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.toAddCommSemigroup.eq_1 : ∀ {M : Type u_5} [inst : AddCommSemigroup M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddMemClass A M] (S : A),
  AddMemClass.toAddCommSemigroup S = { toAddSemigroup := AddMemClass.toAddSemigroup S, add_comm := ⋯ }
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.disjoint_left_ordSeparatingSet : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α}, Disjoint s (s.ordSeparatingSet t)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R (n - 2) = Polynomial.X * Polynomial.Chebyshev.S R (n - 1) - Polynomial.Chebyshev.S R n
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.lt_tsub_of_add_lt_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable a → a + c < b → c < b - a
-- Mathlib.Tactic.Basic
/-- Syntax for the `variables` command: this command is just a stub,
and merely warns that it has been renamed to `variable` in Lean 4.  -/
Mathlib.Tactic.variables : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasFDerivWithinAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {f' g' : G →L[ℝ] E} {s : Set G} {x : G},
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      HasFDerivWithinAt (fun t => inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') s x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Construct a strong natural transformation from an oplax natural transformation whose
naturality 2-morphism is an isomorphism.  -/
CategoryTheory.Oplax.StrongTrans.mkOfOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : CategoryTheory.Oplax.OplaxTrans F G) → η.StrongCore → CategoryTheory.Oplax.StrongTrans F G
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.restrict : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ {s : Set α}, MeasureTheory.AECover (μ.restrict s) l φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      k' ∈ Std.DTreeMap.Internal.Impl.alter! k f t ↔
        if compare k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' ∈ t
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.hasPow : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → Pow (HomogeneousLocalization 𝒜 x) ℕ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray.eq_1 : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray clauses =
    { clauses := clauses, rupUnits := #[], ratUnits := #[],
      assignments :=
        Array.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn
          (Array.replicate n Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned) clauses }
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`.
See `quotientToQuotientRangePowQuotSucc` for this as a linear map,
and `quotientRangePowQuotSuccInclusionEquiv` for this as a linear equivalence.
 -/
Ideal.quotientToQuotientRangePowQuotSuccAux : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            (P : Ideal S) →
              {i : ℕ} →
                {a : S} →
                  a ∈ P ^ i →
                    S ⧸ P →
                      ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) ⧸
                        (p.powQuotSuccInclusion P i).range
-- Mathlib.Algebra.Homology.SpectralObject.Homology
/-- The homology of the short complex
`E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)` identifies to
`E^n(f₂ ≫ f₃, f₄, f₅ ≫ f₆)`.  -/
CategoryTheory.Abelian.SpectralObject.dHomologyIso : {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₃) →
                              CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                                (f₅₆ : i₄ ⟶ i₆) →
                                  CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆ →
                                    (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                      (hn₁ :
                                          autoParam (n₀ + 1 = n₁)
                                            CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_1) →
                                        (hn₂ :
                                            autoParam (n₁ + 1 = n₂)
                                              CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_3) →
                                          (hn₃ :
                                              autoParam (n₂ + 1 = n₃)
                                                CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_5) →
                                            (hn₄ :
                                                autoParam (n₃ + 1 = n₄)
                                                  CategoryTheory.Abelian.SpectralObject.dHomologyIso._auto_7) →
                                              (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯ ⋯).homology ≅
                                                X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_compl : ∀ {α : Type u_1} [inst : BooleanRing α] (a : AsBoolAlg α), ofBoolAlg aᶜ = 1 + ofBoolAlg a
-- Mathlib.Data.Finset.Insert
Finset.coe_eq_pair : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, ↑s = {a, b} ↔ s = {a, b}
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.tensor_add_right : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (f : ρ.IntertwiningMap σ) (g₁ g₂ : τ.IntertwiningMap π), f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_apply : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C} (f : L₁.obj X ⟶ L₁.obj Y),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) f = (CategoryTheory.LocalizerMorphism.id W).homMap L₁ L₂ f
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- Typecheck a `CoalgHom` as a morphism in `CoalgCat R`.  -/
CoalgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommGroup Y] →
            [inst_4 : Module R Y] →
              [inst_5 : Coalgebra R X] → [inst_6 : Coalgebra R Y] → (X →ₗc[R] Y) → (CoalgCat.of R X ⟶ CoalgCat.of R Y)
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- `ContinuousAlgEquiv R A B`, with notation `A ≃A[R] B`, is the type of bijections
between the topological `R`-algebras `A` and `B` which are both homeomorphisms
and `R`-algebra isomorphisms.
 -/
«term_≃A[_]_» : Lean.TrailingParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.ofBool.eq_1 : ∀ (b : Bool), BitVec.ofBool b = bif b then 1 else 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_4.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_5 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableExtraTheorem.hash : Lean.Elab.Tactic.Grind.ExtraTheorem → UInt64
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.single.eq_1 : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J),
  CategoryTheory.GradedObject.single j =
    { obj := fun X i => if i = j then X else ⊥_ C,
      map := fun {X₁ X₂} f i =>
        if h : i = j then
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
        else CategoryTheory.eqToHom ⋯,
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.ModelCategory C] → HomotopicalAlgebra.CategoryWithWeakEquivalences C
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.congrIsometry_refl_refl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  TensorProduct.congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F) =
    LinearIsometryEquiv.refl 𝕜 (TensorProduct 𝕜 E F)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of the ring of integers of `K` in the mixed space.  -/
NumberField.mixedEmbedding.integerLattice : (K : Type u_1) → [inst : Field K] → Submodule ℤ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_intCast : ∀ {R : Type u_1} [inst : AddGroupWithOne R] [inst_1 : Mul R] (c : RingCon R) (n : ℕ), ↑↑n = ↑n
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.mul_right : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : MulZeroClass β] {f f' : α → β},
  HasCompactSupport f → HasCompactSupport (f * f')
-- Init.Data.Vector.Algebra
Vector.smul_zero : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} [inst : Zero β] [inst_1 : SMul α β],
  (∀ (c : α), c • 0 = 0) → ∀ (c : α), c • 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- Given a morphism of presheaves of commutative rings `φ : S ⟶ F.op ⋙ R`,
this is the type of relative `φ`-derivation of a presheaf of `R`-modules `M`.  -/
PresheafOfModules.Derivation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)) →
                (S ⟶ F.op.comp R) → Type (max (max u u₂) v)
-- Mathlib.Data.Multiset.Fintype
Multiset.map_fst_le_of_subset_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {s : Finset (α × ℕ)},
  s ⊆ m.toEnumFinset → Multiset.map Prod.fst s.val ≤ m
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.instMul.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : One M] [inst_1 : MulOneClass N],
  OneHom.instMul = { mul := fun f g => { toFun := fun m => f m * g m, map_one' := ⋯ } }
-- Mathlib.Order.CompactlyGenerated.Basic
Directed.inf_iSup_eq : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
-- Mathlib.Tactic.Algebraize
/-- Version of `algebraize`, which only adds `Algebra` instances and `IsScalarTower` instances,
but does not try to add any instances about any properties tagged with
`@[algebraize]`, like for example `Finite` or `IsIntegral`.  -/
Mathlib.Tactic.tacticAlgebraize_only__ : Lean.ParserDescr
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_6 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match n.succ.succ.succ.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_6 n
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).map CategoryTheory.Limits.WalkingReflexivePair.Hom.right = g
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.tsum_coe : ∀ {α : Type u_1} (p : PMF α), ∑' (a : α), p a = 1
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `locallyLipschitzOn_neg_iff`. -/
LocallyLipschitzOn.neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s (-f)
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- A faithful functor equipped with a `InducingFunctorData` structure is monoidal.  -/
CategoryTheory.Monoidal.fromInducedCoreMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategoryStruct D] →
            (F : CategoryTheory.Functor D C) →
              [inst_4 : F.Faithful] → (fData : CategoryTheory.Monoidal.InducingFunctorData F) → F.CoreMonoidal
-- Init.Tactics
/-- Syntax for omitting a local hypothesis in `solve_by_elim`.  -/
Lean.Parser.Tactic.SolveByElim.erase : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lidOfCompatibleSMul_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_4) (M : Type u_5) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : CommSemiring A] [inst_4 : Module A M] [inst_5 : Module R A] [inst_6 : SMulCommClass R A A]
  [inst_7 : TensorProduct.CompatibleSMul R A A M] [inst_8 : TensorProduct.CompatibleSMul A R A M] (a : A) (m : M),
  (TensorProduct.lidOfCompatibleSMul R A M) (a ⊗ₜ[R] m) = a • m
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_antidistrib_right`.  -/
Option.map_map₂_right_anticomm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6}
  {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' b a)) → Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' b a)
-- Std.Data.String.ToNat
String.toNat?_eq_none_iff : ∀ {s : String}, s.toNat? = none ↔ s.isNat = false
-- Mathlib.Topology.Connected.PathConnected
Function.Surjective.pathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PathConnectedSpace X]
  {f : X → Y}, Function.Surjective f → Continuous f → PathConnectedSpace Y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_inv : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Inv β], MeasureTheory.stoppedProcess u⁻¹ τ = (MeasureTheory.stoppedProcess u τ)⁻¹
-- Mathlib.Analysis.InnerProductSpace.NormPow
hasDerivAt_abs_rpow : ∀ (x : ℝ) {p : ℝ}, 1 < p → HasDerivAt (fun x => |x| ^ p) (p * |x| ^ (p - 2) * x) x
-- Mathlib.Topology.Order.Basic
instIsCountablyGenerated_atTop : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [TopologicalSpace.SeparableSpace α], Filter.atTop.IsCountablyGenerated