mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `G : Cone F ⥤ Cone F'` preserves terminal objects, it preserves limit cones.  -/
CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F : CategoryTheory.Functor J C} →
                  {F' : CategoryTheory.Functor K D} →
                    (G : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone F')) →
                      [CategoryTheory.Limits.PreservesLimit
                            (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cone F)) G] →
                        {c : CategoryTheory.Limits.Cone F} →
                          CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (G.obj c)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.saveState : Lean.Elab.Tactic.Grind.GrindTacticM Lean.Elab.Tactic.Grind.SavedState
-- Mathlib.Data.EReal.Inv
EReal.min_neg_neg : ∀ (x y : EReal), min (-x) (-y) = -max x y
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} {f₃ : F₁ ⟶ F₃},
  CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃ →
    ∀ [CategoryTheory.Presheaf.IsLocallySurjective J f₃], CategoryTheory.Presheaf.IsLocallySurjective J f₂
-- Init.Data.Vector.Attach
Vector.mem_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {H : ∀ a ∈ xs, p a}
  {b : β}, b ∈ Vector.pmap f xs H ↔ ∃ a, ∃ (h : a ∈ xs), f a ⋯ = b
-- Init.Data.BitVec.Lemmas
BitVec.two_pow_le_toInt_mul_toInt_iff : ∀ {w : ℕ} {x y : BitVec w},
  2 ^ (w - 1) ≤ x.toInt * y.toInt ↔
    (BitVec.signExtend (w * 2) (BitVec.intMax w)).slt (BitVec.signExtend (w * 2) x * BitVec.signExtend (w * 2) y) = true
-- Mathlib.Order.RelSeries
RelSeries.smash_succ_natAdd : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length),
  (p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.toEmbedding_sumCongr : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H'),
  (f.sumCongr g).toEmbedding = f.toEmbedding.sum g.toEmbedding
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_modify_eq_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β → β}, (t.modify k f).minKey! = t.minKey!
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_ext : ∀ {M N : AddMonCat} {f g : M ⟶ N}, AddMonCat.Hom.hom f = AddMonCat.Hom.hom g → f = g
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffOn_diffeomorph_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : M' → M},
  m ≤ n → ∀ {s : Set M'}, ContMDiffOn I' J m (⇑h ∘ f) s ↔ ContMDiffOn I' I m f s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.instDecidableEqPoint : {R : Type u_1} → {inst : CommRing R} → {W' : WeierstrassCurve.Affine R} → [DecidableEq R] → DecidableEq W'.Point
-- Mathlib.CategoryTheory.Balanced
/-- A category is called balanced if any morphism that is both monic and epic is an isomorphism.  -/
CategoryTheory.Balanced : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Order.Filter.CardinalInter
Filter.le_cardinalGenerate_iff_of_cardinalInterFilter : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {f : Filter α} [CardinalInterFilter f c] (hc : 2 < c),
  f ≤ Filter.cardinalGenerate g hc ↔ g ⊆ f.sets
