mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKey! k' = k
-- Mathlib.Order.Defs.LinearOrder
Ordering.Compares.eq_1 : ∀ {α : Type u_1} [inst : LT α] (x x_1 : α), Ordering.lt.Compares x x_1 = (x < x_1)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.comulAlgHom_apply : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a : A),
  (Bialgebra.comulAlgHom R A) a = CoalgebraStruct.comul a
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  (∀ (x : ℝ), Measurable fun p => ↑(f p) x) →
    (∀ (a : α) (x : ℝ), MeasureTheory.Integrable (fun b => ↑(f (a, b)) x) (ν a)) →
      (∀ (p : α × β), Filter.Tendsto (↑(f p)) Filter.atTop (nhds 1)) →
        (∀ (p : α × β), Filter.Tendsto (↑(f p)) Filter.atBot (nhds 0)) →
          (∀ (a : α) {s : Set β},
              MeasurableSet s → ∀ (x : ℝ), ∫ (b : β) in s, ↑(f (a, b)) x ∂ν a = (κ a).real (s ×ˢ Set.Iic x)) →
            ProbabilityTheory.IsCondKernelCDF f κ ν
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
/-- The precoverage on `Scheme` of jointly surjective families.  -/
AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Init.Data.BitVec.Lemmas
BitVec.zero_ushiftRight : ∀ {w n : ℕ}, 0#w >>> n = 0#w
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaPairingExt_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)}
  {x y : (CategoryTheory.coyonedaPairing C).obj X}, x = y ↔ ∀ (Y : C), x.app Y = y.app Y
