mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `truncGE'.X K e i ≅ K.X (e.f i)` when `e.BoundaryGE i` does not hold.  -/
HomologicalComplex.truncGE'.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 : ∀ (i' : ι'), K.HasHomology i'] →
                    {i : ι} → ¬e.BoundaryGE i → (HomologicalComplex.truncGE'.X K e i ≅ K.X (e.f i))
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.invLimEquiv_apply_coe : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (nat : InverseSystem.IsNatEquiv f equiv) (t : ↑(InverseSystem.limit f i)) (l : ↑(Set.Iio i)) (l_1 : ↑(Set.Iio ↑l)),
  ↑((InverseSystem.invLimEquiv nat) t) l l_1 = (equiv l) (↑t l) l_1
-- Init.Data.List.MinMaxOn
List.minOn?_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β}, List.minOn? f (List.replicate n a) = if n = 0 then none else some a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.IsIso T.mor₂ → CategoryTheory.Limits.IsZero T.obj₁
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.homEquiv_eq`.

---

`h.homEquiv` acts like an "object comprehension" operator: it maps any characteristic map
`f : X ⟶ Ω` to the associated subobject of `X`, obtained by pulling back `h.Ω₀` along `f`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {X : C} (f : X ⟶ Ω),
  h.homEquiv f = (CategoryTheory.Subobject.pullback f).obj h.Ω₀
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffWithinAt.smul`

---

The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
set at this point.  -/
ContDiffWithinAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun i => f i • g i) s x
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The identity functor from `C` to `C`, where the codomain is given the
reversed braiding, upgraded to a braided functor.  -/
CategoryTheory.SymmetricCategory.equivReverseBraiding : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.SymmetricCategory C] → (CategoryTheory.Functor.id C).Braided
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- **Alias** of `CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom`. -/
CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  (F : CategoryTheory.Sheaf K A),
  ((G.sheafAdjunctionCocontinuous A J K).unit.app F).hom = (G.op.ranAdjunction A).unit.app F.obj
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The maximal tensor product is commutative.  -/
PointedCone.maxTensorProduct_comm : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {C₁ : PointedCone R G} {C₂ : PointedCone R H},
  PointedCone.map (↑(TensorProduct.comm R G H)) (C₁.maxTensorProduct C₂) = C₂.maxTensorProduct C₁
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂),
  ((I.ofPiForkFunctor hd).map f).hom = f.hom
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.rename.inj : ∀ {a a_1 : Lean.Lsp.RenameFile}, Lean.Lsp.DocumentChange.rename a = Lean.Lsp.DocumentChange.rename a_1 → a = a_1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i` on an open set `u` containing `x`, if a section `t` has `C^k`
coefficients at `x ∈ u` w.r.t. `s i`, then `t` is `C^n` at `x`.  -/
IsLocalFrameOn.contMDiffAt_of_coeff_aux : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} {t : (x : M) → V x} (hs : IsLocalFrameOn I F n s u) [VectorBundle 𝕜 F V]
  [FiniteDimensional 𝕜 F],
  (∀ (i : ι), ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n ((LinearMap.piApply (hs.coeff i)) t) x) →
    IsOpen u → x ∈ u → ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- The mapping cocone of a morphism `φ : K ⟶ L` of cochain complexes: it is
`(mappingCone φ)⟦(-1 : ℤ)⟧`.  -/
CochainComplex.mappingCocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} → (φ : K ⟶ L) → [HomologicalComplex.HasHomotopyCofiber φ] → CochainComplex C ℤ
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctorCompSnd_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op),
  (CategoryTheory.Comma.unopFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle, where one side is a multiple of a
rotation of another by `π / 2`.  -/
Orientation.tan_oangle_add_left_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 → ∀ (r : ℝ), (o.oangle (x + r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x)).tan = r⁻¹
-- Init.Data.UInt.Lemmas
UInt16.toUInt16_toUInt8 : ∀ (n : UInt16), n.toUInt8.toUInt16 = n % 256
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.comp_X_add_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → ∀ (r : R), (p.comp (Polynomial.X + Polynomial.C r)).Monic
-- Mathlib.Analysis.Calculus.Deriv.Add
hasStrictDerivAt_const_add_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasStrictDerivAt (fun x => c + f x) f' x ↔ HasStrictDerivAt f f' x
-- Init.Data.BitVec.Lemmas
BitVec.srem_zero : ∀ {w : ℕ} {x : BitVec w}, x.srem 0#w = x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivalence_unitIso : ∀ {I : Type u₁} {J : Type u₂} (e : I ≃ J),
  (CategoryTheory.Discrete.equivalence e).unitIso = CategoryTheory.Discrete.natIso fun i => CategoryTheory.eqToIso ⋯
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.Colimit.ι_map_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colim.map α))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι G j))
      ((CategoryTheory.ConcreteCategory.hom (α.app j)) x)
-- Mathlib.Data.FP.Basic
FP.Float.mul : [C : FP.FloatCfg] → FP.RMode → FP.Float → FP.Float → FP.Float
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) {Z : Ab}
  (h : M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Modules.smul
          ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r))
        h)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.zpow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) {k : ℤ}, padicValRat p (q ^ k) = k * padicValRat p q
-- Std.Http.Internal.Char
/-- tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
/ "+" / "-" / "." / "^" / "_" / "`" / "|" / "~"
/ DIGIT / ALPHA
; Visible token characters used to build `token`.
 -/