-- Mathlib.GroupTheory.CoprodI
/-- An element of `M i`, the first letter of the word.  -/
Monoid.CoprodI.Word.Pair.head : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → Monoid.CoprodI.Word.Pair M i → M i
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The fields of `StrictSegal` define an equivalence between `X _⦋m⦌ₙ₊₁`
and `Path X m`.  -/
SSet.Truncated.StrictSegal.spineEquiv : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    X.StrictSegal →
      (m : ℕ) →
        (h : autoParam (m ≤ n + 1) _auto_33✝) → X.obj (Opposite.op { obj := { len := m }, property := h }) ≃ X.Path m
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], ↑0 = 0
-- Mathlib.Logic.Function.Basic
Function.swap_ge : ∀ {α : Type u_4} [inst : LE α], (Function.swap fun x1 x2 => x1 ≥ x2) = fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R), (γ.smul a).φK = a • γ.φK
-- Mathlib.Algebra.Ring.Invertible
/-- A version of `inv_sub_inv'` for `invOf`.  -/
invOf_sub_invOf : ∀ {R : Type u_1} [inst : Ring R] (a b : R) [inst_1 : Invertible a] [inst_2 : Invertible b], ⅟a - ⅟b = ⅟a * (b - a) * ⅟b
-- Std.Data.DHashMap.Basic
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.DHashMap.forM : {α : Type u} →
  {β : α → Type v} →
    {m : Type w → Type w'} →
      [Monad m] →
        {x : BEq α} → {x_1 : Hashable α} → ((a : α) → β a → m PUnit.{w + 1}) → Std.DHashMap α β → m PUnit.{w + 1}
-- Mathlib.LinearAlgebra.Semisimple
LinearEquiv.isSemisimple_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  {M₂ : Type u_3} [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (g : Module.End R M₂) (e : M ≃ₗ[R] M₂),
  ↑e ∘ₗ f = g ∘ₗ ↑e → (f.IsSemisimple ↔ g.IsSemisimple)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- The sum over two finsupps agree if the functions agree and are well-behaved within the
shared support.  -/
Finsupp.sum_congr_of_eq_on_union : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : DecidableEq α]
  {f1 f2 : α →₀ M} {g1 g2 : α → M → N},
  (∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)) →
    (∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 0) → (∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 0) → f1.sum g1 = f2.sum g2
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) (U : C),
  (CategoryTheory.Subfunctor.equalizer f g).obj U =
    {x |
      ∃ (hx : x ∈ A.obj U),
        (CategoryTheory.ConcreteCategory.hom (f.app U)) ⟨x, hx⟩ =
          (CategoryTheory.ConcreteCategory.hom (g.app U)) ⟨x, hx⟩}
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.checkFunInfoCache : Lean.Expr → Option ℕ → Lean.MetaM Lean.Meta.FunInfo → Lean.MetaM Lean.Meta.FunInfo
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_minKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β}, cmp (Std.DTreeMap.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_zero_le : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.cpopNatRec n 0 ≤ w
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D),
  F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
    (((self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso self.εIso.symm (CategoryTheory.Iso.refl (F.obj X))) ≪≫
        CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.is_empty : ∀ {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β], IsEmpty (α ↪ β)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommSemiringOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → CommSemiring (DirectLimit G f)
-- Mathlib.Data.Finset.Prod
Finset.inter_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t : Finset β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_comp_reindex_symm : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E]
  [inst_4 : Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R s E),
  PiTensorProduct.lift φ ∘ₗ ↑(PiTensorProduct.reindex R s e).symm =
    PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    CategoryTheory.Mono
        (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
          CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
      CategoryTheory.Mono
          (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2) →
        CategoryTheory.Mono
            (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
          CategoryTheory.Mono
            (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] [IsManifold I ⊤ M],
  ContMDiffVectorBundle ⊤ E (TangentSpace I) I
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filterM : ∀ {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.filterM f it) =
    Std.Iter.foldM
      (fun d b => do
        let __do_lift ← f b
        pure (if __do_lift.down = true then g d b else d))
      init it
-- Init.Prelude
/-- Encode a list of characters (Unicode scalar value) in UTF-8. This is an inefficient model
implementation. Use `List.asString` instead.  -/
List.utf8Encode : List Char → ByteArray
-- Mathlib.Topology.Algebra.Order.Field
inv_atBot₀ : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.atBot⁻¹ = nhdsWithin 0 (Set.Iio 0)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Construct a strong natural transformation from a lax natural transformation whose
naturality 2-morphism is an isomorphism.  -/
CategoryTheory.Lax.StrongTrans.mkOfLax' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : CategoryTheory.Lax.LaxTrans F G) →
            [∀ (a b : B) (f : a ⟶ b), CategoryTheory.IsIso (η.naturality f)] → CategoryTheory.Lax.StrongTrans F G
-- Mathlib.Algebra.Quaternion
Quaternion.re_add_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), ↑a.re + a.im = a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMonC_nc_go : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p acc) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p +
      Lean.Grind.CommRing.Poly.denote ctx acc
-- Mathlib.Algebra.Module.Presentation.Tensor
_private.Mathlib.Algebra.Module.Presentation.Tensor.0.Module.Relations.tensor.match_1.eq_2 : ∀ {A : Type u_5} [inst : CommRing A] (relations₁ : Module.Relations A) (relations₂ : Module.Relations A)
  (motive : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R → Sort u_6) (g₁ : relations₁.G)
  (r₂ : relations₂.R) (h_1 : (r₁ : relations₁.R) → (g₂ : relations₂.G) → motive (Sum.inl (r₁, g₂)))
  (h_2 : (g₁ : relations₁.G) → (r₂ : relations₂.R) → motive (Sum.inr (g₁, r₂))),
  (match Sum.inr (g₁, r₂) with
    | Sum.inl (r₁, g₂) => h_1 r₁ g₂
    | Sum.inr (g₁, r₂) => h_2 g₁ r₂) =
    h_2 g₁ r₂
-- Batteries.Data.List.Lemmas
List.idxsOf_eq_filterMap_zipIdx : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α],
  List.idxsOf x xs s = List.filterMap (fun ab => bif ab.1 == x then some ab.2 else none) (xs.zipIdx s)
-- Lean.Message
/-- Maximum number of trace node children to display by default to prevent slowdowns from rendering. In
the info view, more children can be expanded interactively.
 -/
