mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- For all sets `s` in `(μ.sigmaFiniteSetWRT ν)ᶜ`, if `ν s ≠ 0` then `μ s = ∞`.  -/
MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SFinite ν],
  s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ → ν s ≠ 0 → μ s = ⊤
-- Mathlib.Topology.Bases
TopologicalSpace.isBasis_countableBasis : ∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
  TopologicalSpace.IsTopologicalBasis (TopologicalSpace.countableBasis α)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.h : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Logic.Function.Iterate
Function.involutive_iff_iter_2_eq_id : ∀ {α : Sort u_1} {f : α → α}, Function.Involutive f ↔ f^[2] = id
-- Mathlib.Control.Functor
/-- `Const.mk` is the canonical map `α → Const α β` (the identity), and
it can be used as a pattern to extract this value.  -/
Functor.Const.mk : {α : Type u_1} → {β : Type u_2} → α → Functor.Const α β
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_inv_apply : ∀ {R S : SemiRingCat} (e : R ≅ S) (s : ↑S),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Init.Data.UInt.Lemmas
UInt8.le_of_eq : ∀ {a b : UInt8}, a = b → a ≤ b
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonOneHom_apply : ∀ {α : Type u_2} [inst : One α] (a : α), Finset.singletonOneHom a = {a}
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.finrank F ↥⊥ = 1
-- Mathlib.Algebra.Ring.Idempotent
/-- `a + b` is idempotent when `a` and `b` anti-commute.  -/
IsIdempotentElem.add : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → a * b + b * a = 0 → IsIdempotentElem (a + b)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.not_le_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert rhs lhs p = true →
    ¬Lean.Grind.Linarith.Expr.denote ctx lhs ≤ Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p < 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.support = p.support.reverse
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_eq_top : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α}, ¬P s → MeasureTheory.extend m s = ⊤
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_eq_refl : ∀ {α : Type u_1} {s : Multiset α}, Multiset.Rel (fun x1 x2 => x1 = x2) s s
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.map₂HomologicalComplex_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c : ComplexShape J)
  [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c]
  [inst_10 : ∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
  (K₁ : HomologicalComplex C₁ c₁) {X Y : HomologicalComplex C₂ c₂} (g : X ⟶ Y),
  ((F.map₂HomologicalComplex c₁ c₂ c).obj K₁).map g =
    HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) g F c
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.noMatch.sizeOf_spec : sizeOf Mathlib.Tactic.GRewrite.Progress.noMatch✝ = 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_toFun : ∀ {basis : Tactic.ComputeAsymptotics.Basis}, Tactic.ComputeAsymptotics.MultiseriesExpansion.zero.toFun = 0
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.instInhabited : {C : Type u} → [Inhabited C] → Inhabited (CategoryTheory.LocallyDiscrete C)
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.GrpCat.Hom.mk : {A B : GrpCat} → (↑A →* ↑B) → A.Hom B
-- Mathlib.Data.ZMod.Basic
ZMod.eq_2 : ∀ (n : ℕ), ZMod n.succ = Fin (n + 1)
-- Mathlib.SetTheory.Cardinal.Defs
/-- The equivalence relation on types given by equivalence (bijective correspondence) of types.
Quotienting by this equivalence relation gives the cardinal numbers.
 -/
Cardinal.isEquivalent : Setoid (Type u)
-- Mathlib.Data.Nat.Prime.Nth
Nat.nth_prime_one_eq_three : Nat.nth Nat.Prime 1 = 3
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.pi_top : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] (s : Set ι), (Subalgebra.pi s fun i => ⊤) = ⊤
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shift_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a b c : A),
  a + b = c → ∀ [P.IsClosedUnderIsomorphisms], (P.shift b).shift a = P.shift c
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mk.sizeOf_spec : ∀ (unify zetaDelta : Bool) (lctxInitialNextIndex : ℕ) (mvarsNew mvarsToCheckType : Array Lean.MVarId),
  sizeOf
      { unify := unify, zetaDelta := zetaDelta, lctxInitialNextIndex := lctxInitialNextIndex, mvarsNew := mvarsNew,
        mvarsToCheckType := mvarsToCheckType } =
    1 + sizeOf unify + sizeOf zetaDelta + sizeOf lctxInitialNextIndex + sizeOf mvarsNew + sizeOf mvarsToCheckType
