mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelIso.Basic
RelIso.relIsoCongr_symm_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ≃r s₂),
  (e₁.relIsoCongr e₂).symm f₂ = (e₁.trans f₂).trans e₂.symm
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.preimageIso.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : Y.Opens),
  AlgebraicGeometry.Scheme.Hom.preimageIso f U = AlgebraicGeometry.Scheme.Hom.preimageIso f U
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_threeMore_iff : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.threeMore ↔ b &&& 248 = 240
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.continuousOn_termTSum : ContinuousOn ZetaAsymptotics.termTSum (Set.Ici 1)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsLimit.isZero_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C}
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Limits.IsZero F → CategoryTheory.Limits.IsZero c.pt
-- Mathlib.Topology.Order
coinduced_le_iff_le_induced : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {tα : TopologicalSpace α} {tβ : TopologicalSpace β},
  TopologicalSpace.coinduced f tα ≤ tβ ↔ tα ≤ TopologicalSpace.induced f tβ
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instSMulIntSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → SMul ℤ ↥I
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_eq_zero_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α), G.eccent u = 0 ↔ Subsingleton α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `Bimon.mk'`.  -/
CategoryTheory.Bimon.mk'X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (X : C) → [CategoryTheory.BimonObj X] → CategoryTheory.Mon C
-- Mathlib.Logic.Equiv.Option
/-- Any type with a distinguished element is equivalent to an `Option` type on the subtype excluding
that element.  -/
Equiv.optionSubtypeNe : {α : Type u_1} → [DecidableEq α] → (a : α) → Option { b // b ≠ a } ≃ α
-- Mathlib.Data.Nat.Choose.Lucas
/-- For a prime power `n`, the minimal prime factor divides the greatest common divisor of
`choose n 1, ⋯, choose n (n - 1)`.  -/
Choose.minFac_dvd_gcd_choose_of_isPrimePow : ∀ {n : ℕ}, IsPrimePow n → n.minFac ∣ (Finset.Icc 1 (n - 1)).gcd n.choose
-- Mathlib.Order.Category.PartOrdEmb
_private.Mathlib.Order.Category.PartOrdEmb.0.PartOrdEmb.Hom.mk.inj : ∀ {X Y : PartOrdEmb} {hom' hom'_1 : ↑X ↪o ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instNeg : {α : ℚ} → Neg (Std.Time.Internal.UnitVal α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α},
  k ∉ m₂ → Std.ExtDHashMap.Const.get? (m₁.union m₂) k = Std.ExtDHashMap.Const.get? m₁ k
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Suppose we have a cofiltered diagram of schemes whose transition maps are affine. The limit of
a family of compatible nonempty quasicompact closed sets in the diagram is also nonempty.
 -/
AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] (Z : (i : I) → Set ↥(D.obj i)),
  (∀ (i : I), IsClosed (Z i)) →
    (∀ (i : I), (Z i).Nonempty) →
      (∀ (i : I), IsCompact (Z i)) →
        (∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')) → ∃ s, ∀ (i : I), (c.π.app i) s ∈ Z i
-- Init.System.IO
/-- Writes the provided string to the file handle using the UTF-8 encoding.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use
`IO.FS.Handle.flush` to write changes to buffers to the associated device.
 -/
IO.FS.Handle.putStr : IO.FS.Handle → String → IO Unit
-- Mathlib.Order.Filter.Cofinite
Filter.disjoint_cofinite_left : ∀ {α : Type u_2} {l : Filter α}, Disjoint Filter.cofinite l ↔ ∃ s ∈ l, s.Finite
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instInhabited : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Inhabited (CuspForm Γ k)
-- Init.Data.Vector.Lemmas
Vector.take_size : ∀ {α : Type u_1} {n : ℕ} {as : Vector α n}, as.take n = Vector.cast ⋯ as
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.mk.sizeOf_spec : ∀ (perm : Mathlib.Tactic.Translate.Permutation) (argReorders : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)),
  sizeOf { perm := perm, argReorders := argReorders } = 1 + sizeOf perm + sizeOf argReorders
-- Mathlib.Data.Nat.Factorial.Basic
Nat.dvd_factorial : ∀ {m n : ℕ}, 0 < m → m ≤ n → m ∣ n.factorial
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- State for each `CommRing` processed by this module.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing : Type
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitIso_inv_hom_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D) {Z : D} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = h
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_dvd_iff : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} {φ : PowerSeries R},
  PowerSeries.X ^ n ∣ φ ↔ ∀ m < n, (PowerSeries.coeff m) φ = 0
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.mulLeft₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0), ⇑(Equiv.mulLeft₀ a ha) = fun x => a * x
-- Std.Http.Server.Handler
Std.Http.Server.StatelessHandler.mk.sizeOf_spec : ∀ (onRequest : Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
  (onFailure : IO.Error → Std.Async.Async Unit) (onContinue : Std.Http.Request.Head → Std.Async.Async Bool),
  sizeOf { onRequest := onRequest, onFailure := onFailure, onContinue := onContinue } = 1
-- Lean.Data.Options
Lean.Options.instForInProdNameDataValueOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.Options (Lean.Name × Lean.DataValue)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The range of `circleMap c R` is the circle with center `c` and radius `|R|`.  -/
range_circleMap : ∀ (c : ℂ) (R : ℝ), Set.range (circleMap c R) = Metric.sphere c |R|
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_const : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} {b : β},
  b ∈ B → IsMulFreimanHom n A B fun x => b