Lean.MessageData.maxTraceChildren : Lean.Option ℕ
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.commMonoid.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : CommMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.commMonoid = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instIsGroupoidLocalizationTopMorphismProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], CategoryTheory.IsGroupoid ⊤.Localization
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra : (C : Type u) →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → CompleteBooleanAlgebra (CategoryTheory.MorphismProperty C)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The trivial subgroup `{1}` of a group `G`.  -/
Subgroup.instBot : {G : Type u_1} → [inst : Group G] → Bot (Subgroup G)
-- Mathlib.Topology.Instances.CantorSet
ofDigits_bool_to_fin_three_mem_cantorSet : ∀ (f : ℕ → Bool), (Real.ofDigits fun i => bif f i then 2 else 0) ∈ cantorSet
-- Init.Data.Fin.Lemmas
Fin.le_refl : ∀ {n : ℕ} (a : Fin n), a ≤ a
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Abelian C} {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀}
  {hom : (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯}
  {comm :
    autoParam
      (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
        (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
          CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom r' ⋯).f pq))
      CategoryTheory.SpectralSequence.Hom.comm._autoParam}
  {hom_1 : (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯}
  {comm_1 :
    autoParam
      (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
        (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom_1 r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
          CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom_1 r' ⋯).f pq))
      CategoryTheory.SpectralSequence.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.lt_ord_succ_card : ∀ (o : Ordinal.{u_1}), o < (Order.succ o.card).ord
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_abs : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β), ⇑|f| = |⇑f|
-- Batteries.Data.String.Lemmas
String.utf8Len_cons : ∀ (c : Char) (cs : List Char), String.utf8Len (c :: cs) = String.utf8Len cs + c.utf8Size
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R], ↑0 = 0
-- Mathlib.Analysis.Normed.MulAction
norm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  (Std.DTreeMap.Const.modify t k f).maxKey he = if cmp (t.maxKey ⋯) k = Ordering.eq then k else t.maxKey ⋯
-- Mathlib.Topology.Irreducible
/-- In a preirreducible space, `Set.univ` is a preirreducible set.  -/
PreirreducibleSpace.isPreirreducible_univ : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : PreirreducibleSpace X], IsPreirreducible Set.univ
-- Aesop.Search.Expansion.Norm
Aesop.updateForwardState : Lean.MVarId → Aesop.NormM Unit
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.symm : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → G.IsPathGraph3Compl v w₂ w₁
-- Init.Data.SInt.Lemmas
Int8.ofInt_tdiv : ∀ {a b : ℤ},
  Int8.minValue.toInt ≤ a →
    a ≤ Int8.maxValue.toInt →
      Int8.minValue.toInt ≤ b → b ≤ Int8.maxValue.toInt → Int8.ofInt (a.tdiv b) = Int8.ofInt a / Int8.ofInt b
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_sub : ∀ {A : Type u_1} {G : Type u_2} [inst : Semiring A] [inst_1 : Monoid G] {V : Type u_6} {W : Type u_7}
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommGroup W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_smul : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (r : R) (P : MvPolynomial σ R), (MvPolynomial.eval₂Hom f g) (r • P) = f r • (MvPolynomial.eval₂Hom f g) P
-- Mathlib.Order.Heyting.Hom
CoheytingHomClass.toBoundedLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CoheytingAlgebra α]
  {x : CoheytingAlgebra β} [CoheytingHomClass F α β], BoundedLatticeHomClass F α β
-- Mathlib.Algebra.DirectSum.Internal
Submodule.setLike.coe_galgebra_toFun : ∀ {S : Type u_3} {R : Type u_4} {ι : Type u_5} [inst : AddMonoid ι] [inst_1 : CommSemiring S] [inst_2 : Semiring R]
  [inst_3 : Algebra S R] (A : ι → Submodule S R) [inst_4 : SetLike.GradedMonoid A] (s : S),
  ↑(DirectSum.GAlgebra.toFun s) = (algebraMap S R) s
-- Mathlib.Algebra.Homology.ExactSequence
/-- `F : ComposableArrows C n` is exact if it is a complex and that all short
complexes consisting of two consecutive arrows are exact.  -/
CategoryTheory.ComposableArrows.Exact : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → Prop
-- Mathlib.Data.Finsupp.Order
Finsupp.sub_single_one_add : ∀ {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ}, u a ≠ 0 → (u - fun₀ | a => 1) + u' = u + u' - fun₀ | a => 1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_eq : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [hl : Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)},
  forIn' it init f =
    Std.IterM.DefaultConsumers.forIn' (fun x x_1 f x_2 => f x_2.run) γ (fun x x_1 x_2 => True) it.toIterM init
      it.toIterM.IsPlausibleIndirectOutput ⋯ fun out h acc => do
      let __do_lift ← f out ⋯ acc
      pure ⟨__do_lift, trivial⟩
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.support_closure_subset_union : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (S : Set (Equiv.Perm α)),
  ∀ a ∈ Subgroup.closure S, ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Iio_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderBot α]
  (a : Subtype p), Finset.Iio a = Finset.subtype p (Finset.Iio ↑a)
-- Init.Data.Vector.Algebra
Vector.zero_add : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α], (∀ (x : α), 0 + x = x) → ∀ (xs : Vector α n), 0 + xs = xs