-- Aesop.Script.TacticState
Aesop.Script.instInhabitedTacticState.default : Aesop.Script.TacticState
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.id_apply : ∀ {x : ℕ}, ArithmeticFunction.id x = x
-- Std.Data.ExtDTreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.ExtDTreeMap.Const.mergeWith : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] →
        (α → β → β → β) →
          Std.ExtDTreeMap α (fun x => β) cmp → Std.ExtDTreeMap α (fun x => β) cmp → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_le_descFactorial : ∀ (n k : ℕ), n.choose k ≤ n.descFactorial k
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.Approx.head'.match_1.splitter : {F : PFunctor.{u_1, u_2}} →
  (motive : (x : ℕ) → PFunctor.Approx.CofixA F x.succ → Sort u_3) →
    (x : ℕ) →
      (x_1 : PFunctor.Approx.CofixA F x.succ) →
        ((x : ℕ) → (i : F.A) → (a : F.B i → PFunctor.Approx.CofixA F x) → motive x (PFunctor.Approx.CofixA.intro i a)) →
          motive x x_1
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizedGCDMonoid.toGCDMonoid : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : NormalizedGCDMonoid α] → GCDMonoid α
-- Mathlib.RingTheory.Binomial
Ring.multichoose_one : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (k : ℕ),
  Ring.multichoose 1 k = 1
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The canonical fork on `f g : A ⟶ B` is limiting.  -/
CommRingCat.Under.equalizerForkIsLimit : {R : CommRingCat} →
  {A B : CategoryTheory.Under R} → (f g : A ⟶ B) → CategoryTheory.Limits.IsLimit (CommRingCat.Under.equalizerFork f g)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis_iff_indep_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.closureCommGroupOfComm.eq_1 : ∀ {G : Type u_1} [inst : Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x),
  Subgroup.closureCommGroupOfComm hcomm = inferInstance
