mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.mk.injEq : ∀ (ref : Lean.Syntax) (lhs rhs : Lean.Level) (ctx? : Option Lean.Meta.DefEqContext) (ref_1 : Lean.Syntax)
  (lhs_1 rhs_1 : Lean.Level) (ctx?_1 : Option Lean.Meta.DefEqContext),
  ({ ref := ref, lhs := lhs, rhs := rhs, ctx? := ctx? } =
      { ref := ref_1, lhs := lhs_1, rhs := rhs_1, ctx? := ctx?_1 }) =
    (ref = ref_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1 ∧ ctx? = ctx?_1)
-- Mathlib.Data.Multiset.Defs
Multiset.eq_of_le_of_card_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → t.card ≤ s.card → s = t
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_equiv_apply : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F ≃ₗ[K] E) (x : ↥L), ↑((ZLattice.comap_equiv K L e) x) = e.symm ↑x
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_eq_single : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, (∀ x ∈ xs, p x = false) → List.splitOnP p xs = [xs]
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.hom_comp : ∀ {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  UniformSpaceCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    ⟨⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f), ⋯⟩
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.noConfusionType : Sort v✝ → Lean.Lsp.SemanticTokenType → Lean.Lsp.SemanticTokenType → Sort v✝
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.sub_one_ne_zero : ∀ {R : Type u_4} [inst : CommRing R] {n : ℕ} {ζ : R}, 1 < n → IsPrimitiveRoot ζ n → ζ - 1 ≠ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_neg : ∀ {α : Type u_2} [inst : Neg α] (S : Set (Set α)), -⋂₀ S = ⋂ s ∈ S, -s
-- Mathlib.CategoryTheory.Yoneda
/-- Corepresenting `F` composed with universe lifting is the same as corepresenting `F`.  -/
CategoryTheory.Functor.corepresentableByUliftFunctorEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v)} →
      {X : C} → (F.comp CategoryTheory.uliftFunctor.{w, v}).CorepresentableBy X ≃ F.CorepresentableBy X
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC_nc.induct_unfolding : ∀ (p : Lean.Grind.CommRing.Poly) (c : ℕ) (motive : ℕ → Lean.Grind.CommRing.Poly → Prop),
  motive 0 (Lean.Grind.CommRing.Poly.num 1) →
    motive 1 p →
      (∀ (k : ℕ), (k = 0 → False) → motive k (p.powC_nc k c) → motive k.succ ((p.powC_nc k c).mulC_nc p c)) →
        ∀ (k : ℕ), motive k (p.powC_nc k c)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f],
  (CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.id (f a)) =
    CategoryTheory.CategoryStruct.id (∏ᶜ f)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instSubOffset : Sub Std.Time.Month.Offset
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
/-- This lemma expresses `Iter.allM` in terms of `IterM.allM`.
It requires all involved types to live in `Type 0`.
 -/
