mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.desc.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁),
  HomologicalComplex.cylinder.desc φ₀ φ₁ h =
    HomologicalComplex.homotopyCofiber.desc
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))
      (CategoryTheory.Limits.biprod.desc φ₀ φ₁) ((Homotopy.ofEq ⋯).trans (Homotopy.equivSubZero h))
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (c : F), fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x
-- Mathlib.Algebra.Algebra.Operations
Submodule.restrictScalars_image_smul_eq : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_1} {M : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra S R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M] (s : Set S)
  (N : Submodule R M), Submodule.restrictScalars S (⇑(algebraMap S R) '' s • N) = s • Submodule.restrictScalars S N
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonLet : Array Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H N : AddSubgroup G} [N.Normal], (N.addSubgroupOf H).Normal
-- Init.Prelude
/-- Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : UInt8) ≤ 7 by decide`
 -/
UInt8.decLe : (a b : UInt8) → Decidable (a ≤ b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Every diagram indexing a pullback is naturally isomorphic (actually, equal) to a `cospan`  -/
CategoryTheory.Limits.diagramIsoCospan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C) →
      F ≅
        CategoryTheory.Limits.cospan (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
          (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)
-- Mathlib.Order.Filter.CountableInter
countable_sInter_mem : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {S : Set (Set α)}, S.Countable → (⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E},
  p ≠ ⊤ →
    ∀ {μ : MeasureTheory.Measure β} (fmeas : Measurable f)
      [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})],
      MeasureTheory.eLpNorm f p μ < ⊤ →
        Filter.Tendsto
          (fun n =>
            MeasureTheory.eLpNorm (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ)
          Filter.atTop (nhds 0)
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left : ∀ (m n k : ℕ), (m * n).gcd (m * k) = m * n.gcd k
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.any_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {p : (a : α) → β a → Bool}, t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_preimage : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [Finite ι] {F : Type u_5} [inst_2 : FunLike F (ι → ℕ) M]
  [AddMonoidHomClass F (ι → ℕ) M] {s : Set M}, IsSemilinearSet s → ∀ (f : F), IsSemilinearSet (⇑f ⁻¹' s)
-- Init.Data.SInt.Lemmas
Int32.toInt64_div_of_ne_right : ∀ (a b : Int32), b ≠ -1 → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Init.Data.Array.Lemmas
Array.set_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} {h : i < xs.size}, xs.set i a h = #[] ↔ xs = #[]
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getEntryLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mk.sizeOf_spec : ∀ {n : ℕ} (boundaries : Finset (Fin n.succ)) (zero_mem : 0 ∈ boundaries) (getLast_mem : Fin.last n ∈ boundaries),
  sizeOf { boundaries := boundaries, zero_mem := zero_mem, getLast_mem := getLast_mem } =
    1 + sizeOf boundaries + sizeOf zero_mem + sizeOf getLast_mem
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.addSubMap_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [IsReduced R] {x : Fin 3 → R},
  x ≠ 0 → (fun i => (MvPolynomial.eval x) (W.addSubMap i)) ≠ 0
-- Mathlib.Algebra.Algebra.Defs
/-- Compose an `Algebra` with a `RingHom`, with action `f s • m`.

This is the algebra version of `Module.compHom`.
 -/
Algebra.compHom : {R : Type u} →
  {S : Type v} →
    (A : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → [inst_2 : Semiring A] → [Algebra R A] → (S →+* R) → Algebra S A
-- Init.Data.List.Erase
List.eraseIdx_of_length_le : ∀ {α : Type u_1} {l : List α} {k : ℕ}, l.length ≤ k → l.eraseIdx k = l
-- Mathlib.Combinatorics.Graph.Delete
Graph.induce_isLink : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (e : β) (x y : α),
  (G.induce X).IsLink e x y = (G.IsLink e x y ∧ x ∈ X ∧ y ∈ X)
-- Mathlib.Order.Category.FinPartOrd
/-- The category of finite partial orders with monotone functions.  -/
FinPartOrd : Type (u_1 + 1)
-- Mathlib.Algebra.Lie.OfAssociative
/-- The map `ofAssociativeAlgebra` associating a Lie algebra to an associative algebra is
functorial.  -/
AlgHom.toLieHom : {A : Type v} →
  [inst : Ring A] →
    {R : Type u} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R A] → {B : Type w} → [inst_3 : Ring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → A →ₗ⁅R⁆ B
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.WidePullbackShape.fintypeObj : {J : Type v} → [Fintype J] → Fintype (CategoryTheory.Limits.WidePullbackShape J)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_one : UInt64.toBitVec 1 = 1#64
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(yoneda.obj X).obj (op Y) = Y ⟶ X`.  -/
CategoryTheory.yoneda_obj_obj_eq_hom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → C → C → Prop
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.FormatterM : Type → Type
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.mk.sizeOf_spec : ∀ (textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities) (window? : Option Lean.Lsp.WindowClientCapabilities)
  (workspace? : Option Lean.Lsp.WorkspaceClientCapabilities) (lean? : Option Lean.Lsp.LeanClientCapabilities),
  sizeOf { textDocument? := textDocument?, window? := window?, workspace? := workspace?, lean? := lean? } =
    1 + sizeOf textDocument? + sizeOf window? + sizeOf workspace? + sizeOf lean?
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- For a sheaf `F`, `F(U ⊔ V)` is the pullback of `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)`.
This is the pullback cone.  -/
TopCat.Sheaf.interUnionPullbackCone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Sheaf C X) →
        (U V : TopologicalSpace.Opens ↑X) →
          CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
            (F.obj.map (CategoryTheory.homOfLE ⋯).op)