-- Std.Http.Data.Response
/-- Optional dynamic metadata attached to the response.
 -/
Std.Http.Response.Builder.extensions : Std.Http.Response.Builder → Std.Http.Extensions
-- Std.Data.ExtDHashMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.ExtDHashMap.insertIfNew : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → (a : α) → β a → Std.ExtDHashMap α β
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.compl_coindep : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.Spanning S → M.Coindep (M.E \ S)
-- Mathlib.Data.ENNReal.Basic
/-- Notation for infinity as an `ENNReal` number.  -/
ENNReal.«term∞» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Ray
SameRay.rfl : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x : M}, SameRay R x x
-- Mathlib.Data.Int.Log
Int.log_one_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ), Int.log b 1 = 0
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.elabReduceConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.Command.ReduceConfig
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.liftedLimitMapsToOriginal_hom_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [inst_3 : CategoryTheory.CreatesLimit K F]
  {c : CategoryTheory.Limits.Cone (K.comp F)} (t : CategoryTheory.Limits.IsLimit c) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.liftedLimitMapsToOriginal t).hom.hom (c.π.app j) =
    F.map ((CategoryTheory.liftLimit t).π.app j)
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A linear equivalence between topological modules is a homeomorphism if and only if it is
continuous in both directions.  -/
LinearEquiv.isHomeomorph_iff : ∀ {S : Type u_1} [inst : Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [inst_1 : Semiring S₁]
  {σ : S →+* S₁} {σ' : S₁ →+* S} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module S M] [inst_7 : TopologicalSpace M₁]
  [inst_8 : AddCommMonoid M₁] [inst_9 : Module S₁ M₁] (e : M ≃ₛₗ[σ] M₁),
  IsHomeomorph ⇑e ↔ Continuous ⇑e ∧ Continuous ⇑e.symm
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.InfoCacheKey.mk.inj : ∀ {configKey : UInt64} {expr : Lean.Expr} {nargs? : Option ℕ} {configKey_1 : UInt64} {expr_1 : Lean.Expr}
  {nargs?_1 : Option ℕ},
  { configKey := configKey, expr := expr, nargs? := nargs? } =
      { configKey := configKey_1, expr := expr_1, nargs? := nargs?_1 } →
    configKey = configKey_1 ∧ expr = expr_1 ∧ nargs? = nargs?_1
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_inj : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f g : Polynomial R}, (Polynomial.expand R p) f = (Polynomial.expand R p) g ↔ f = g
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sigma_arrow : ∀ {ι : Type u_3} (α : Type u_1) (f : ι → Type u_2), Cardinal.mk (Sigma f → α) = Cardinal.mk ((i : ι) → f i → α)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- An `ExteriorAlgebra` over a nontrivial ring is nontrivial.  -/
ExteriorAlgebra.instNontrivial : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R],
  Nontrivial (ExteriorAlgebra R M)
