mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Topology.Compactness.Compact
IsCompact.insert : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → ∀ (a : X), IsCompact (insert a s)
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyEq.cardinal_iInter : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α},
  Cardinal.mk ι < c → (∀ (i : ι), s i =ᶠ[l] t i) → ⋂ i, s i =ᶠ[l] ⋂ i, t i
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.isUnit_den_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K], IsUnit ↑(IsFractionRing.den A 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.functor_map : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] {f g : α → C} (t : f ⟶ g),
  (CategoryTheory.Limits.Pi.functor α).map t = CategoryTheory.Limits.Pi.map t
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_add_left : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Add M] [IsIsometricVAdd M M] (a b c : M),
  dist (a + b) (a + c) = dist b c
-- Mathlib.RingTheory.Binomial
Ring.choose_neg : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ),
  Ring.choose (-r) n = (↑n).negOnePow • Ring.choose (r + ↑n - 1) n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_inj : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂}, ↑f = ↑g ↔ f = g
-- Mathlib.Order.Preorder.Chain
Flag.instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq : {α : Type u_1} →
  [inst : PartialOrder α] → [DecidableLE α] → [DecidableLT α] → [DecidableEq α] → (s : Flag α) → LinearOrder ↥s
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, Filter.map₂ (fun x1 x2 => x1 -ᵥ x2) f g = f -ᵥ g
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned_of_has_neither : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  ¬assignment.hasPosAssignment = true →
    ¬assignment.hasNegAssignment = true → assignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `y` returned by `lowerBound? x` is less or equal to `x`.  -/
RBTree.RBSet.lowerBound?_le : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp},
  t.lowerBound? x = some y → cmp x y ≠ Ordering.lt
