mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₁'.RespectsIso] [W₂'.RespectsIso] [L.IsInduced]
  [L.functor.IsEquivalence] [R.IsInduced] [R.functor.IsEquivalence] [T.IsRightDerivabilityStructure]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor), B.IsRightDerivabilityStructure
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.instNonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Nonempty X], Nonempty (ZerothHomotopy X)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit G f =
    CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit G f
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_eq_top_of_isEmpty : ∀ {α : Type u_1} {G : SimpleGraph α} [IsEmpty α], G.radius = ⊤
-- Init.Data.UInt.Lemmas
USize.toBitVec_inj : ∀ {a b : USize}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_8 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.ret k with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_8 k
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.symmL_trivialization : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (x : B),
  Bundle.Trivialization.symmL 𝕜 (Bundle.Trivial.trivialization B F) x = ContinuousLinearMap.id 𝕜 F
-- Lean.Meta.Basic
Lean.Meta.instBEqDefEqCacheKey : BEq Lean.Meta.DefEqCacheKey
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_eraseMin : ∀ {α : Type u_1} (t : Ordnode α), t.eraseMin.dual = t.dual.eraseMax
-- Mathlib.Data.List.Sort
/-- `l.SortedLE` means that the list is monotonic.  -/
List.SortedLE : {α : Type u_1} → [Preorder α] → List α → Prop
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- In the following results, we need a large set of distinct elements of `R`.  -/
ClassGroup.distinctElems : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} →
                [inst_4 : DecidableEq ι] →
                  [inst_5 : Fintype ι] →
                    (bS : Module.Basis ι R S) →
                      (adm : abv.IsAdmissible) → [Infinite R] → Fin (ClassGroup.cardM bS adm).succ ↪ R
-- Mathlib.Probability.BrownianMotion.Basic
/-- If `B` is a pre-Brownian motion then `t ↦ t * B (1 / t)` is a pre-Brownian motion.  -/
ProbabilityTheory.IsPreBrownianReal.inv : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ProbabilityTheory.IsPreBrownianReal (fun t ω => ↑t * B (1 / t) ω) P
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_sdiff_right : ∀ {α : Type u_1} {s t u : Set α}, t ⊆ u → s \ u ⊆ s \ t
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-closed right-open range as a list in ascending order.
 -/
Std.Rco.toList : {α : Type u} →
  [inst : LT α] →
    [DecidableLT α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Rco α → List α
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ext : ∀ {X Y : AddSemigrp} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Algebra.Group.Commute.Defs
/-- Any element commutes with itself.  -/
AddCommute.refl : ∀ {S : Type u_3} [inst : Add S] (a : S), AddCommute a a
-- Mathlib.Algebra.Order.Algebra
algebraMap_strictMono : ∀ {α : Type u_1} (β : Type u_2) [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [Nontrivial β] [SMulPosStrictMono α β],
  StrictMono ⇑(algebraMap α β)
-- Mathlib.RingTheory.IsTensorProduct
Algebra.pushoutDesc_right : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_12 : Semiring A] [inst_13 : Algebra R A] (f : S →ₐ[R] A)
  (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : R'),
  (Algebra.pushoutDesc S' f g H) ((algebraMap R' S') x) = g x
-- Init.Data.Array.Lemmas
Array.size_singleton : ∀ {α : Type u_1} {x : α}, #[x].size = 1
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The trivial bimonoid object.  -/
CategoryTheory.Bimon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Bimon C
-- Mathlib.Data.Set.Lattice
Set.iInter_and : ∀ {α : Type u_1} {p q : Prop} (s : p ∧ q → Set α), ⋂ (h : p ∧ q), s h = ⋂ (hp : p), ⋂ (hq : q), s ⋯
-- Mathlib.NumberTheory.LSeries.RiemannZeta
two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even : ∀ {k : ℕ}, 2 ≤ k → Even k → 2 * riemannZeta ↑k = ∑' (n : ℤ), (↑n ^ k)⁻¹
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.argsPacker : Lean.Elab.WF.EqnInfo → Lean.Meta.ArgsPacker
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMap_snd : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {X : TangentSpace I x}, (tangentMap I I' f ⟨x, X⟩).snd = (mfderiv% f x) X
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_xor_cancel_right : ∀ (x y : ℕ), x ^^^ y ^^^ y = x
-- Mathlib.NumberTheory.FunctionField
FunctionField.isAlgebraic_X_over_adjoin_transcendental : ∀ {F : Type u_3} {K : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (RatFunc F) K] [FunctionField F K]
  [inst_4 : Algebra F K] [IsScalarTower F (RatFunc F) K] {y : K},
  Transcendental F y → IsAlgebraic (↥F⟮y⟯) ((algebraMap (RatFunc F) K) RatFunc.X)
-- Mathlib.Data.Finmap
Finmap.keys_empty : ∀ {α : Type u} {β : α → Type v}, ∅.keys = ∅
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ofList_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.ofList [] cmp = ∅
-- Mathlib.Algebra.Order.SuccPred
Order.lt_add_one_iff : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  x < y + 1 ↔ x ≤ y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.step_uLift.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Algebra.Regular.Basic
/-- If `R` is a monoid, an element in `Rˣ` is regular.  -/
Units.isRegular : ∀ {R : Type u_1} [inst : Monoid R] (a : Rˣ), IsRegular ↑a
-- Init.Prelude
/-- Show that a byte array is valid UTF-8 by exhibiting it as `List.utf8Encode m` for some list `m`
of characters.
  -/
ByteArray.IsValidUTF8.intro : ∀ {b : ByteArray} (m : List Char), b = m.utf8Encode → b.IsValidUTF8
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true},
  Std.Internal.List.getKey a (Std.Internal.List.insertEntry k v l) h =
    if h' : (k == a) = true then k else Std.Internal.List.getKey a l ⋯
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.of_isPushout : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_4)
  (S' : Type u_5) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [Algebra.IsPushout R S R' S'] [Algebra.IsStandardOpenImmersion R S], Algebra.IsStandardOpenImmersion R' S'
-- Init.Data.Order.Ord
Fin.instTransOrd : ∀ (n : ℕ), Std.TransOrd (Fin n)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction : ∀ {κ : Type u_2} {Z : Type u_3} {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)}
  [inst : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)]
  {mZ : MeasurableSpace Z} [inst_3 : TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] [inst_6 : Fintype κ]
  {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure ((j : κ) → Y j)}
  {ξ : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ),
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ξ =
        (∫ (z : Z), f z ∂μ) * ∫ (y : (j : κ) → Y j), ∏ j, (g j) (y j) ∂ν) →
    ξ = μ.prod ν
