mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_10 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId)
  (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.del fvarId h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_10 fvarId h
-- Mathlib.Algebra.Star.Prod
Prod.instTrivialStar : ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] [TrivialStar R] [TrivialStar S], TrivialStar (R × S)
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The universe level associated with the `birdDet` call  -/
Mathlib.Tactic.Determinant.ReifiedBirdDet.u : Mathlib.Tactic.Determinant.ReifiedBirdDet → Lean.Level
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_X_self : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (i : σ),
  MvPolynomial.degreeOf i (MvPolynomial.X i) = 1
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_sSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P : Set (CategoryTheory.MorphismProperty C)),
  (sSup P).strictMap F = ⨆ P' ∈ P, P'.strictMap F
-- Mathlib.Data.Fintype.Option
Fintype.card_option : ∀ {α : Type u_3} [inst : Fintype α], Fintype.card (Option α) = Fintype.card α + 1
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inl_coprodIsoPushout_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  {Z : C} (h : X ⨿ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y))
      (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.mk : Lean.Syntax → Lean.Parser.ModuleParserState → Lean.Elab.Command.State → Lean.Server.Snapshots.Snapshot
-- Mathlib.RingTheory.Extension.Generators
/-- The polynomial ring w.r.t. a family of generators.  -/
Algebra.Generators.Ring : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S ι → Type (max w u)
-- Aesop.Nanos
Aesop.Nanos.instLT : LT Aesop.Nanos
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.uliftFunctor_obj : ∀ (X : GrpCat), GrpCat.uliftFunctor.obj X = GrpCat.of (ULift.{u, v} ↑X)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mem_pure : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ∈ NonemptyInterval.pure a ↔ b = a
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_meet_le_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop},
  (φ → Lean.Order.PartialOrder.rel Q R) →
    Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.CompleteLattice.ofProp φ) Q) R
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.tmul_right : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Bialgebra R A] [inst_3 : Semiring B] [inst_4 : Bialgebra R B] {a : A} {b : B}
  (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) (i : ι × κ),
  (ℛa.tmul ℛb).right i = ℛa.right i.1 ⊗ₜ[R] ℛb.right i.2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_union_le_size_add_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.generator_map_dvd_of_mem : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Module R M] {N : Submodule R M}
  (ϕ : M →ₗ[R] R) [inst_3 : (Submodule.map ϕ N).IsPrincipal] {x : M},
  x ∈ N → Submodule.IsPrincipal.generator (Submodule.map ϕ N) ∣ ϕ x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (M : CategoryTheory.Grp C) (X : Cᵒᵖ),
  Small.{w, v} ↑((CategoryTheory.yonedaGrp.obj M).obj X)
-- Mathlib.Algebra.Group.Center
Set.mem_addCenter_iff : ∀ {M : Type u_1} [inst : Add M] {z : M}, z ∈ Set.addCenter M ↔ IsAddCentral z
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
addOrderOf_eq_card_of_forall_mem_multiples : ∀ {α : Type u_1} [inst : AddGroup α] {g : α}, (∀ (x : α), x ∈ AddSubmonoid.multiples g) → addOrderOf g = Nat.card α
-- Mathlib.Logic.Basic
/-- A 'dite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `dite` that applies
either branch to `a`.  -/
dite_apply : ∀ {α : Sort u_1} {σ : α → Sort u_2} (P : Prop) [inst : Decidable P] (f : P → (a : α) → σ a) (g : ¬P → (a : α) → σ a)
  (a : α), dite P f g a = if h : P then f h a else g h a
-- Mathlib.Algebra.Free
FreeMagma.recOnPure.eq_1 : ∀ {α : Type u} {C : FreeMagma α → Sort l} (x : FreeMagma α) (ih1 : (x : α) → C (pure x))
  (ih2 : (x y : FreeMagma α) → C x → C y → C (x * y)), x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