-- Mathlib.Data.List.TakeDrop
List.dropSlice_eq : ∀ {α : Type u} (xs : List α) (n m : ℕ), List.dropSlice n m xs = List.take n xs ++ List.drop (n + m) xs
-- Mathlib.Data.Num.Basic
/-- Representation of integers using trichotomy around zero.

```
13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
-13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one)))
```  -/
ZNum : Type
-- Mathlib.Order.Directed
IsMin.not_isMax : ∀ {β : Type u_2} [inst : PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] {b : β}, IsMin b → ¬IsMax b
-- Mathlib.Order.WithBot
WithBot.map_comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ),
  WithBot.map g ∘ WithBot.map f = WithBot.map (g ∘ f)
-- Std.Data.DTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.DTreeMap.foldrM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → ((a : α) → β a → δ → m δ) → δ → Std.DTreeMap α β cmp → m δ
-- Init.Data.String.Basic
String.Slice.Pos.le_trans : ∀ {s : String.Slice} {p q r : s.Pos}, p ≤ q → q ≤ r → p ≤ r
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.finset_logSizeBallSeq_zero : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), (PairReduction.logSizeBallSeq J hJ a c 0).finset = J
-- Mathlib.Topology.Compactness.Compact
Topology.IsInducing.isCompact_preimage_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → ∀ {K : Set Y}, K ⊆ Set.range f → (IsCompact (f ⁻¹' K) ↔ IsCompact K)
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.ofMatrix_rel : ∀ {R : Type u_1} {n : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {c : RingCon (Matrix n n R)} {x y : R}, c.ofMatrix x y ↔ ∀ (i j : n), c (Matrix.single i j x) (Matrix.single i j y)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `![1, I]` is an orthonormal basis for `ℂ` considered as a real inner product space.  -/
Complex.orthonormalBasisOneI : OrthonormalBasis (Fin 2) ℝ ℂ
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instOne.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → One (M i)], Pi.instOne = { one := fun x => 1 }
-- Mathlib.Dynamics.OmegaLimit
eventually_closure_subset_of_isOpen_of_omegaLimit_subset : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [CompactSpace β] {v : Set β}, IsOpen v → omegaLimit f ϕ s ⊆ v → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ v
-- Std.Data.Iterators.Combinators.Monadic.Zip
/-- Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
outputs of `left` and `right`. When one of them terminates,
the `zip` iterator will also terminate.

**Marble diagram:**

```text
left               --a        ---b        --c
right                 --x         --y        --⊥
left.zip right     -----(a, x)------(b, y)-----⊥
```

**Termination properties:**

* `Finite` instance: only if either `left` or `right` is finite and the other is productive
* `Productive` instance: only if `left` and `right` are productive

There are situations where `left.zip right` is finite (or productive) but none of the instances
above applies. For example, if the computation happens in an `Except` monad and `left` immediately
fails when calling `step`, then `left.zip right` will also do so. In such a case, the `Finite`
(or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator incurs an additional O(1) cost with each step taken by `left` or `right`.

Right now, the compiler does not unbox the internal state, leading to worse performance than
possible.
 -/
Std.IterM.zip : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] → {α₂ β₂ : Type w} → Std.IterM m β₁ → Std.IterM m β₂ → Std.IterM m (β₁ × β₂)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulConstC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulConstC k p c) =
    ↑k * Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.MeasureTheory.Measure.IntegralCharFun
/-- A bound on the measure of the set `{x | r < |x|}` in terms of the integral of
the characteristic function, for a probability measure on `ℝ`.  -/
MeasureTheory.measureReal_abs_gt_le_integral_charFun : ∀ {μ : MeasureTheory.Measure ℝ} {r : ℝ} [MeasureTheory.IsProbabilityMeasure μ],
  0 < r → μ.real {x | r < |x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - MeasureTheory.charFun μ t‖
-- Mathlib.Order.Interval.Set.LinearOrder
Set.notMem_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a c : α}, c ∉ Set.Iic a ↔ a < c
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_n : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (C : PrimeSpectrum.BasicConstructibleSetData R), (PrimeSpectrum.BasicConstructibleSetData.map φ C).n = C.n
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.sub_martingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Submartingale (f - g) ℱ μ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HasHomology.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), S.HasHomology
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns an `Array` of the keys in order.  -/
Std.DTreeMap.Internal.Impl.keysArray : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Array α
-- Init.Data.Array.Sort.Lemmas
Subarray.mergeSort.induct_unfolding : ∀ {α : Type u_1} (le : α → α → Bool) (motive : Subarray α → Array α → Prop),
  (∀ (x : Subarray α),
      1 < Std.Slice.size x →
        have splitIdx := (Std.Slice.size x + 1) / 2;
        have left := Std.Rio.Sliceable.mkSlice x *...splitIdx;
        have right := Std.Rci.Sliceable.mkSlice x splitIdx...*;
        motive left (left.mergeSort le) →
          motive right (right.mergeSort le) →
            motive x (Array.MergeSort.Internal.merge✝ (left.mergeSort le) (right.mergeSort le) le)) →
    (∀ (x : Subarray α), ¬1 < Std.Slice.size x → motive x (Std.Slice.toArray x)) →
      ∀ (xs : Subarray α), motive xs (xs.mergeSort le)