Std.Http.Internal.Char.tchar : Char → Bool
-- Lean.Elab.InfoTree.Types
Lean.Elab.ElabInfo.mk.inj : ∀ {elaborator : Lean.Name} {stx : Lean.Syntax} {elaborator_1 : Lean.Name} {stx_1 : Lean.Syntax},
  { elaborator := elaborator, stx := stx } = { elaborator := elaborator_1, stx := stx_1 } →
    elaborator = elaborator_1 ∧ stx = stx_1
-- Mathlib.Order.Interval.Finset.Nat
List.toFinset_range'_1_1 : ∀ (a : ℕ), (List.range' 1 a).toFinset = Finset.Icc 1 a
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.hComp'_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  {T₁₂ : CategoryTheory.Functor C₁ C₃} {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp T₂ ≅ T₁₂)
  (eB : B₁.comp B₂ ≅ B₁₂) (X : C₁),
  (w.hComp' w' eT eB).app X =
    CategoryTheory.CategoryStruct.comp (V₃.map (eT.inv.app X))
      (CategoryTheory.CategoryStruct.comp (w'.natTrans.app (T₁.obj X))
        (CategoryTheory.CategoryStruct.comp (B₂.map (w.natTrans.app X)) (eB.hom.app (V₁.obj X))))
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.map_sub : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (A' : Type u_8)
  [inst_2 : AddGroup A'] [inst_3 : DistribMulAction M A'] (B' : Type u_9) [inst_4 : AddGroup B']
  [inst_5 : DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x y : A'), f (x - y) = f x - f y
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `encodingProd`.  -/
Computability.finEncodingPair : {α : Type u_1} →
  {β : Type u_2} →
    {Γ₁ : Type u_3} →
      {Γ₂ : Type u_4} →
        [Fintype Γ₁] →
          [Fintype Γ₂] →
            Computability.Encoding α Γ₁ → Computability.Encoding β Γ₂ → Computability.Encoding (α × β) (Γ₁ ⊕ Γ₂)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E D),
  e.congrRight.counitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (X.associator e.inverse e.functor).hom
      (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.hom) X.rightUnitor.hom)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.op_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
-- Mathlib.RingTheory.Finiteness.Basic
/-- The submodule generated by a finset is `R`-finite.  -/
Module.Finite.span_finset : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Finset M),
  Module.Finite R ↥(Submodule.span R ↑s)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_congr : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign1 assign2 : α → Bool) (aig : Std.Sat.AIG α) (idx : ℕ)
  (invert : Bool) (hidx : idx < aig.decls.size),
  (∀ a ∈ aig, assign1 a = assign2 a) →
    ⟦assign1, { aig := aig, ref := { gate := idx, invert := invert, hgate := hidx } }⟧ =
      ⟦assign2, { aig := aig, ref := { gate := idx, invert := invert, hgate := hidx } }⟧
-- Mathlib.Algebra.Order.Group.Synonym
toColex_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), toColex (b • a) = b • toColex a
-- Mathlib.Order.Monotone.Defs
antitone_app : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder γ] (f : β → α → γ) (b : β),
  (Antitone fun a b => f b a) → Antitone (f b)
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_ofNatLT : ∀ {w : ℕ} (x : ℕ) (p : x < 2 ^ w), (x#'p).toNat = x
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.inv_inv : ∀ {a b : ENNReal}, a + b = 1 → a⁻¹.HolderConjugate b⁻¹
-- Mathlib.Algebra.Ring.Subgroup
AddSubgroup.mul_toAddSubmonoid : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (M N : AddSubgroup R),
  (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.SemanticTokensState.mk : Lean.Server.FileWorker.SemanticTokensState
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.app_one_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (s : CategoryTheory.Limits.Cotrident f) (j : J) {Z : C}
  (h :
    ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj
        CategoryTheory.Limits.WalkingParallelFamily.one ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f j)
      (CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) h) =
    CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero) h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- As long as the category has equalizers,