-- Mathlib.Algebra.Ring.Basic
isLeftRegular_iff_right_eq_zero_of_mul : ∀ {R : Type u_3} [inst : NonUnitalNonAssocRing R] {r : R}, IsLeftRegular r ↔ ∀ (x : R), r * x = 0 → x = 0
-- Lean.Language.Basic
/-- Monad holding all relevant data for processing.  -/
Lean.Language.ProcessingM : Type → Type
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.ofAddDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddCommGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)),
  NormedAddCommGroup.ofAddDist h₁ h₂ =
    { toNorm := (NormedAddGroup.ofAddDist h₁ h₂).toNorm, toAddGroup := (NormedAddGroup.ofAddDist h₁ h₂).toAddGroup,
      add_comm := ⋯, toMetricSpace := (NormedAddGroup.ofAddDist h₁ h₂).toMetricSpace, dist_eq := ⋯ }
-- Lean.Util.LeanOptions
Lean.LeanOptions.mk : Lean.NameMap Lean.LeanOptionValue → Lean.LeanOptions
-- Mathlib.Data.Rel.Cover
/-- A maximal `U`-separated subset of a set `s` is a `U`-cover of `s`.

[R. Vershynin, *High Dimensional Probability*][vershynin2018high], 4.2.6.  -/
SetRel.IsCover.of_maximal_isSeparated : ∀ {X : Type u_1} {U : SetRel X X} {s N : Set X} [U.IsRefl] [U.IsSymm],
  Maximal (fun N => N ⊆ s ∧ U.IsSeparated N) N → U.IsCover s N
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushouts_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.pushouts
-- Lean.MetavarContext
Lean.instBEqLocalInstance : BEq Lean.LocalInstance
-- Mathlib.Data.List.Count
List.countP_lt_length_iff : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.countP p l < l.length ↔ ∃ a ∈ l, p a = false
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, k ∈ m.insert k v
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.isIso_of_to_star : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C}
  (f : X ⟶ CategoryTheory.WithInitial.star), CategoryTheory.IsIso f
-- Mathlib.MeasureTheory.Function.SimpleFunc
_private.Mathlib.MeasureTheory.Function.SimpleFunc.0.MeasureTheory.SimpleFunc.eapproxDiff.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.sum_adj_inr : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {w w' : W},
  (G ⊕g H).Adj (Sum.inr w) (Sum.inr w') ↔ H.Adj w w'
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Comon D)),
  CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝.obj F =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ico : ∀ {a b : ℝ}, 0 < a → a ≤ b → Real.log '' Set.Ico a b = Set.Ico (Real.log a) (Real.log b)
-- Mathlib.Data.Set.Subsingleton
/-- `s`, coerced to a type, is a nontrivial type if and only if `s` is a nontrivial set.  -/
Set.nontrivial_coe_sort : ∀ {α : Type u} {s : Set α}, Nontrivial ↑s ↔ s.Nontrivial
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [inst : IrreducibleSpace ↥X]
  [inst_1 : AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X} [inst_2 : X.IsGermInjectiveAt x]
  (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)
  (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).hom sY =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).domain.ι sX
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Comma.ext_iff : ∀ {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},
  x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `IsCentralVAdd` across an `Equiv`  -/
Equiv.isCentralVAdd : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : VAdd M β] [inst_1 : VAdd Mᵃᵒᵖ β] (e : α ≃ β) [IsCentralVAdd M β],
  IsCentralVAdd M α
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.mkHomFromSingle.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} (φ φ_1 : A ⟶ K.X j) (e_φ : φ = φ_1)
  (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0),
  HomologicalComplex.mkHomFromSingle φ hφ = HomologicalComplex.mkHomFromSingle φ_1 ⋯
