mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Box product of simple graphs. It relates `(a₁, b)` and `(a₂, b)` if `G` relates `a₁` and `a₂`,
and `(a, b₁)` and `(a, b₂)` if `H` relates `b₁` and `b₂`.  -/
SimpleGraph.boxProd : {α : Type u_1} → {β : Type u_2} → SimpleGraph α → SimpleGraph β → SimpleGraph (α × β)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.eventuallyEq_of_toReal_eventuallyEq : ∀ {α : Type u_1} {l : Filter α} {f g : α → ENNReal},
  (∀ᶠ (x : α) in l, f x ≠ ⊤) →
    (∀ᶠ (x : α) in l, g x ≠ ⊤) → ((fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal) → f =ᶠ[l] g
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The inverse of a partial equivalence  -/
PartialEquiv.symm : {α : Type u_1} → {β : Type u_2} → PartialEquiv α β → PartialEquiv β α
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight_zero : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (x : Finset α × Finset α),
  Finset.addETransformRight 0 x = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β}, (Std.ExtDHashMap.Const.modify m k f).contains k' = m.contains k'
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `deriv_fun_finsetProd`. -/
deriv_fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) →
    deriv (fun x => ∏ i ∈ u, f i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.hasInducedTStructure_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : P.IsTriangulated],
  P.HasInducedTStructure t ↔
    ∀ (A : C),
      P A →
        ∃ X Y,
          ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1),
            ∃ f g h,
              ∃ (_ :
                CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
                  CategoryTheory.Pretriangulated.distinguishedTriangles),
                P.isoClosure X ∧ P.isoClosure Y
-- Init.GetElem
List.instLawfulGetElemNatLtLength : ∀ {α : Type u_1}, LawfulGetElem (List α) ℕ α fun as i => i < as.length
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_neg_iff`. -/
Wbtw.neg : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V}, Wbtw R x y z → Wbtw R (-x) (-y) (-z)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.map_modByMonic : ∀ {R : Type u} {S : Type v} [inst : Ring R] {p q : Polynomial R} [inst_1 : Ring S] (f : R →+* S),
  q.Monic → Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
-- Std.Data.DTreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Const.getThenInsertIfNew? : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → β → Option β × Std.DTreeMap α (fun x => β) cmp
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_inj : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c.toSetoid = d.toSetoid ↔ c = d
-- Mathlib.RingTheory.Congruence.Hom
/-- The first isomorphism theorem for rings in the case of a surjective homomorphism.

For a `computable` version, see `RingCon.quotientKerEquivOfRightInverse`.
 -/
RingCon.quotientKerEquivOfSurjective : {M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring P] → (f : M →+* P) → Function.Surjective ⇑f → (RingCon.ker f).Quotient ≃+* P
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_op₂ : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [inst : (i : ι) → Zero (M i)]
  [inst_1 : (i : ι) → Zero (N i)] [inst_2 : (i : ι) → Zero (O i)] [inst_3 : DecidableEq ι]
  (op : (i : ι) → M i → N i → O i),
  (∀ (i : ι), op i 0 0 = 0) →
    ∀ (i : ι) (x : M i) (y : N i), Pi.single i (op i x y) = fun j => op j (Pi.single i x j) (Pi.single i y j)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty =
        ((t.isEmpty || t.size == 1 && Std.DTreeMap.Internal.Impl.contains k t) && (f (t.get? k)).isNone)
-- Init.SimpLemmas
true_iff : ∀ (p : Prop), (True ↔ p) = p
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_assoc : ∀ {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.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ f₃ : L.obj X ⟶ L.obj Y),
  CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.Localization.Preadditive.add' W f₁ f₂) f₃ =
    CategoryTheory.Localization.Preadditive.add' W f₁ (CategoryTheory.Localization.Preadditive.add' W f₂ f₃)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₅_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_451✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_452✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄.hom =
      CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_453✝))
  (w₄ :
    CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅.hom =
      CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_453✝ _proof_454✝)),
  (CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).hom =
    CategoryTheory.ComposableArrows.homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄
-- Mathlib.Data.Finset.Basic
Finset.erase_sdiff_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), s.erase a \ t = (s \ t).erase a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
/-- Returns `.done` for Char values.

These values should not be unfolded in the symbolic evaluator.

In regular `simp`, the nested raw literal should be prevented from being converted into an
`OfNat.ofNat` application.
 -/
Char.isValue : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_three_add_inv_three : 3⁻¹ + 3⁻¹ + 3⁻¹ = 1
-- Aesop.Options.Internal
Aesop.Options'.generateScript : Aesop.Options' → Bool
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_eq_cfcₙ_real : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A]
  [IsSemitopologicalRing A] (a : A) (y : NNReal),
  autoParam (0 ≤ a) CFC.nnrpow_eq_cfcₙ_real._auto_1 → a ^ y = cfcₙ (fun x => x ^ ↑y) a
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_sub_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g g' : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g - g') h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f g') h
-- Mathlib.Algebra.RingQuot
RingQuot.instSub : {R : Type uR} → [inst : Ring R] → (r : R → R → Prop) → Sub (RingQuot r)
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_3.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (x x_1 : ℕ) (h_1 : Unit → motive 1 0) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_2 : ℕ) → motive x x_2),
  (x = 1 → x_1 = 0 → False) →
    (∀ (i j : ℕ), x = i.succ → x_1 = j.succ → False) →
      (match x, x_1 with
        | 1, 0 => h_1 ()
        | i.succ, j.succ => h_2 i j
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderStateRefT' : {m : Type → Type} →
  {ω σ α : Type} → [inst : Lean.Order.PartialOrder (m α)] → Lean.Order.PartialOrder (StateRefT' ω σ m α)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes, this
is the canonical morphism (which is a homotopy equivalence) from the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)` to `mappingCone g`.  -/
CochainComplex.MappingConeCompHomotopyEquiv.inv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (f : X₁ ⟶ X₂) →
            (g : X₂ ⟶ X₃) →
              CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁ ⟶
                CochainComplex.mappingCone g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      (m₁.diff m₂ ⋯).get! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default else m₁.get! k