-- Mathlib.Order.IsNormal
Order.IsNormal.lt_iff_exists_lt : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  Order.IsNormal f → Order.IsSuccLimit a → ∀ {b : β}, b < f a ↔ ∃ a' < a, b < f a'
-- Std.Data.TreeMap.Lemmas
/-- Variant of `getElem?_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.TreeMap.map f t)[k]? = Option.pmap (fun v h' => f (t.getKey k h') v) t[k]? ⋯
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
AddMonoidAlgebra.instIsCancelAddZeroOfIsCancelAddOfUniqueSums : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsCancelMulZero R] [inst_3 : Add A] [UniqueSums A],
  IsCancelMulZero (AddMonoidAlgebra R A)
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.visitRapp : Lean.Environment → Lean.MVarId → Aesop.Rapp → Lean.MetaM (Array Aesop.MVarClusterRef × Lean.Environment)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
exists_affineIndependent : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap_comp_descOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S S₁ : CategoryTheory.ShortComplex C} {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] (φ : S₁ ⟶ S) [inst_3 : S₁.HasRightHomology] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ)
      (CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) h) =
    CategoryTheory.CategoryStruct.comp (S₁.descOpcycles (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯) h
-- Mathlib.Algebra.Polynomial.Monic
/-- The constructor for `MonicDegreeEq` given a monic polynomial of degree `n`.  -/
Polynomial.MonicDegreeEq.mk : {R : Type u} →
  {n : ℕ} → [inst : Semiring R] → (p : Polynomial R) → p.Monic → p.natDegree = n → Polynomial.MonicDegreeEq R n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).getKeyD a fallback = fallback
-- Mathlib.Topology.Algebra.MvPolynomial
MvPolynomial.continuous_eval : ∀ {X : Type u_1} {σ : Type u_2} [inst : TopologicalSpace X] [inst_1 : CommSemiring X] [IsTopologicalSemiring X]
  (p : MvPolynomial σ X), Continuous fun x => (MvPolynomial.eval x) p
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instIsIsoLeft : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (e : X ⟶ Y) [CategoryTheory.IsIso e],
  CategoryTheory.IsIso e.left
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f g : CompleteLatticeHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_mono : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ), A.EqId ↔ CategoryTheory.Mono A.e
-- Init.Data.Nat.Lemmas
Nat.pow_dvd_pow_iff_pow_le_pow : ∀ {k l x : ℕ}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
-- Init.Data.Int.Basic
/-- Returns the “sign” of the integer as another integer:
* `1` for positive numbers,
* `-1` for negative numbers, and
* `0` for `0`.

Examples:
* `Int.sign 34 = 1`
* `Int.sign 2 = 1`
* `Int.sign 0 = 0`
* `Int.sign -1 = -1`
* `Int.sign -362 = -1`
 -/
Int.sign : ℤ → ℤ
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_homToOrderHom_zero : ∀ {n : ℕ} (i : Fin n), (SimplexCategory.Hom.toOrderHom (SimplexCategory.mkOfSucc i)) 0 = i.castSucc
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.cocone_pt : ∀ (X : Type u) (κ : Cardinal.{u}), (HasCardinalLT.Set.cocone X κ).pt = X
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHomSuperset_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : spectrum R a ⊆ s) (x : C(↑s, R)),
  (cfcHomSuperset ha hs) x = (cfcHom ha) (x.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯ })
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_eq_projVandermonde : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R), Matrix.vandermonde v = Matrix.projVandermonde v 1
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.normalizeAux.match_1.eq_3 : ∀ {B : Type u_2} [inst : Quiver B] {a : B}
  (motive : (x x_1 : B) → Quiver.Path a x → CategoryTheory.FreeBicategory.Hom x x_1 → Sort u_3) (x x_1 : B)
  (p : Quiver.Path a x) (b : B) (f : CategoryTheory.FreeBicategory.Hom x b)
  (g : CategoryTheory.FreeBicategory.Hom b x_1)
  (h_1 : (x x_2 : B) → (p : Quiver.Path a x) → (f : x ⟶ x_2) → motive x x_2 p (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (x : B) → (p : Quiver.Path a x) → motive x x p (CategoryTheory.FreeBicategory.Hom.id x))
  (h_3 :
    (x x_2 : B) →
      (p : Quiver.Path a x) →
        (b : B) →
          (f : CategoryTheory.FreeBicategory.Hom x b) →
            (g : CategoryTheory.FreeBicategory.Hom b x_2) → motive x x_2 p (f.comp g)),
  (match x, x_1, p, f.comp g with
    | x, x_2, p, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_2 p f
    | x, .(x), p, CategoryTheory.FreeBicategory.Hom.id .(x) => h_2 x p
    | x, x_2, p, f.comp g => h_3 x x_2 p b f g) =
    h_3 x x_1 p b f g
-- Lean.Meta.CoeAttr
/-- Add `name` to the coercion extension and add a coercion delaborator for the function.  -/
Lean.Meta.registerCoercion : Lean.Name → optParam (Option Lean.Meta.CoeFnInfo) none → Lean.MetaM Unit
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction.eq_def : ∀ {σs : List (Type u)} (env : List (Std.Do.SPred σs)),
  Std.Do.SPred.conjunction env =
    match env with
    | [] => ⌜True⌝
    | P :: env => spred(P ∧ Std.Do.SPred.conjunction env)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_le_of_le_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => c ≤ x],
  c ≤ a → Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico a b
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₂_add_one : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'')
  (n : ℕ),
  Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
    ⟨CategoryTheory.CategoryStruct.comp (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).fst
        (HomologicalComplex.xPrevIso Q ⋯).inv,
      ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom
          (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).snd.fst,
        ⋯⟩⟩
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution.map (HomotopicalAlgebra.CofibrantObject.toHoCat.map f) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f)
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Returns `true` if adding the assignment `e := v` to `a` will falsify any asserted disequality in core.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.ModelUtil.0.Lean.Meta.Grind.Arith.satisfyDiseqs : Lean.Meta.Grind.Goal → Std.HashMap Lean.Expr ℚ → Lean.Expr → ℤ → Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_3.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.gt → motive Ordering.gt) → (x = Ordering.eq → motive Ordering.eq) → motive x
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.val_lt_val : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] {a b : AddUnits α}, ↑a < ↑b ↔ a < b
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsExtensionProduct : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C), (P.extensionProduct Q).IsClosedUnderIsomorphisms
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- An auxiliary lemma for `toSphereBallBound_mul_measure_unitBall_le_toSphere_ball`.
The estimate in this lemma is highly suboptimal.
For a non-private lemma, we should aim for a more precise and a more general fact
(e.g., an estimate on the radius of a ball centered at `t • x`
that is guaranteed to be a subset of the cone.  -/
_private.Mathlib.MeasureTheory.Constructions.HaarToSphere.0.MeasureTheory.Measure.ball_subset_sector_of_small_epsilon : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E),
  ‖x‖ = 1 →
    ∀ (ε : ℝ),
      0 < ε → ε ≤ 2 → Metric.ball ((1 - ε / 4) • x) (ε / 4) ⊆ Set.Ioo 0 1 • (Metric.ball x ε ∩ Metric.sphere 0 1)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.top_coe_inv : ∀ {K : Type u} [inst : Field K] (x : ↥⊤), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblXYZ P = P 1 ^ 4 • ![0, 1, 0]
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The result of evaluating `subject` using the ring tactic.  -/
Mathlib.Tactic.Determinant.Cert.result : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      (self : Mathlib.Tactic.Determinant.Cert rα) → Mathlib.Tactic.Determinant.CertResult rα self.subject
-- Aesop.Script.Tactic
Aesop.Script.STactic : Type
-- Mathlib.Data.ENNReal.Action
ENNReal.smulCommClass_right : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ENNReal N] [inst_1 : SMul M N] [SMulCommClass M ENNReal N],
  SMulCommClass M NNReal N
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_empty : ∀ {α : Type u} [inst : Semiring α], Ideal.span ∅ = ⊥
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_add_add_eq_append : ∀ {m n k : ℕ}, (m...m + n + k).toList = (m...m + n).toList ++ ((m + n)...m + n + k).toList
-- Mathlib.Order.Hom.Lattice
/-- An `InfHom` preserves infima.

Do not use this directly. Use `map_inf` instead.  -/
LatticeHom.map_inf' : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] (self : LatticeHom α β) (a b : α),
  self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.clm_prodMap : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M}
  {x : M}, MDiffAt[s] g x → MDiffAt[s] f x → (MDiffAt[s] fun x => (g x).prodMap (f x)) x
-- Aesop.Rule.Name
Aesop.DisplayRuleName.normSimp : Aesop.DisplayRuleName
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.of_is_bilimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPullback 0 0 b.inl b.inr
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.nhds_hasBasis : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) (x₀ : G),
  (nhds x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- Given a map `φ : R[X] →ₐ[R] S`. Suppose `t = φ r / φ p` is integral over `R[X]` where
`p` is monic with `deg p > deg r`, then `t` is also integral over `R`.  -/
isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (φ : Polynomial R →ₐ[R] S) (t : S) (p r : Polynomial R),
  φ.IsIntegralElem t → p.Monic → r.natDegree < p.natDegree → φ p * t = φ r → IsIntegral R t