-- Init.Data.BitVec.Lemmas
/-- Extracting all the bits of a bitvector is an identity operation.  -/
BitVec.extractLsb'_eq_self : ∀ {w : ℕ} {x : BitVec w}, BitVec.extractLsb' 0 w x = x
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`.  -/
Semiring.natCast_zero : ∀ {α : Type u} [self : Semiring α], ↑0 = 0
-- Mathlib.Analysis.Convex.Basic
/-- Alternative definition of set convexity, in terms of pointwise set operations.  -/
convex_iff_pointwise_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s
-- Init.Data.String.Lemmas.Splits
/-- We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
and `t₂`.
 -/
String.Slice.Pos.Splits : {s : String.Slice} → s.Pos → String → String → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
CategoryTheory.Iso.toIsometryEquiv_invFun : ∀ {R : Type u} [inst : CommRing R] {X Y : QuadraticModuleCat R} (i : X ≅ Y) (a : ↑Y.toModuleCat),
  i.toIsometryEquiv.invFun a = (QuadraticModuleCat.Hom.toIsometry i.inv) a
-- Std.Do.WP.SimpLemmas
Std.Do.WP.seq : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : m (α → β)) (x : m α) (Q : Std.Do.PostCond β ps),
  (Std.Do.wp (f <*> x)).apply Q = (Std.Do.wp f).apply (fun f => (Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2), Q.2)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instInhabitedQuotient : {R : Type u_1} → [Inhabited R] → [inst : Add R] → [inst_1 : Mul R] → (c : RingCon R) → Inhabited c.Quotient
-- Std.Internal.UV.UDP
/-- Sends data through an UDP socket. The `addr` parameter specifies the destination address. If `addr`
is `none`, the data is sent to the default peer address set by `connect`.
 -/
Std.Internal.UV.UDP.Socket.send : Std.Internal.UV.UDP.Socket → Array ByteArray → Option Std.Net.SocketAddress → IO (IO.Promise (Except IO.Error Unit))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.IsBimonHom.toIsComonHom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {M N : C} {inst_3 : CategoryTheory.BimonObj M}
  {inst_4 : CategoryTheory.BimonObj N} {f : M ⟶ N} [self : CategoryTheory.IsBimonHom f], CategoryTheory.IsComonHom f
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' : ∀ (f : ℝ ≃ᵐ ℝ) {s : Set ℝ},
  MeasurableSet s →
    ∀ {f' : ℝ → ℝ},
      (∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) →
        ∀ {g : ℝ → ℝ},
          0 ≤ᵐ[MeasureTheory.volume] g →
            MeasureTheory.Integrable g MeasureTheory.volume →
              (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s =
                ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.repGHSpaceMetricSpace : {p : GromovHausdorff.GHSpace} → MetricSpace p.Rep
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.iCycles_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], CategoryTheory.CategoryStruct.comp S.iCycles S.g = 0
-- Mathlib.Order.CompleteLattice.Basic
iInf_plift_up : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : PLift ι → α), ⨅ i, f { down := i } = ⨅ i, f i
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero if and only if
`m ∈ S`.  -/
QuotientGroup.norm_mk_eq_zero : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {m : M} [hS : IsClosed ↑S], ‖↑m‖ = 0 ↔ m ∈ S
-- Init.Data.Dyadic.Basic
Dyadic.instIsPreorder : Std.IsPreorder Dyadic
-- Mathlib.Data.Set.Image
/-- If the image of a set is nontrivial, the set is nontrivial.  -/
Set.nontrivial_of_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), (f '' s).Nontrivial → s.Nontrivial
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.symmDiff : ∀ {α : Type u} {s t : Set α}, s.Finite → t.Finite → (symmDiff s t).Finite
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_one : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ↑1 = 1
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorUnit_carrier : ∀ {R : Type u} [inst : CommSemiring R], ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R)) = R
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.coe_toAdditiveLeft : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (f : α →* Multiplicative β),
  ⇑(MonoidHom.toAdditiveLeft f) = ⇑Multiplicative.toAdd ∘ ⇑f ∘ ⇑Additive.toMul
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.exists_isClosed_of_not_isPreirreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PrespectralSpace X] (Z : Set X),
  ¬IsPreirreducible Z →
    ∃ A B, IsClosed A ∧ IsClosed B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  {n : ℕ} [inst_5 : HasDerivedCategory C]
  (a :
    CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
      ↑n),
  CategoryTheory.Abelian.Ext.homLinearEquiv.symm a = CategoryTheory.Abelian.Ext.homAddEquiv.invFun a
-- Mathlib.Order.PFilter
Order.PFilter.isPFilter : ∀ {P : Type u_1} [inst : Preorder P] (F : Order.PFilter P), Order.IsPFilter ↑F
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂)
  (i : m) (j : n), (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_iInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] {a : α} {f : ι → LowerSet α}, a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
-- Init.Data.Ord.Basic
List.compareLex : {α : Type u_1} → (α → α → Ordering) → List α → List α → Ordering
-- Mathlib.Tactic.GCongr.CoreAttrs
Mathlib.Tactic.GCongr.and_mono : ∀ {a b c d : Prop}, (a → c) → (a → b → d) → a ∧ b → c ∧ d
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_bind : ∀ {m : Type u → Type v} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n} {lift : ⦃α : Type u⦄ → m α → n α}
  [self : Std.Internal.LawfulMonadLiftFunction lift] {α β : Type u} (ma : m α) (f : α → m β),
  lift (ma >>= f) = do
    let x ← lift ma
    lift (f x)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_one : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  (TensorProduct.AlgebraTensorModule.lTensor A M) 1 = 1
-- Init.Data.Option.Basic
liftOption : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Alternative m] → Option α → m α
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
MulAlgebraNormClass.map_smul_eq_mul : ∀ {F : Type u_1} {R : outParam (Type u_2)} {inst : SeminormedCommRing R} {S : outParam (Type u_3)} {inst_1 : Ring S}
  {inst_2 : Algebra R S} {inst_3 : FunLike F S ℝ} [self : MulAlgebraNormClass F R S] (f : F) (a : R) (x : S),
  f (a • x) = ‖a‖ * f x
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `p` holds on some element of the tree.  -/
RBTree.RBNode.Any : {α : Type u_1} → (α → Prop) → RBTree.RBNode α → Prop
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddMonoidWithOne : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [AddMonoidWithOne Y] → AddMonoidWithOne (LocallyConstant X Y)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- A homothety with a nonzero scale factor preserves angles.  -/
EuclideanGeometry.angle_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p p₁ p₂ p₃ : P) {r : ℝ},
  r ≠ 0 →
    EuclideanGeometry.angle ((AffineMap.homothety p r) p₁) ((AffineMap.homothety p r) p₂)
        ((AffineMap.homothety p r) p₃) =
      EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.mk : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [toIsSimpleOrder : IsSimpleOrder (Submodule R M)], IsSimpleModule R M
-- Init.Data.Slice.Basic
Std.Slice.internalRepresentation : {γ : Type u} → Std.Slice γ → γ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_add_sum_filter_not : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p]
  [inst_2 : (x : ι) → Decidable ¬p x] (f : ι → M), ∑ x ∈ s with p x, f x + ∑ x ∈ s with ¬p x, f x = ∑ x ∈ s, f x
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {α : Type t} →
        {J : α → Type u'} →
          [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] →
            {motive : (a : C) → P.limitsClosure J a → Prop} → {a : C} → P.limitsClosure J a → Prop
-- Mathlib.Order.Filter.CardinalInter
CardinalInterFilter.mk : ∀ {α : Type u} {l : Filter α} {c : Cardinal.{u}},
  (∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l) → CardinalInterFilter l c
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.eq_1 : ∀ {α : Type u_1} {n : Type u_3} (A : Matrix n n α), A.IsSymm = (A.transpose = A)