-- Init.GetElem
getElem_congr_coll : ∀ {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  {c d : coll} {i : idx} {w : valid c i} (h : c = d), c[i] = d[i]
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of the forward direction of `QuadraticMap.isOrtho_comm`. -/
QuadraticMap.IsOrtho.symm : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} {x y : M}, Q.IsOrtho x y → Q.IsOrtho y x
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticMap.IsometryEquiv.map_negDef_iff : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : AddCommGroup M] [inst_1 : AddCommGroup M'] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [inst_4 : Module R M] {Q : QuadraticForm R M} [inst_5 : Module R M']
  {Q' : QuadraticForm R M'} {V : Submodule R M} (e : QuadraticMap.IsometryEquiv Q Q'),
  (QuadraticMap.restrict (-Q') (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (QuadraticMap.restrict (-Q) V).PosDef
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ioo_left : ∀ {α : Type u_2} {a₁ a₂ b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ a₂ → Finset.Ioo a₂ b ⊆ Finset.Ioo a₁ b
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The ideal of `A ⊗[R] B` generated by `I` is the image of `A ⊗[R] I`  -/
Ideal.map_includeRight_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B),
  Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeRight I) =
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- An operation on multiseries called a "friend" if any `n`-prefix of its output depends only on
the `n`-prefix of the input. Such operations can be used in the tail of (non-primitive) corecursive
definitions.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
      Prop
-- Mathlib.Analysis.Matrix.Order
Matrix.instIsOrderedAddMonoid : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜], IsOrderedAddMonoid (Matrix n n 𝕜)
-- Mathlib.Analysis.MellinTransform
MellinConvergent.div_const : ∀ {f : ℝ → ℂ} {s : ℂ}, MellinConvergent f s → ∀ (a : ℂ), MellinConvergent (fun t => f t / a) s
-- Mathlib.Analysis.Real.Hyperreal
/-- A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧. 

Conventions for notations in identifiers:

 * The recommended spelling of `ε` in identifiers is `epsilon`. -/
Hyperreal.termε : Lean.ParserDescr
-- Mathlib.Order.Filter.Pointwise
Filter.map_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] {f₁ f₂ : Filter α}
  [inst_2 : FunLike F α β] [MulHomClass F α β] (m : F),
  Filter.map (⇑m) (f₁ * f₂) = Filter.map (⇑m) f₁ * Filter.map (⇑m) f₂
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instTop.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  SaturatedSubmonoid.instTop =
    {
      top :=
        let __src := ⊤;
        { toSubmonoid := __src, mulSaturated := ⋯ } }