-- Mathlib.ModelTheory.Fraisse
/-- The class of finite structures in the empty language is Fraïssé.  -/
FirstOrder.Language.empty.isFraisse_finite : FirstOrder.Language.IsFraisse {S | Finite ↑S}
-- Mathlib.Algebra.Ring.Prod
/-- The product of two nontrivial rings is not a domain  -/
false_of_nontrivial_of_product_domain : ∀ (R : Type u_6) (S : Type u_7) [inst : Semiring R] [inst_1 : Semiring S] [IsDomain (R × S)] [Nontrivial R]
  [Nontrivial S], False
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.u_csInf' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {s : Set β}, s.Nonempty → BddBelow s → u (sInf s) = sInf (u '' s)
-- Mathlib.RingTheory.Polynomial.Basic
/-- The push-forward of an ideal `I` of `R` to `MvPolynomial σ R` via inclusion
is exactly the set of polynomials whose coefficients are in `I`  -/
MvPolynomial.mem_map_C_iff : ∀ {R : Type u} {σ : Type v} [inst : CommRing R] {I : Ideal R} {f : MvPolynomial σ R},
  f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mk : {X : Type u_3} →
  [inst : MetricSpace X] →
    (carrier : Set X) →
      (packingRadius : NNReal) →
        0 < packingRadius →
          Metric.IsSeparated (↑packingRadius) carrier →
            (coveringRadius : NNReal) →
              0 < coveringRadius → Metric.IsCover coveringRadius Set.univ carrier → Delone.DeloneSet X
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The property that describes how `homEquiv` transforms compositions `F X ⟶ Y ⟶ Y'`  -/
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreHomEquiv F G)
  {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
  (self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The cokernel of `biproduct.ι f i` is the projection from the biproduct over the index set `J`
onto the biproduct omitting `i`.  -/
CategoryTheory.Limits.biproduct.isColimitToSubtype : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          (i : J) →
            [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] →
                CategoryTheory.Limits.IsColimit
                  (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun j => j ≠ i)
                    ⋯)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.setTag.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (cidx : ℕ) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13),
  sizeOf (Lean.Compiler.LCNF.Code.setTag fvarId cidx k h) = 1 + sizeOf fvarId + sizeOf cidx + sizeOf k + sizeOf h
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.brecOn : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α]
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv1 a a_1 → Prop} {a : ℕ}
  {a_1 : Std.HashMap α ℕ} (t : Std.Sat.AIG.RelabelNat.State.Inv1 a a_1),
  (∀ (a : ℕ) (a_2 : Std.HashMap α ℕ) (t : Std.Sat.AIG.RelabelNat.State.Inv1 a a_2),
      Std.Sat.AIG.RelabelNat.State.Inv1.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_obj₂ : ∀ {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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).obj₂ = Z₁₃
-- Lean.Meta.Match.Match
Lean.Meta.Match.State.mk : Std.HashSet ℕ → Lean.Meta.Match.Overlaps → Array (List Lean.Meta.Match.Example) → Lean.Meta.Match.State
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `i` is an equivalence.  -/
CategoryTheory.instIsEquivalenceShiftFunctor : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i : A), (CategoryTheory.shiftFunctor C i).IsEquivalence
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.eq_2 : ∀ (C : Type u_1) (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of x => h_1 x
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Term.realize_mem : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {α : Type u_3} (t : L.Term α)
  (xs : α → M), (∀ (a : α), xs a ∈ S) → FirstOrder.Language.Term.realize xs t ∈ S
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.mulHeight₁ x =
    (Multiset.map (fun v => max (v x) 1) Height.AdmissibleAbsValues.archAbsVal).prod *
      ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), max (↑v x) 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.instFaithfulFunctorTensoringRight : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalCategory.tensoringRight C).Faithful
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.SeparatesPoints.mk : ∀ {α : Type u_3} [m : MeasurableSpace α],
  (∀ (x y : α), (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y) → MeasurableSpace.SeparatesPoints α
-- Init.Data.List.Pairwise
List.pairwise_append_comm : ∀ {α : Type u_1} {R : α → α → Prop},
  (∀ {x y : α}, R x y → R y x) → ∀ {l₁ l₂ : List α}, List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R (l₂ ++ l₁)
-- Mathlib.Data.Matrix.Mul
Matrix.smul_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Mul α] [inst_1 : SMul R α] [IsScalarTower R α α]
  (r : R) (w : m → α) (v : n → α), Matrix.vecMulVec (r • w) v = r • Matrix.vecMulVec w v
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instInvSubtypeMemAddSubgroup : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → Inv ↥(selfAdjoint R)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Ioo_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.Ioo ↑i ↑j = Set.Ioo i j
-- Mathlib.RepresentationTheory.Coinduced
Representation.coind'_apply_apply : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{max u w, u, v} k G) (h : H) (f : Rep.res φ (Rep.leftRegular k H) ⟶ A),
  ((Representation.coind' φ A) h) f =
    CategoryTheory.CategoryStruct.comp
      ((Rep.resFunctor φ).map (↑(Rep.leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single h 1))) f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t → symmDiff s t = s ∪ t
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.instIteratorLoop : {m : Type w → Type w'} →
  {α : Type w} →
    [inst : Monad m] → {n : Type x → Type x'} → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.ArrayIterator α) m n
-- Mathlib.Logic.Basic
or_not_of_imp : ∀ {a b : Prop}, (a → b) → b ∨ ¬a
-- Init.Data.UInt.Lemmas
UInt8.neg_eq_neg_one_mul : ∀ (a : UInt8), -a = -1 * a
-- Mathlib.NumberTheory.AlmostPrime
/-- A semiprime is a `2`-almost-prime number.  -/
Nat.IsSemiprime : ℕ → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_left_zero : ∀ {α : Type u_2} [inst : AddGroup α] {a : α}, (fun x => a + x) ⁻¹' 0 = {-a}
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- The canonical map from the quotient of the stabilizer to the set.  -/
AddAction.ofQuotientStabilizer : (G : Type u) →
  {X : Type v} → [inst : AddGroup G] → [inst_1 : AddAction G X] → (x : X) → G ⧸ AddAction.stabilizer G x → X
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
/-- If `C` has strict initial objects and `X` is an initial object, the category
`P.Over Q X` is equivalent to a point.  -/
CategoryTheory.MorphismProperty.overEquivOfIsInitial : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P Q : CategoryTheory.MorphismProperty C) →
      [P.ContainsIdentities] →
        [inst_2 : Q.IsMultiplicative] →
          [Q.RespectsIso] →
            [CategoryTheory.Limits.HasStrictInitialObjects C] →
              (X : C) → CategoryTheory.Limits.IsInitial X → (P.Over Q X ≌ CategoryTheory.Discrete PUnit.{w + 1})
-- Init.Data.Vector.Count
Vector.countP_set : ∀ {α : Type u_1} {n i : ℕ} {p : α → Bool} {xs : Vector α n} {a : α} (h : i < n),
  Vector.countP p (xs.set i a h) = (Vector.countP p xs - if p xs[i] = true then 1 else 0) + if p a = true then 1 else 0
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  LieSubmodule.restr I H = ⨆ α ∈ I.rootSet, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Mathlib.Topology.NhdsWithin
eventually_nhdsWithin_of_eventually_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop},
  (∀ᶠ (x : α) in nhds a, p x) → ∀ᶠ (x : α) in nhdsWithin a s, p x