-- Mathlib.Algebra.CharP.Lemmas
/-- The characteristic of a finite ring cannot be zero.  -/
CharP.char_ne_zero_of_finite : ∀ (R : Type u_1) [inst : NonAssocRing R] (p : ℕ) [CharP R p] [Finite R], p ≠ 0
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivCLM_smul : ∀ {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] {n k : ℕ∞}
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {c : ℝ} {v : E},
  Distribution.lineDerivCLM (c • v) = c • Distribution.lineDerivCLM v
-- Mathlib.GroupTheory.OrderOfElement
pow_card_eq_one' : ∀ {G : Type u_6} [inst : Group G] {x : G}, x ^ Nat.card G = 1
-- Init.Data.UInt.Lemmas
UInt8.toFin_mul : ∀ (a b : UInt8), (a * b).toFin = a.toFin * b.toFin
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.epi_iff_surjective : ∀ {X Y : Profinite} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.ENNReal.Action
ENNReal.nnreal_smul_ne_top : ∀ {x : NNReal} {y : ENNReal}, y ≠ ⊤ → x • y ≠ ⊤
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fromProd_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  ((CategoryTheory.Comma.fromProd L R).obj X).hom = CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_tendsto_atTop : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜], 0 < P.degree → Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atTop Filter.atTop
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instCoeHeadValuesList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → CoeHead (RBTree.RBMap.Values α β cmp) (List β)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
rootsOfUnity.integer_power_of_ringEquiv' : ∀ {L : Type u} [inst : CommRing L] [IsDomain L] (n : ℕ) [NeZero n] (g : L ≃+* L),
  ∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertManyIfNewUnit_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit},
  m.WF → ∀ {l : List α} {k : α}, m.insertManyIfNewUnit (k :: l) = (m.insertIfNew k ()).insertManyIfNewUnit l
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_inv_comp_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).inv
      ((CategoryTheory.Limits.pullback.fst f g).app d) =
    CategoryTheory.Limits.pullback.fst (f.app d) (g.app d)
-- Mathlib.Algebra.Star.Rat
Rat.instTrivialStar : TrivialStar ℚ
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) '' Set.Ioo b c = Set.Ioo (b / a) (c / a)
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Data.List.Forall2
List.Forall₂.mp : ∀ {α : Type u_1} {β : Type u_2} {R S Q : α → β → Prop},
  (∀ (a : α) (b : β), Q a b → R a b → S a b) →
    ∀ {l₁ : List α} {l₂ : List β}, List.Forall₂ Q l₁ l₂ → List.Forall₂ R l₁ l₂ → List.Forall₂ S l₁ l₂
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_sub_le_iff_right : ∀ {R : Type u} {n : ℕ} [inst : Ring R] {p q : Polynomial R}, p.natDegree ≤ n → ((p - q).natDegree ≤ n ↔ q.natDegree ≤ n)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.mem_countablyGeneratedAtom_natGeneratingSequence : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α] (x : α),
  x ∈ MeasurableSpace.countablyGeneratedAtom α fun x_1 => x ∈ MeasurableSpace.natGeneratingSequence α x_1
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.mk : {α : Type u} → α → Std.Roi α
-- Init.Data.SInt.Lemmas
Int16.toBitVec_toInt64 : ∀ (x : Int16), x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₂ : ∀ {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'.triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₂ = u₁₂
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.CreatesLimitsOfShape J FintypeCat.incl
-- Mathlib.NumberTheory.BernoulliPolynomials
/-- Rearrangement of `Polynomial.sum_range_pow_eq_bernoulli_sub`.  -/
Polynomial.bernoulli_succ_eval : ∀ (n p : ℕ),
  Polynomial.eval (↑n) (Polynomial.bernoulli p.succ) = bernoulli p.succ + (↑p + 1) * ∑ k ∈ Finset.range n, ↑k ^ p
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_trans : ∀ {a b c : ℕ} (hab : a = b) (hbc : b = c),
  (ZMod.ringEquivCongr hab).trans (ZMod.ringEquivCongr hbc) = ZMod.ringEquivCongr ⋯
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Pull back the normed ring structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
algebra homomorphism `Unitization.splitMul 𝕜 A`. This does not give us the desired topology,
uniformity or bornology on `Unitization 𝕜 A` (which we want to agree with `Prod`), so we only use
it as a local instance to build the real one.  -/
Unitization.normedRingAux : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] → [RegularNormedAlgebra 𝕜 A] → NormedRing (Unitization 𝕜 A)
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.adjoin_of_finite : ∀ {R : Type uR} [inst : CommSemiring R] {A : Type u_1} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {t : Set A},
  t.Finite → Algebra.FiniteType R ↥(Algebra.adjoin R t)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂) (x : A ⟶ S.X₁)
  (hx : k = CategoryTheory.CategoryStruct.comp x S.f) {Z : C} (h_1 : h.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.liftK k ⋯) (CategoryTheory.CategoryStruct.comp h.π h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Init.Data.Vector.Lemmas
Vector.map_setIfInBounds : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} {a : α},
  Vector.map f (xs.setIfInBounds i a) = (Vector.map f xs).setIfInBounds i (f a)