-- Mathlib.Analysis.Convex.Strict
StrictConvex.eq_of_openSegment_subset_frontier : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x y : E} [IsOrderedRing 𝕜] [Nontrivial 𝕜]
  [DenselyOrdered 𝕜], StrictConvex 𝕜 s → x ∈ s → y ∈ s → openSegment 𝕜 x y ⊆ frontier s → x = y
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.norm_eq_one_iff_ne_zero_of_discrete : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜}, ‖x‖ = 1 ↔ x ≠ 0
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_iff_tmod_eq_zero : ∀ {a b : ℤ}, a ∣ b ↔ b.tmod a = 0
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_pair_lcm_eq.f.eq_1 : ∀ {n : ℕ} (a : Fin 3 → ℕ) (x : a ∈ Nat.finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f✝ a x = (a 0 * a 1, a 0 * a 2)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
_private.Mathlib.NumberTheory.NumberField.Completion.FinitePlace.0.NumberField.HeightOneSpectrum.termLw : Lean.ParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.coprodCon.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.coprodCon M N =
    sInf
      {c |
        (∀ (x y : M), c (FreeMonoid.of (Sum.inl (x * y))) (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) ∧
          (∀ (x y : N), c (FreeMonoid.of (Sum.inr (x * y))) (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) ∧
            c (FreeMonoid.of (Sum.inl 1)) 1 ∧ c (FreeMonoid.of (Sum.inr 1)) 1}
-- Mathlib.Data.Num.Bitwise
NzsNum.brecOn.go : {motive : NzsNum → Sort u} → (t : NzsNum) → ((t : NzsNum) → NzsNum.below t → motive t) → motive t ×' NzsNum.below t
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.comp_aemeasurable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {α' : Type u_8} [inst_2 : MeasurableSpace α'] {f : α → α'} {g : α' → ε},
  MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → MeasureTheory.Integrable (g ∘ f) μ
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to `R`, for `R` a smooth ring, as a sheaf of
rings.  -/
smoothSheafRing : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : Ring R] →
                                          [ContMDiffRing I (↑⊤) R] → TopCat.Sheaf RingCat (TopCat.of M)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, a point in the family is not
in the affine span of the other points, if the underlying ring is
nontrivial.  -/
AffineIndependent.notMem_affineSpan_sdiff : ∀ {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] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p → ∀ (i : ι) (s : Set ι), p i ∉ affineSpan k (p '' (s \ {i}))
-- Mathlib.Data.Fin.Tuple.Basic
Fin.comp_tail : ∀ {n : ℕ} {α : Sort u_1} {β : Sort u_2} (g : α → β) (q : Fin n.succ → α), g ∘ Fin.tail q = Fin.tail (g ∘ q)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_2.go : {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} →
  {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u} →
    {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} →
      {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u} →
        {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} →
          (t : Option (Array Lean.Lsp.DocumentSymbol)) →
            ((t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t) →
              ((t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
                  Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t) →
                ((t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t) →
                  ((t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t) →
                    ((t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t) →
                      motive_3 t ×' Lean.Lsp.DocumentSymbol.below_2 t
-- Mathlib.Analysis.Normed.Algebra.Exponential
Function.update_exp : ∀ {ι : Type u_3} {𝔸 : ι → Type u_4} [Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → NormedRing (𝔸 i)]
  [(i : ι) → NormedAlgebra ℚ (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (j : ι) (xj : 𝔸 j),
  Function.update (NormedSpace.exp x) j (NormedSpace.exp xj) = NormedSpace.exp (Function.update x j xj)
-- Mathlib.RingTheory.Finiteness.Cardinality
Set.Finite.submoduleSpan : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite R]
  {s : Set M}, s.Finite → (↑(Submodule.span R s)).Finite
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.coe_sup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M), ↑(p ⊔ p') = ↑p + ↑p'
-- Mathlib.Logic.IsEmpty.Defs
Empty.instIsEmpty : IsEmpty Empty
-- Mathlib.Analysis.Matrix.LDL
LDL.diag.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.diag hS = Matrix.diagonal (LDL.diagEntries hS)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffEquiv_apply : ∀ (R : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (self : PolynomialModule R M), (PolynomialModule.coeffEquiv R) self = self.coeff
-- Mathlib.Topology.LocallyFinsupp
/-- On a T1 space, the support of a function with locally finite support within `U` is discrete within
`U`.
 -/
Function.locallyFinsuppWithin.eq_zero_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] [T1Space X]
  (D : Function.locallyFinsuppWithin U Y), ⇑D =ᶠ[Filter.codiscreteWithin U] 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in both endpoints.

If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a` and `b`, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` in the sense of
strict differentiability.  -/
intervalIntegral.integral_hasStrictFDerivAt : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        ContinuousAt f a →
          ContinuousAt f b →
            HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
              ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (a, b)
-- Mathlib.Computability.DFA
DFA.eval_reindex : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ') (x : List α),
  ((DFA.reindex g) M).eval x = g (M.eval x)
-- Mathlib.Topology.Algebra.ProperAction.Basic
QuotientAddGroup.instT2Space : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {H : AddSubgroup G}
  [IsClosed ↑H], T2Space (G ⧸ H)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.iUnion.congr_simp : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f f_1 : α → ZFSet.{u}), f = f_1 → ZFSet.iUnion f = ZFSet.iUnion f_1
-- Mathlib.Analysis.Calculus.Deriv.Inv
fderiv_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜},
  fderiv 𝕜 (fun x => x⁻¹) x = ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.toNorm : {E : Type u_8} → [self : SeminormedAddCommGroup E] → Norm E
-- Lean.ExtraModUses
/-- Lets `shake` know that references to `declName` may also require importing the current module due to
some additional metaprogramming dependency expressed by `kind`. Currently this is always the name of
an attribute applied to `declName`, which is not from the current module, in the current module.
`kind` is not currently used to further filter what references to `declName` require importing the
current module but may in the future.
 -/
Lean.recordIndirectModUse : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadTrace m] →
        [Lean.MonadOptions m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → String → Lean.Name → m Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zpow_lt_of_lt_log : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.mk : {m : Type → Type} → Array Bool → (Array Bool → m Bool) → ℕ → Lean.Util.ParamMinimizer.Context✝ m
-- Mathlib.Data.ENNReal.Basic
ENNReal.le_of_forall_pos_le_add : ∀ {a b : ENNReal}, (∀ (ε : NNReal), 0 < ε → b < ⊤ → a ≤ b + ↑ε) → a ≤ b
-- Mathlib.Topology.Constructible
IsRetrocompact.finsetSup' : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {s : Finset ι} {hs : s.Nonempty} {t : ι → Set X},
  (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup' hs t)
-- Mathlib.Data.String.Defs
/-- Determine if a unicode character is part of the ASCII subset.

ASCII characters have code points in the range U+0000-U+007F.
(Note: [the Unicode standard](https://www.unicode.org/Public/draft/charts/CodeCharts.pdf)) does
not mention ASCII and instead calls this subset "C0 Controls and Basic Latin".)
 -/
Char.isAscii : Char → Bool
-- Mathlib.Data.List.Range
_private.Mathlib.Data.List.Range.0.List.ranges.match_1.splitter : (motive : List ℕ → Sort u_1) → (x : List ℕ) → (Unit → motive []) → ((a : ℕ) → (l : List ℕ) → motive (a :: l)) → motive x
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.Iter.step_uLift.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Lean.Meta.CoeAttr
Lean.Meta.instInhabitedCoeFnType.default : Lean.Meta.CoeFnType
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.mk.inj : ∀ {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₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {m₁ : Z₁₂ ⟶ Z₁₃} {m₃ : Z₁₃ ⟶ Z₂₃}
  {comm₁ : CategoryTheory.CategoryStruct.comp v₁₂ m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃}
  {comm₂ : CategoryTheory.CategoryStruct.comp m₁ w₁₃ = w₁₂} {comm₃ : CategoryTheory.CategoryStruct.comp v₁₃ m₃ = v₂₃}
  {comm₄ :
    CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
      CategoryTheory.CategoryStruct.comp m₃ w₂₃}
  {mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles}
  {m₁_1 : Z₁₂ ⟶ Z₁₃} {m₃_1 : Z₁₃ ⟶ Z₂₃}
  {comm₁_1 : CategoryTheory.CategoryStruct.comp v₁₂ m₁_1 = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃}
  {comm₂_1 : CategoryTheory.CategoryStruct.comp m₁_1 w₁₃ = w₁₂}
  {comm₃_1 : CategoryTheory.CategoryStruct.comp v₁₃ m₃_1 = v₂₃}
  {comm₄_1 :
    CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
      CategoryTheory.CategoryStruct.comp m₃_1 w₂₃}
  {mem_1 :
    CategoryTheory.Pretriangulated.Triangle.mk m₁_1 m₃_1
        (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles},
  { m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
      { m₁ := m₁_1, m₃ := m₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1, comm₄ := comm₄_1, mem := mem_1 } →
    m₁ = m₁_1 ∧ m₃ = m₃_1
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_orElse_OptionT_apply : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (x : OptionT m α) (h : Unit → OptionT m α),
  Lean.Order.PartialOrder.rel
    (Std.Internal.Do.wp x post (EPost.Cons.mk✝ (Std.Internal.Do.wp (h ()) post epost) epost.tail))
    (Std.Internal.Do.wp (OrElse.orElse x h) post epost)
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.forget_obj`. -/
SemiRingCat.forget_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (X : C), (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : Field R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] (x : V → R),
  (((Matrix.toLinearMap₂' R) (SimpleGraph.lapMatrix R G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
-- Mathlib.Algebra.Homology.CommSq
/-- The limit kernel fork attached to a pullback square.  -/
CategoryTheory.IsPullback.isLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {fst : X₁ ⟶ X₂} →
            {snd : X₁ ⟶ X₃} →
              {f : X₂ ⟶ X₄} →
                {g : X₃ ⟶ X₄} → (h : CategoryTheory.IsPullback fst snd f g) → CategoryTheory.Limits.IsLimit ⋯.kernelFork
-- Init.Data.Array.Zip
Array.zipWith_replicate : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {m n : ℕ},
  Array.zipWith f (Array.replicate m a) (Array.replicate n b) = Array.replicate (min m n) (f a b)
-- ProofWidgets.Presentation.Expr
/-- A user-friendly name for this presenter. For example, "LaTeX".  -/
ProofWidgets.ExprPresenter.userName : ProofWidgets.ExprPresenter → String
-- Batteries.Data.Fin.Coding
Fin.encodePi.eq_def : ∀ {n : ℕ} (f : Fin n → ℕ) (x : (i : Fin n) → Fin (f i)),
  Fin.encodePi f x =
    match n, f, x with
    | 0, x, x_1 => ⟨0, ⋯⟩
    | n.succ, f, x =>
      match
        Fin.encodePi (fun x => f x.succ) fun x_1 =>
          match x_1 with
          | ⟨i, hi⟩ => x ⟨i + 1, ⋯⟩ with
      | ⟨k, hk⟩ => ⟨f 0 * k + ↑(x 0), ⋯⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.forM_eq_forM_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.HashMap.forM f m = Array.forM (fun a => f a.1 a.2) m.toArray
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.normedGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : SubgroupClass S E] (s : S),
  SubgroupClass.normedGroup s =
    { toNorm := (SubgroupClass.seminormedGroup s).toNorm, toGroup := SubgroupClass.toGroup s,
      toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_ext : ∀ {X Y : AddCommGrpCat} {f g : X ⟶ Y}, AddCommGrpCat.Hom.hom f = AddCommGrpCat.Hom.hom g → f = g
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toFun_eq_coe : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  (↑v.toMonoidWithZeroHom).toFun = ⇑v
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.intermediateFieldMap_symm_apply_coe : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L)
  (a : ↥(IntermediateField.map (↑e) E)), ↑((IntermediateField.intermediateFieldMap e E).symm a) = e.symm ↑a
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.infsep_of_fintype : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : Fintype ↑s] (hs : s.Nontrivial),
  s.infsep = s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist)
-- Lean.Parser.Term
Lean.Parser.Term.letRecDecls.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) (x x_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) x x_1 =
    CategoryTheory.MonObj.mul
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.isCoprime : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, (f * g).Separable → IsCoprime f g
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.fun_sum : ∀ {𝕜 : 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]
  {L : Filter (E × E)} {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L) → HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (n : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17) (n_1 : ℕ)
  (var_1 : Lean.FVarId) (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17),
  (Lean.Compiler.LCNF.LetValue.reset n var h = Lean.Compiler.LCNF.LetValue.reset n_1 var_1 h_1) =
    (n = n_1 ∧ var = var_1)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
FiberBundleCore.localTriv.eq_1 : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι),
  Z.localTriv i =
    { toPartialEquiv := Z.localTrivAsPartialEquiv i, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯,
      open_source := ⋯, open_target := ⋯, baseSet := Z.baseSet i, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯,
      proj_toFun := ⋯ }
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.pos : Lean.ParseImports.State → String.Pos.Raw
-- Lean.Parser.Term
Lean.Parser.Term.panic.formatter : Lean.PrettyPrinter.Formatter