-- Init.Data.Int.Gcd
Int.gcd_sub_mul_right_left : ∀ (m n k : ℤ), (n - k * m).gcd m = n.gcd m
-- Mathlib.Data.List.Basic
List.surjective_head! : ∀ {α : Type u} [inst : Inhabited α], Function.Surjective List.head!
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to another `CompHausLike` preserves finite coproducts if they exist.  -/
CompHausLike.instPreservesFiniteCoproductsToCompHausLike : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] {P' : TopCat → Prop}
  (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop),
  CategoryTheory.Limits.PreservesFiniteCoproducts (CompHausLike.toCompHausLike h)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R n
-- Mathlib.Analysis.RCLike.Basic
RCLike.toPosMulReflectLT : ∀ {K : Type u_1} [inst : RCLike K], PosMulReflectLT K
-- Lean.Meta.Tactic.Grind.Types
/-- State of the E-matching module.  -/
Lean.Meta.Grind.GoalState.ematch : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.EMatch.State
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.cast_symm_apply : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M j),
  (MulEquiv.cast h).symm a = cast ⋯ a
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.instReprComp : Repr Mathlib.Tactic.Linarith.Comp
-- Init.Omega.Constraint
Lean.Omega.Constraint.div.eq_1 : ∀ (c : Lean.Omega.Constraint) (k : ℕ),
  c.div k =
    { lowerBound := Option.map (fun x => -(-x / ↑k)) c.lowerBound,
      upperBound := Option.map (fun y => y / ↑k) c.upperBound }
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The coefficients `a i` are positive.  -/
AkraBazziRecurrence.a_pos : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α), 0 < a i
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_2.eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1}
  {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1}
  (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp)
  (F_1 : (t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t)
  (F_2 : (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_1 t → motive_2 t)
  (F_3 :
    (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_2 t → motive_3 t)
  (F_4 :
    (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
      Lean.PrefixTreeNode.below_3 t → motive_4 t),
  Lean.PrefixTreeNode.brecOn_2 t F_1 F_2 F_3 F_4 = F_3 t (Lean.PrefixTreeNode.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Order.Category.BoolAlg
/-- The powerset functor. `Set` as a contravariant functor.  -/
typeToBoolAlgOp : CategoryTheory.Functor (Type u) BoolAlgᵒᵖ
-- Lean.Meta.Tactic.Simp.Arith.Nat.Simp
Lean.Meta.Simp.Arith.Nat.simpExpr? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointAux_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (hT : Dense ↑T.domain) (y : ↥T.adjointDomain) (x : ↥T.domain),
  inner 𝕜 ((LinearPMap.adjointAux hT) y) ↑x = inner 𝕜 (↑y) (↑T x)
-- Init.Meta.Defs
Lean.Name.beq_iff_eq : ∀ {m n : Lean.Name}, (m == n) = true ↔ m = n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roo α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Roo α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toArray_zip_of_finite : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toArray = it₁.toArray.zip it₂.toArray
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.add_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : CategoryTheory.Arrow.RightHomotopy f₁ g₁)
  (h₂ : CategoryTheory.Arrow.RightHomotopy f₂ g₂), (h₁.add h₂).hom = h₁.hom + h₂.hom
-- Mathlib.Topology.Neighborhoods
IsClosed.interior_union_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed t → interior (s ∪ t) ⊆ interior s ∪ t
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.inter_isBasis_iInter : ∀ {α : Type u_2} {M : Matroid α} {ι : Sort u_3} {I : Set α} [Nonempty ι] {X : ι → Set α},
  M.Indep I → (∀ (i : ι), M.IsBasis (X i ∩ I) (X i)) → M.IsBasis ((⋂ i, X i) ∩ I) (⋂ i, X i)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverBlockWith : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_filter_key : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, k ∈ Std.DHashMap.filter (fun a x => f a) m ↔ ∃ (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (i : EInt),
  WithBotTop.coe n ≤ i → ∀ (X : C), t.IsGE ((t.eTruncGE.obj i).obj X) n
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.eq_top_of_mem_invtSubmodule_of_forall_eq_univ : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] (P : RootPairing ι K M N) [P.IsRootSystem]
  (q : Submodule K M),
  q ≠ ⊥ →
    (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) →
      (∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ LinearMap.ker (P.coroot' i)) → Φ = Set.univ) →
        q = ⊤
-- Mathlib.Analysis.Complex.Trigonometric
Real.abs_sin_eq_sqrt_one_sub_cos_sq : ∀ (x : ℝ), |Real.sin x| = √(1 - Real.cos x ^ 2)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.OplaxTrans.Modification η θ},
  x = y ↔ x.app = y.app
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.typeClass.injEq : ∀ (extraErrorMsg? extraErrorMsg?_1 : Option Lean.MessageData),
  (Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg? =
      Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg?_1) =
    (extraErrorMsg? = extraErrorMsg?_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.penultimate_cons_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w w' : V} (h : G.Adj u v) (h₂ : G.Adj v w) (p : G.Walk w w'),
  (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h₂ p)).penultimate = (SimpleGraph.Walk.cons h₂ p).penultimate
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.one_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N}, SemidirectProduct.right 1 = 1
-- Mathlib.Order.Types.Defs
OrderType.type_le_type_iff : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.type α ≤ OrderType.type β ↔ Nonempty (α ↪o β)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.sum_mul_sub : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ},
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.StronglyAdapted 𝒢 ξ →
      (∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
        (∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
          MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
-- Mathlib.Lean.Meta.Basic
/-- Checks that `e` has type `expectedType` (i.e. that its type is defeq to `expectedType`
at the current transparency). If not, coerces `e` to this type
or fails with a descriptive error.  -/
Lean.Meta.ensureHasType : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.List.AList
AList.keys_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β), (AList.erase a s).keys = s.keys.erase a
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
then `F = E`.  -/
IntermediateField.eq_of_le_of_finrank_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [hfin : FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥E ≤ Module.finrank K ↥F → F = E
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.disjointBase : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Disjoint (Topology.RelCWComplex.openCell n i) D
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Ioo : ∀ {n : ℕ} (a b : Fin n), Finset.map Fin.valEmbedding (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
-- Init.Core
/-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`. -/
«term_↔_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {E : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} E] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : W.LeftFraction X Y) (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f).map F hF = f.map F hF
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_minus_one : ∀ (a : ℤ), a / -1 = -a
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.inseparable_lim_iff : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α] {f g : CauchyFilter α},
  Inseparable (↑f).lim (↑g).lim ↔ Inseparable f g
-- Std.Sat.AIG.RelabelNat
/-- Insert a `Decl.gate` into the `State` structure.
 -/
Std.Sat.AIG.RelabelNat.State.addGate : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {idx : ℕ} →
        {decls : Array (Std.Sat.AIG.Decl α)} →
          {hidx : idx < decls.size} →
            Std.Sat.AIG.RelabelNat.State α decls idx →
              (lhs rhs : Std.Sat.AIG.Fanin) →
                decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs → Std.Sat.AIG.RelabelNat.State α decls (idx + 1)
-- Init.Data.SInt.Lemmas
Int16.ofInt_int32ToInt : ∀ (x : Int32), Int16.ofInt x.toInt = x.toInt16
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- An equivalence between the height one and maximal spectra for rings of Krull dimension 1.  -/
IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum : {R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → ¬IsField R → IsDedekindDomain.HeightOneSpectrum R ≃ MaximalSpectrum R
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- Intermediate result for `CliffordAlgebraComplex.equiv`: clifford algebras over
`CliffordAlgebraComplex.Q` above can be converted to `ℂ`.  -/
CliffordAlgebraComplex.toComplex : CliffordAlgebra CliffordAlgebraComplex.Q →ₐ[ℝ] ℂ
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.strictAntiOn_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, StrictConcaveOn ℝ S f → (∀ x ∈ S, DifferentiableAt ℝ f x) → StrictAntiOn (deriv f) S
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_toDual : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.uIcc a b)
-- Mathlib.Order.Defs.PartialOrder
PartialOrder.toPreorder : {α : Type u_2} → [self : PartialOrder α] → Preorder α
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instIsZeroApply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  IsZeroApply (ContDiffMapSupportedIn E F n K) E F
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderSupOpposite : ∀ {α : Type u_1} {il : LE α} {im : Max α} [Std.LawfulOrderSup α], Std.LawfulOrderInf α
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- We can more explicitly show that a category has an initial object by specifying the object,
and showing there is a unique morphism from it to any other object.  -/
CategoryTheory.Limits.hasInitial_of_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (X ⟶ Y)]
  [∀ (Y : C), Subsingleton (X ⟶ Y)], CategoryTheory.Limits.HasInitial C
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3),
  (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
-- Init.Data.Nat.Lemmas
Nat.succ_min_succ : ∀ (x y : ℕ), min x.succ y.succ = (min x y).succ
-- Init.Control.Basic
/-- A type that can be used to reconstruct both a returned value and any state used by the outer
monad.
 -/
MonadControlT.stM : (m : Type u → Type v) → (n : Type u → Type w) → [self : MonadControlT m n] → Type u → Type u
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  CategoryTheory.PreservesPullbacksOfInclusions F
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [inst : L.Structure M] {N : Type u_2}
  [inst_1 : L.Structure N] {F : Type u_3} [inst_2 : FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N]
  {φ : L.BoundedFormula α n},
  φ.IsExistential → ∀ (f : F) {v : α → M} {xs : Fin n → M}, φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- The identity functor on a site is cover-preserving.  -/
CategoryTheory.idCoverPreserving : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.CoverPreserving J J (CategoryTheory.Functor.id C)
-- Init.Data.Vector.Lemmas
Vector.back_eq_of_push_eq : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs ys : Vector α n}, xs.push a = ys.push b → a = b
-- Init.Data.Int.LemmasAux
Int.toNat_sub_self_max : ∀ (a : ℤ), (a - max 0 a).toNat = 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapWithPostcondition_eq_toListRev_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition f it).toListRev =
    (Std.IterM.filterMapWithPostcondition (fun x => Std.Iterators.PostconditionT.map some (f x)) it).toListRev
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_algebraMap : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {A : Type u_8} {b : m → α} [inst : LinearOrder α] [inst_1 : CommSemiring R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : DecidableEq m] [inst_5 : Fintype m] (r : R),
  ((algebraMap R (Matrix m m A)) r).BlockTriangular b
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Γ_restrict_isLocalization : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
  IsLocalization.Away r ↑((↑(X.basicOpen r)).presheaf.obj (Opposite.op ⊤))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonFoldingRangeParams.toJson : Lean.Lsp.FoldingRangeParams → Lean.Json
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} [inst_2 : SizeOf α]
  (lhs rhs : aig.RefVec len), sizeOf { lhs := lhs, rhs := rhs } = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.Order.WithBot
/-- `WithBot.toDual` is the equivalence sending `⊥` to `⊤` and any `a : α` to `toDual a : αᵒᵈ`.
See `WithBot.toDualTopEquiv` for the related order-iso.  -/
WithBot.toDual : {α : Type u_1} → WithBot α ≃ WithTop αᵒᵈ
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNatClamp n).toNat = n
-- Lean.DocString.Extension
Lean.instInhabitedVersoDocString : Inhabited Lean.VersoDocString
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₂ = h.chosenPullback.p
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.LocallyQuasiFinite f],
  AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Data.List.GetD
List.getI_zero_eq_headI : ∀ {α : Type u} (l : List α) [inst : Inhabited α], l.getI 0 = l.headI
-- Mathlib.Data.NNRat.Defs
NNRat.sub_def : ∀ (p q : ℚ≥0), p - q = (↑p - ↑q).toNNRat
-- Batteries.Data.Nat.Basic
/-- Construct a natural number from a sequence of bits using little endian convention.
 -/
Nat.ofBits : {n : ℕ} → (Fin n → Bool) → ℕ
-- Mathlib.Data.Num.ZNum
ZNum.addCommGroup : AddCommGroup ZNum
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.getParam : Lean.Name → Lean.Syntax → Lean.AttrM Lean.MethodSpecsAttrData
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.neg_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {x : PreLp E} {i : α}, (-x) i = -x i
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- The category of R-semimodules and their morphisms.

Note that in the case of `R = ℕ`, we can not
impose here that the `ℕ`-multiplication field from the module structure is defeq to the one coming
from the `isAddCommMonoid` structure (contrary to what we do for all module structures in
mathlib), which creates some difficulties down the road.  -/
SemimoduleCat : (R : Type u) → [Semiring R] → Type (max u (v + 1))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?ₘ.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α]
  (l l_1 : Std.DTreeMap.Internal.Impl α β), l = l_1 → ∀ (k : α), l.get?ₘ k = l_1.get?ₘ k
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertIfNew : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Init.Data.Array.Lemmas
Array.snd_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.2 = Array.map Prod.snd xs
-- Mathlib.RingTheory.SimpleModule.Basic
isSimpleModule_iff_isCoatom : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M},
  IsSimpleModule R (M ⧸ m) ↔ IsCoatom m