the image inclusion maps commute with `image.eqToIso`.
 -/
CategoryTheory.Limits.image.eq_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f']
  [CategoryTheory.Limits.HasEqualizers C] (h : f = f'),
  CategoryTheory.Limits.image.ι f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToIso h).hom (CategoryTheory.Limits.image.ι f')
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.Associative.ε₂_eq_mul : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c}
  {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β} {b : β},
  l.mapFinIdx f = [b] ↔ ∃ a, ∃ (w : l = [a]), f 0 a ⋯ = b
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_abs : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α), |↑(Equiv.Perm.sign f)| = 1
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablePartitionSet_mem : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) (a : α),
  MeasurableSpace.countablePartitionSet n a ∈ MeasurableSpace.countablePartition α n
-- Init.Data.Dyadic.Basic
/-- Negate a dyadic number.  -/
Dyadic.neg : Dyadic → Dyadic
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
MeasureTheory.Content.mk.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] (toFun toFun_1 : TopologicalSpace.Compacts G → NNReal)
  (e_toFun : toFun = toFun_1) (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂)
  (sup_disjoint' :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂)
  (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂),
  { toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } =
    { toFun := toFun_1, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
-- Mathlib.Order.Filter.Bases.Finite
Filter.ofSets_filter_eq_generate : ∀ {α : Type u_1} (s : Set (Set α)), (Filter.FilterBasis.ofSets s).filter = Filter.generate s
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- If a function is $C^{k+α}$ on a neighborhood of a point `a`,
i.e., it is $C^k$ on this neighborhood and $D^k f$ is Hölder continuous on it,
then the function is $C^{k+(α)}$ at `a`.  -/
ContDiffPointwiseHolderAt.of_contDiffOn_holderOnWith : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} {s : Set E} {C : NNReal},
  ContDiffOn ℝ (↑k) f s →
    s ∈ nhds a → HolderOnWith C ⟨↑α, ⋯⟩ (iteratedFDeriv ℝ k f) s → ContDiffPointwiseHolderAt k α f a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.isEmpty_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], IsEmpty (TopologicalSpace.NonemptyCompacts α) ↔ IsEmpty α
-- Mathlib.LinearAlgebra.AffineSpace.Slope
sub_smul_slope : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b : k), (b - a) • slope f a b = f b -ᵥ f a
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.ext_iff : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : ClosedAddSubgroup G},
  x = y ↔ (↑x).carrier = (↑y).carrier
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- See `linearGrowthInf_add_le` for a version with swapped argument `u` and `v`.  -/
LinearGrowth.linearGrowthInf_add_le' : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthInf u ≠ ⊥ ∨ LinearGrowth.linearGrowthSup v ≠ ⊤ →
    LinearGrowth.linearGrowthInf u ≠ ⊤ ∨ LinearGrowth.linearGrowthSup v ≠ ⊥ →
      LinearGrowth.linearGrowthInf (u + v) ≤ LinearGrowth.linearGrowthInf u + LinearGrowth.linearGrowthSup v
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizationMonoid.normUnit_zero : ∀ {α : Type u_2} {inst : MonoidWithZero α} [self : NormalizationMonoid α], normUnit 0 = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addRightReflectLT : ∀ {α : Type u} [inst : LT α] [inst_1 : Add α] [c : AddRightReflectLT α], AddRightReflectLT αᵒᵈ
-- Batteries.Tactic.HelpCmd
/-- The command `#help attribute` (or the short form `#help attr`) shows all attributes that have been
defined in the current environment.
Each attribute has a format like:
```
[inline]: mark definition to always be inlined
```
This says that `inline` is an attribute that can be placed on definitions like
`@[inline] def foo := 1`. (Individual attributes may have restrictions on where they can be
applied; see the attribute's documentation for details.) Both the attribute's `descr` field as well
as the docstring will be displayed here.

The form `#help attr id` will show only attributes that begin with `id`.
 -/
Batteries.Tactic.«command#help_AttrAttribute___» : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h' : k ∈ Std.DTreeMap.filterMap f t), (f k (t.get k ⋯)).isSome = true
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.eq_of_isLongestMatchAt_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos →
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos startPos → startPos = endPos
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∃ s, IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.adjoin R ↑s)) S) (IsUnit.submonoid S)) S) →
    Algebra.EssFiniteType R S
-- Mathlib.Analysis.Distribution.Distribution
Distribution.instContinuousLineDerivTopENat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F], ContinuousLineDeriv E (Distribution Ω F ⊤) (Distribution Ω F ⊤)