-- Mathlib.Data.Finsupp.Multiset
/-- `Finsupp.toMultiset` as an order isomorphism.  -/
Finsupp.orderIsoMultiset : {ι : Type u_3} → [DecidableEq ι] → (ι →₀ ℕ) ≃o Multiset ι
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The morphism `K.truncGE n ⟶ L.truncGE n` induced by a morphism `K ⟶ L`.  -/
CochainComplex.truncGEMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K L : CochainComplex C ℤ} →
        (K ⟶ L) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
              [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i] → (n : ℤ) → K.truncGE n ⟶ L.truncGE n
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `P : ObjectProperty C` is separating if the functors `C(G, -)`
for `G : C` such that `P G` are collectively faithful,
i.e., if `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`.  -/
CategoryTheory.ObjectProperty.IsSeparating : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.filterMap f m) k =
    (Std.DHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right,
excluding the subtraction of that point from itself.  -/
vectorSpan_eq_span_vsub_finset_right_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] [inst_5 : DecidableEq V] {s : Finset P} {p : P},
  p ∈ s → vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (s.erase p))
-- Lean.Elab.DeclModifiers
/-- Short name for recursively referring to the declaration.  -/
Lean.Elab.ExpandDeclIdResult.shortName : Lean.Elab.ExpandDeclIdResult → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.comp_id : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv (f.comp (CategoryTheory.FreeMonoidalCategory.Hom.id Y)) f
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.diagonalStrongDualPi_apply : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ} (x y : StrongDual ℝ ((i : ι) → E i)),
  ((ContinuousLinearMap.diagonalStrongDualPi✝ L) x) y =
    ∑ i, ((L i) (x ∘SL ContinuousLinearMap.single ℝ E i)) (y ∘SL ContinuousLinearMap.single ℝ E i)
-- Lean.Parser.Command
Lean.Parser.Command.computedFields : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_comap_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N),
  Subgroup.map f (Subgroup.comap f H) = f.range ⊓ H
-- Mathlib.Algebra.Group.Basic
zpow_mul : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m n : ℤ), a ^ (m * n) = (a ^ m) ^ n
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.exp_apply : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieAlgebra ℚ L] (D : LieDerivation R L L) (h : IsNilpotent ↑D),
  ↑(D.exp h).toLinearEquiv = IsNilpotent.exp ↑D
-- Aesop.Options.Public
/-- Use `simp_all`, rather than `simp at *`, for the builtin `simp` normalisation
rule.
 -/
Aesop.Options.useSimpAll : Aesop.Options → Bool
-- Init.Data.List.Lemmas
List.getElem?_cons : ∀ {α : Type u_1} {a : α} {l : List α} {i : ℕ}, (a :: l)[i]? = if i = 0 then some a else l[i - 1]?
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_natCast : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, Polynomial.derivative ↑n = 0