-- Std.Http.Data.Status
Std.Http.Status.noContent.sizeOf_spec : sizeOf Std.Http.Status.noContent = 1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mulRightMono : MulRightMono Ordinal.{u}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : m₂.contains k = true),
  Std.ExtDHashMap.Const.get (m₁.union m₂) k ⋯ = Std.ExtDHashMap.Const.get m₂ k mem
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The trivial zeroes of the zeta function.  -/
riemannZeta_neg_two_mul_nat_add_one : ∀ (n : ℕ), riemannZeta (-2 * (↑n + 1)) = 0
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ext : ∀ {X Y : HeytAlg} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_div : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p / q) = ↑p / ↑q
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.getThenInsertIfNew? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {b : β a}, t.WF → (t.getThenInsertIfNew? a b).2.WF
-- Std.Http.Data.Body.Full
/-- Builds a request with a JSON body.
Sets `Content-Type: application/json`.
 -/
Std.Http.Request.Builder.json : Std.Http.Request.Builder → String → Std.Async.Async (Std.Http.Request Std.Http.Body.Full)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The configuration state of a Turing machine during operation
consists of a label (machine state), and a tape.
The tape is represented in the form `(a, L, R)`, meaning the tape looks like `L.rev ++ [a] ++ R`
with the machine currently reading the `a`. The lists are
automatically extended with blanks as the machine moves around.  -/
Turing.TM0.Cfg : (Γ : Type u_1) → Type u_2 → [Inhabited Γ] → Type (max u_1 u_2)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.comp_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} {f₁ g₁ : C₁ ⟶ C₂} {f₂ g₂ : C₂ ⟶ C₃} (h₁ : Homotopy f₁ g₁)
  (h₂ : Homotopy f₂ g₂) (i j : ι),
  (h₁.comp h₂).hom i j =
    CategoryTheory.CategoryStruct.comp (h₁.hom i j) (f₂.f j) + CategoryTheory.CategoryStruct.comp (g₁.f i) (h₂.hom i j)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero_assoc : ∀ {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1)
        h) =
    CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.δ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
        h)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The action of a pair of maps `f : c ⟶ c'` and `d ⟶ d'`. By default,