-- Mathlib.Analysis.Normed.Field.Ultra
isUltrametricDist_iff_forall_norm_natCast_le_one : ∀ {R : Type u_1} [inst : NormedDivisionRing R], IsUltrametricDist R ↔ ∀ (n : ℕ), ‖↑n‖ ≤ 1
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a.fdiv b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init ↑m = forIn (↑m).toList init fun a b => f a.fst a.snd b
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_mem_interior : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.incenter ∈ s.interior
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame : Type
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is `C^1` on `uIcc a b`, then `f` is absolutely continuous on `uIcc a b`.  -/
ContDiffOn.absolutelyContinuousOnInterval : ∀ {a b : ℝ} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
  ContDiffOn ℝ 1 f (Set.uIcc a b) → AbsolutelyContinuousOnInterval f a b
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tprod_apply : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → CommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} [L.NeBot] [∀ (x : α), T2Space (X x)]
  {f : ι → (x : α) → X x} {x : α}, Multipliable f L → (∏'[L] (i : ι), f i) x = ∏'[L] (i : ι), f i x
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
      (CategoryTheory.Limits.kernelSubobject f').arrow =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow
      (CategoryTheory.Arrow.Hom.left sq)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp.sizeOf_spec : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ) =
    1 + sizeOf e + sizeOf f + sizeOf g + sizeOf h + sizeOf η + sizeOf θ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover),
  (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).inv = e.inv
-- Mathlib.Data.Finset.Sort
Finset.sort_range : ∀ (n : ℕ), ((Finset.range n).sort fun a b => a ≤ b) = List.range n
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (f' : F.obj j ⟶ X)
  (w₁ :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam)
  (w₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam)
  (f'_1 : F.obj j ⟶ X)
  (w₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f'_1 = f)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam)
  (w₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f'_1 p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam),
  ({ f' := f', w₁ := w₁, w₂ := w₂ } = { f' := f'_1, w₁ := w₁_1, w₂ := w₂_1 }) = (f' = f'_1)
-- Mathlib.Order.Category.Semilat
SemilatInfCat.instConcreteCategoryInfTopHomX : CategoryTheory.ConcreteCategory SemilatInfCat fun x1 x2 => InfTopHom x1.X x2.X
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ}, HahnSeries.coeff 0 a = 0
-- Lean.Exception
Lean.AddErrorMessageContext.mk : {m : Type → Type} →
  (Lean.Syntax → Lean.MessageData → m (Lean.Syntax × Lean.MessageData)) → Lean.AddErrorMessageContext m
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity `l`, and its derivative is nonpositive, then the
integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
`integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and
continuity at `a⁺`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  ContinuousWithinAt g (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, g' x ≤ 0) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.toPreErgodic : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) Ergodic._auto_1},
  Ergodic f μ → PreErgodic f μ
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
deriv_comp_add_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜), deriv (fun x => f (x + a)) x = deriv f (x + a)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toIsAffineHom : AlgebraicGeometry.IsAffineHom f],
  (∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).Finite) →
    AlgebraicGeometry.IsFinite f
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g),
  CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c =
    CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯) (CategoryTheory.Under.homMk c.inr ⋯)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Iic : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.castAddEmb m) (Finset.Iic i) = Finset.Iic (Fin.castAdd m i)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.apply_inl_apply_inr_eq_of_mem_boundary_sum : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X)
  (p : ↑(GenLoop M (↑(GenLoop N X x)) GenLoop.const)) {y : M ⊕ N → ↑unitInterval},
  y ∈ Cube.boundary (M ⊕ N) → (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x
-- Aesop.Tree.Data
Aesop.Goal.unsafeQueue? : Aesop.Goal → Option Aesop.UnsafeQueue
-- Mathlib.Order.Types.Defs
/-- A "canonical" type order-isomorphic to the order type `o`, living in the same universe.
This is defined through the axiom of choice.  -/
OrderType.ToType : OrderType.{u} → Type u
-- Mathlib.Order.WithBot
WithTop.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u_1} [inst : IsEmpty α], WithTop.instUniqueOfIsEmpty = { toInhabited := WithTop.inhabited, uniq := ⋯ }
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.coe_compAlternatingMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N), ⇑(g.compAlternatingMap f) = ⇑g ∘ ⇑f
-- Lean.Log
/-- Log a new message.  -/
Lean.MonadLog.logMessage : {m : Type → Type} → [self : Lean.MonadLog m] → Lean.Message → m Unit
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If for all `m ≤ n` and every `i : cell C m` the intersection `A ∩ closedCell m j` is closed
and `A ∩ D` is closed then `A ∩ cellFrontier (n + 1) j` is closed for every
`j : cell C (n + 1)`.  -/
Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {A : Set X}
  {n : ℕ},
  (∀ m ≤ n, ∀ (j : Topology.RelCWComplex.cell C m), IsClosed (A ∩ Topology.RelCWComplex.closedCell m j)) →
    ∀ (j : Topology.RelCWComplex.cell C (n + 1)),
      IsClosed (A ∩ D) → IsClosed (A ∩ Topology.RelCWComplex.cellFrontier (n + 1) j)