Std.Iter.allM_eq_allM_mapM_pure : ∀ {α β : Type} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [inst_6 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.allM p it = ULift.down <$> Std.IterM.allM (fun x => ULift.up <$> p x) (Std.Iter.mapM pure it)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_ε : ∀ (a : UnitAddCircle), (HurwitzZeta.hurwitzOddFEPair a).ε = 1
-- Init.Grind.Attr
/-- The `_=_` modifier acts like a macro which expands to `=` and `=_`.  It adds two patterns,
allowing the equality theorem to trigger in either direction.
 -/
Lean.Parser.Attr.grindEqBoth : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k' = some v
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r r' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size)) →
          ((ℓ : Std.DTreeMap.Internal.Impl α β) →
              (hℓ₁ : ℓ.Balanced) →
                (hℓ₂ : ℓ.size = r'.size + r.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
            motive x
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_update_eq_filter_piFinset_mem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} [inst_2 : (a : α) → DecidableEq (δ a)]
  (s : (i : α) → Finset (δ i)) (i : α) {t : Finset (δ i)},
  t ⊆ s i → Fintype.piFinset (Function.update s i t) = {f ∈ Fintype.piFinset s | f i ∈ t}
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.rmatch.match_1.splitter : {α : Type u_1} →
  (motive : RegularExpression α → List α → Sort u_2) →
    (x : RegularExpression α) →
      (x_1 : List α) →
        ((P : RegularExpression α) → motive P []) →
          ((P : RegularExpression α) → (a : α) → (as : List α) → motive P (a :: as)) → motive x x_1
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.mk.inj : ∀ {len len_1 : ℕ}, { len := len } = { len := len_1 } → len = len_1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Return the canonical encoding of `e` as a `Array Key`.
This is used for looking up `e` in a `RefinedDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.encodeExpr : Lean.Expr → Bool → Lean.MetaM (Lean.Meta.RefinedDiscrTree.Key × List Lean.Meta.RefinedDiscrTree.Key)
-- Init.Data.Array.Subarray
Subarray.instEmptyCollection : {α : Type u_1} → EmptyCollection (Subarray α)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- Two submodules in an orthogonal family with different indices are orthogonal.  -/
OrthogonalFamily.isOrtho : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ {i j : ι}, i ≠ j → V i ⟂ V j
-- Std.Do.PostCond
/-- An assertion about each potential exception that's declared in a postcondition shape.

Examples:
```lean example
example : ExceptConds (.pure) = Unit := rfl
example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
```
 -/
Std.Do.ExceptConds : Std.Do.PostShape → Type u
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sSup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set (Set M)),
  Submodule.span R (⋃₀ s) = sSup (Submodule.span R '' s)
-- Mathlib.Probability.BorelCantelli
/-- **The second Borel-Cantelli lemma**: Given a sequence of independent sets `(sₙ)` such that
`∑ n, μ sₙ = ∞`, `limsup sₙ` has measure 1.  -/
ProbabilityTheory.measure_limsup_eq_one : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ → ∑' (n : ℕ), μ (s n) = ⊤ → μ (Filter.limsup s Filter.atTop) = 1
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Pullback.lift.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (z : Bundle.TotalSpace F (f *ᵖ E)),
  Bundle.Pullback.lift f z = ⟨f z.proj, z.snd⟩
-- Mathlib.Analysis.Complex.Poisson
/-- Taking real parts commutes with the Herglotz–Riesz kernel integral of a real-valued
circle-integrable function.
 -/
re_circleAverage_herglotzRieszKernel_smul : ∀ {R : ℝ} {w : ℂ} {g : ℂ → ℝ},
  CircleIntegrable g 0 R →
    w ∈ Metric.ball 0 R →
      (Real.circleAverage (fun ζ => herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R).re =
        Real.circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • g) 0 R
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Cases lemma for `W` types  -/
MvPFunctor.wCases : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {C : P.W α → Sort v} →
        ((a : P.A) → (f' : (P.drop.B a).Arrow α) → (f : P.last.B a → P.W α) → C (P.wMk a f' f)) → (x : P.W α) → C x
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_subtype_zero_eq : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), LinearMap.ofIsCompl hpq p.subtype 0 = p.projection q hpq
-- Mathlib.Data.Finsupp.Order
Finsupp.add_eq_zero_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  (f g : ι →₀ α), f + g = 0 ↔ f = 0 ∧ g = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  (Std.DTreeMap.filterMap f t).isEmpty = false ↔
    ∃ k, ∃ (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Const.get t k h)).isSome = true
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The `A ⧸ I`-vector space `I ⧸ I ^ 2`.  -/
IsLocalRing.CotangentSpace : (R : Type u_1) → [inst : CommRing R] → [IsLocalRing R] → Type u_1
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (P : Type u_3) [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P],
  MulEquiv.coprodAssoc M N P =
    (Monoid.Coprod.lift (Monoid.Coprod.map (MonoidHom.id M) Monoid.Coprod.inl)
          (Monoid.Coprod.inr.comp Monoid.Coprod.inr)).toMulEquiv
      (Monoid.Coprod.lift (Monoid.Coprod.inl.comp Monoid.Coprod.inl)
        (Monoid.Coprod.map Monoid.Coprod.inr (MonoidHom.id P)))
      ⋯ ⋯
-- Init.Data.Vector.Extract
Vector.extract_push_of_le : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {b : α} {start stop : ℕ} (h : stop ≤ n),
  (xs.push b).extract start stop = Vector.cast ⋯ (xs.extract start stop)
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.Kernel.absolutelyContinuous_comp_of_absolutelyContinuous : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ]
  [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] {ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.SFinite ν],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous ν) → ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_pos : ∀ (n : ℕ), 0 < n.doubleFactorial
-- Mathlib.Data.List.Pi
List.pi_cons : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Type u_2} (i : ι) (l : List ι) (t : (j : ι) → List (α j)),
  (i :: l).pi t = List.flatMap (fun b => List.map (List.Pi.cons i l b) (l.pi t)) (t i)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_ofBool : ∀ (b : Bool), (BitVec.ofBool b).toFin = Fin.ofNat 2 b.toNat
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instInfOpenNormalSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → Min (OpenNormalSubgroup G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ⟶ f'.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom)
      CategoryTheory.CostructuredArrow.homMk._auto_1),
  (CategoryTheory.CostructuredArrow.homMk g w).left = g
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X}
  {x : X}, (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (s.sup f) t x
-- Mathlib.Topology.Instances.Nat
Nat.instProperSpace : ProperSpace ℕ
-- Mathlib.GroupTheory.CoprodI
/-- The first letter of a `NeWord`  -/
Monoid.CoprodI.NeWord.head : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j : ι} → Monoid.CoprodI.NeWord M i j → M i
-- Init.Data.BitVec.Lemmas
BitVec.neg_mul_neg : ∀ {w : ℕ} (x y : BitVec w), -x * -y = x * y
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_refl : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M],
  Finsupp.mapRange.addEquiv (AddEquiv.refl M) = AddEquiv.refl (ι →₀ M)
-- Lean.Data.Position
Lean.instDecidableEqPosition.decEq : (x x_1 : Lean.Position) → Decidable (x = x_1)
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α →CO β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofDarts.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} (l : List G.Dart) (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l),
  SimpleGraph.Walk.ofDarts l hne hchain = SimpleGraph.Walk.ofDarts l hne hchain
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a complete lattice
with possibly different definitional equalities.  -/
CompleteLattice.copy : {α : Type u} →
  (c : CompleteLattice α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sSup : Set α → α) →
                          sSup = SupSet.sSup → (sInf : Set α → α) → sInf = InfSet.sInf → CompleteLattice α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α},
  s.Countable → s.PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
-- Mathlib.GroupTheory.Congruence.Defs
Con.hasDiv.eq_1 : ∀ {M : Type u_1} [inst : Group M] (c : Con M), c.hasDiv = { div := Quotient.map₂ (fun x1 x2 => x1 / x2) ⋯ }
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_radical_le : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) {I : Ideal R}, Ideal.map f I.radical ≤ (Ideal.map f I).radical
-- Init.Data.Iterators.Consumers.Access
/-- An induction principle for `Iter.atIdxSlow?`.

This lemma provides a functional induction principle for reasoning about `Iter.atIdxSlow? n it`.

The induction follows the structure of iterator steps.
- base case: when we reach the desired index (`n = 0`) and get a `.yield` step
- inductive case: when we have a `.yield` step but need to continue (`n > 0`)
- skip case: when we encounter a `.skip` step and continue with the same index
- done case: when the iterator is exhausted and we return `none`
 -/
Std.Iter.atIdxSlow?.induct_unfolding : ∀ {α β : Type u} [inst : Std.Iterator α Id β] [Std.Iterators.Productive α Id]
  (motive : ℕ → Std.Iter β → Option β → Prop),
  (∀ (it it' : Std.Iter β) (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out)),
      it.step = ⟨Std.IterStep.yield it' out, property⟩ → motive 0 it (some out)) →
    (∀ (it it' : Std.Iter β) (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out)),
        it.step = ⟨Std.IterStep.yield it' out, property⟩ →
          ∀ (k : ℕ), motive k it' (Std.Iter.atIdxSlow? k it') → motive k.succ it (Std.Iter.atIdxSlow? k it')) →
      (∀ (n : ℕ) (it it' : Std.Iter β) (property : it.IsPlausibleStep (Std.IterStep.skip it')),
          it.step = ⟨Std.IterStep.skip it', property⟩ →
            motive n it' (Std.Iter.atIdxSlow? n it') → motive n it (Std.Iter.atIdxSlow? n it')) →
        (∀ (n : ℕ) (it : Std.Iter β) (property : it.IsPlausibleStep Std.IterStep.done),
            it.step = ⟨Std.IterStep.done, property⟩ → motive n it none) →
          ∀ (n : ℕ) (it : Std.Iter β), motive n it (Std.Iter.atIdxSlow? n it)
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d_none_eq_zero' : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (i j : Option ι), j = none → HomologicalComplex.extend.d K i j = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ^ z < y ^ z ↔ x < y)
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.EnoughInjectives D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [G.PreservesInjectiveObjects], F.PreservesMonomorphisms
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm_isPowMul : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L], IsPowMul ⇑(spectralAlgNorm K L)
-- Mathlib.Topology.CantorBendixson
CantorBendixson.perfectKernel_mono : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X},
  s ⊆ t → CantorBendixson.perfectKernel s ⊆ CantorBendixson.perfectKernel t
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.sum_variance_truncation_le : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  {X : Ω → ℝ},
  MeasureTheory.Integrable X MeasureTheory.volume →
    0 ≤ X →
      ∀ (K : ℕ),
        ∑ j ∈ Finset.range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (ProbabilityTheory.truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.M : Type → Type
-- Mathlib.Data.Countable.Defs
instCountableFin : ∀ {n : ℕ}, Countable (Fin n)
-- Lean.Meta.Basic
/-- Return current transparency setting/mode.  -/
Lean.Meta.getTransparency : Lean.MetaM Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.neg_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv}, f.LimZero → (-f).LimZero
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_vsub : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VSub α β] (s : (i : ι) → κ i → Set β)
  (t : Set β), (⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_uncurry_index' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : AddCommMonoid N]
  (f : α →₀ β →₀ M) (g : α → β → M → N), (f.uncurry.sum fun p c => g p.1 p.2 c) = f.sum fun a f => f.sum (g a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a k : α} {v : β k}, (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_self : ∀ (n : ℕ), ↑n = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_inv : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) [inst : CategoryTheory.IsIso f],
  A.preimage (CategoryTheory.inv f) = A.image f
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.restrictSurjective_of_add_le_ENatCard : ∀ {α : Type u_1} {m n : ℕ}, ↑m + ↑n ≤ ENat.card α → Function.Surjective fun x => (Fin.castAddEmb n).trans x
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.globalEquiv_compatibility : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : WellFoundedLT ι] [inst_2 : SuccOrder ι] [inst_3 : InverseSystem f]
  (equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x })
  (equivLim : (i : ι) → Order.IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Set.Iio i)), ↑(e x) l = f ⋯ x }) ⦃i : ι⦄
  (hi : ¬IsMax i) (x : F (Order.succ i)),
  (InverseSystem.globalEquiv equivSucc equivLim (Order.succ i)) x ⟨i, ⋯⟩ = (↑(equivSucc i hi) x).2
-- Batteries.Recycling.RBTree.Basic
/-- The core of the `erase` function. The tree returned from this function has a broken invariant,
which is restored in `erase`.
 -/
RBTree.RBNode.del : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → RBTree.RBNode α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertMax : ∀ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced},
  (Std.DTreeMap.Internal.Impl.insertMax k v t h).impl.toListModel = t.toListModel ++ [⟨k, v⟩]
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.Entry.mk.sizeOf_spec : ∀ (name : Aesop.RuleName) (pattern : Aesop.RulePattern),
  sizeOf { name := name, pattern := pattern } = 1 + sizeOf name + sizeOf pattern
-- Mathlib.Analysis.Convex.Star
starConvex_iff_forall_ne_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E},
  x ∈ s → (StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (d : D), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)) → F.Initial
-- Mathlib.LinearAlgebra.Dimension.Torsion.Basic
rank_quotient_eq_of_le_torsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {M' : Submodule R M}, M' ≤ Submodule.torsion R M → Module.rank R (M ⧸ M') = Module.rank R M
-- Init.Data.Int.DivMod.Lemmas
Int.tmod.eq_3 : ∀ (m n : ℕ), (Int.negSucc m).tmod (Int.ofNat n) = -Int.ofNat (m.succ % n)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).inv
      (CategoryTheory.Limits.equalizerSubobject f g).arrow =
    CategoryTheory.Limits.equalizer.ι f g
-- Mathlib.RingTheory.Ideal.Nonunits
coe_subset_nonunits : ∀ {α : Type u_2} [inst : Semiring α] {I : Ideal α}, I ≠ ⊤ → ↑I ⊆ nonunits α
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum_obj_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  (a : A), (F.sum G).obj (Sum.inl a) = Sum.inl (F.obj a)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_ofReal_re : ∀ (x : ℝ), (Complex.cos ↑x).re = Real.cos x