this is defined in terms of `actionHomLeft` and `actionHomRight`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom : {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.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            {c c' : C} →
              {d d' : D} →
                (d ⟶ d') →
                  (c ⟶ c') →
                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶
                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d' c')
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.instIsTotallyRealRat : NumberField.IsTotallyReal ℚ
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The invariant vector field associated to a vector `v` in the Lie algebra. At a
point `g`, it is given by the image of `v` under left-addition by `g`.  -/
addInvariantVectorField : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : AddGroup G] → AddGroupLieAlgebra I G → (g : G) → TangentSpace I g
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.mk.inj : ∀ {todo : Array Lean.Expr} {score : ℕ} {c : Lean.Meta.LazyDiscrTree.TrieIndex} {todo_1 : Array Lean.Expr} {score_1 : ℕ}
  {c_1 : Lean.Meta.LazyDiscrTree.TrieIndex},
  { todo := todo, score := score, c := c } = { todo := todo_1, score := score_1, c := c_1 } →
    todo = todo_1 ∧ score = score_1 ∧ c = c_1
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelOpOp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.cokernelOpOp f).hom = CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem: if for all open sets `G` we have the liminf
condition `μ(G) ≤ liminf μsₙ(G)`, then the measures `μsₙ` converge weakly to the measure `μ`.
Superseded by `tendsto_of_forall_isOpen_le_liminf` which works for all countably
generated filters.  -/
MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω},
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) →
    Filter.Tendsto (fun i => μs i) Filter.atTop (nhds μ)
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The second base case for the induction on `n`, giving an explicit formula for `I 1 θ`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I_one : ∀ {θ : ℝ}, I✝ 1 θ * θ ^ 3 = 4 * Real.sin θ - 4 * θ * Real.cos θ
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_mul_compl_eq_piecewise : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {s : Set α} [inst_1 : DecidablePred fun x => x ∈ s]
  (f g : α → M), s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g
-- Mathlib.Topology.Order.ExtendFrom
eq_lim_at_left_extendFrom_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {la : β} [T2Space β],
  a < b → Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la) → extendFrom (Set.Ioo a b) f a = la
-- Mathlib.CategoryTheory.Sites.Canonical
/-- A subcanonical topology is a topology which is smaller than the canonical topology.
Equivalently, a topology is subcanonical iff every representable is a sheaf.
 -/
CategoryTheory.GrothendieckTopology.Subcanonical : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {km : α}, t.max! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.add_def : ∀ {M : Type u_2} {X : Type u_4} [inst : VAdd M X] {f g : X →ₑ[id] X}, f + g = f.comp g
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn (fun x => Set.Iic (f x)) s
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopEquivalence_inverse : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.unopEquivalence V c).inverse = HomologicalComplex.unopInverse V c
-- Mathlib.CategoryTheory.UnivLE
UnivLE_iff_essSurj : UnivLE.{max u v, v} ↔ CategoryTheory.uliftFunctor.{u, v}.EssSurj