mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The cardinality of the ambient space is the product of the cardinality of a block
by the cardinality of the set of translates of that block  -/
AddAction.IsBlock.ncard_block_add_ncard_orbit_eq : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  {B : Set X}, AddAction.IsBlock G B → B.Nonempty → B.ncard * (AddAction.orbit G B).ncard = Nat.card X
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_some : ∀ {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι),
  (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.obj (some i) = some (e i)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquivOverMapIso_inv_app_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (p : f ⟶ g)
  (X_1 : CategoryTheory.Over f),
  ((CategoryTheory.Over.iteratedSliceEquivOverMapIso p).inv.app X_1).left.left =
    CategoryTheory.CategoryStruct.id X_1.left.left
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.isoMk.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Over Q X} (f f_1 : A.left ≅ B.left) (e_f : f = f_1)
  (w : CategoryTheory.CategoryStruct.comp f.hom B.hom = A.hom),
  CategoryTheory.MorphismProperty.Over.isoMk f w = CategoryTheory.MorphismProperty.Over.isoMk f_1 ⋯
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.getThenInsertIfNew? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α} {b : β},
  t.WF → (t.getThenInsertIfNew? a b).2.WF
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
  [inst_2 : Fintype n] [inst_3 : Fintype m] [inst_4 : DecidableEq m] (M : Matrix l m R) (N : Matrix m n R),
  Matrix.toLin' (M * N) = Matrix.toLin' M ∘ₗ Matrix.toLin' N
-- Mathlib.Order.CompleteLattice.Basic
iSup_congr_Prop : ∀ {α : Type u_1} [inst : SupSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q),
  (∀ (x : q), f₁ ⋯ = f₂ x) → iSup f₁ = iSup f₂
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.neg_mem_neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s : NonemptyInterval α), ∀ a ∈ s, -a ∈ -s
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_one_right : ∀ (p : ℕ), padicValNat p 1 = 0
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.bot_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] {x : CompleteLattice β} (a : α), ⊥ a = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path of length `n` in a 1-truncated simplicial set `X` is a directed path
of `n` edges.  -/
SSet.Truncated.Path₁ : SSet.Truncated 1 → ℕ → Type u
-- Mathlib.Algebra.Category.BoolRing
boolRingCatEquivBoolAlg_inverse : boolRingCatEquivBoolAlg.inverse = CategoryTheory.forget₂ BoolAlg BoolRing
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare} {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅}, compare ((t.modify k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.Control.Functor
Functor.Comp.map.eq_1 : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] {α β : Type v} (h : α → β)
  (x : Functor.Comp F G α), Functor.Comp.map h x = Functor.Comp.mk ((fun x => h <$> x) <$> x)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_union : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → ENNReal},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      ⨍⁻ (x : α) in s ∪ t, f x ∂μ =
        μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_compl_self : ∀ {α : Type u_1} (s : Set α), s ∪ sᶜ = Set.univ
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.mk.inj : ∀ {obj : Dynamic} {id : USize} {rc : ℕ} {obj_1 : Dynamic} {id_1 : USize} {rc_1 : ℕ},
  { obj := obj, id := id, rc := rc } = { obj := obj_1, id := id_1, rc := rc_1 } → obj = obj_1 ∧ id = id_1 ∧ rc = rc_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.not_isDiag_of_mem_edgeFinset : ∀ {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [inst : Fintype ↑G.edgeSet], e ∈ G.edgeFinset → ¬e.IsDiag
-- Lean.Declaration
Lean.ConstantInfo.inductInfo.injEq : ∀ (val val_1 : Lean.InductiveVal),
  (Lean.ConstantInfo.inductInfo val = Lean.ConstantInfo.inductInfo val_1) = (val = val_1)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.integral_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ∀ (t : NNReal), ∫ (x : Ω), B t x ∂P = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b c : α},
  1 < a → b ≤ c → b < a * c
-- Mathlib.Topology.Sets.Compacts
/-- The opens neighbourhood of a compact subset that are relatively compact  -/
TopologicalSpace.Compacts.openRcNhds : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.Compacts α → Set (TopologicalSpace.Opens α)
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.sigmaCongrRight_symm : ∀ {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Equiv.Perm (β a)),
  Equiv.symm (Equiv.Perm.sigmaCongrRight F) = Equiv.Perm.sigmaCongrRight fun a => Equiv.symm (F a)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.neg : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproducts.mk : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (P Q : C), CategoryTheory.Limits.HasBinaryBiproduct P Q) → CategoryTheory.Limits.HasBinaryBiproducts C
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `simp`-normal form of `invFun_eq_symm`.  -/
MulEquiv.coe_toEquiv_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), ⇑(↑f).symm = ⇑f.symm
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (h : U = V)
  (W : (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op V))).Opens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op)) W =
    CategoryTheory.eqToHom ⋯
-- Init.Data.UInt.Lemmas
UInt16.neg_add_mul_eq_mul_not : ∀ {a b : UInt16}, -(a + a * b) = a * ~~~b
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsOrderedOrder : FirstOrder.Language.order.IsOrdered
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, a ∉ t → Std.DTreeMap.Const.get! t a = default
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
AEMeasurable.singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x : MeasurableSpace β}
  {f : α → β}, AEMeasurable f μ → ∀ (ν : MeasureTheory.Measure α), AEMeasurable f (μ.singularPart ν)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ), CategoryTheory.Epi (f.app X)
-- Init.Data.Nat.Basic
Nat.add_sub_assoc : ∀ {m k : ℕ}, k ≤ m → ∀ (n : ℕ), n + m - k = n + (m - k)
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_dvd_finrank_top_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A ≤ B → A.relfinrank B ∣ Module.finrank (↥A) E
-- Lean.Environment
/-- Kernel WHNF function. We use it mainly for debugging purposes.
Recall that the kernel type checker does not support metavariables.
When implementing automation, consider using the `MetaM` methods.  -/
Lean.Kernel.whnf : Lean.Environment → Lean.LocalContext → Lean.Expr → Except Lean.Kernel.Exception Lean.Expr
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.prod_X_sub_C_coeff_card_pred : ∀ {R : Type u} {ι : Type w} [inst : CommRing R] (s : Finset ι) (f : ι → R),
  0 < s.card → (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).coeff (s.card - 1) = -∑ i ∈ s, f i
-- Mathlib.Algebra.Lie.Matrix
Matrix.instLieModuleForall : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LieModule R (Matrix n n R) (n → R)
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.infty_mul : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NonUnitalNormedRing (B i)] {f g : (i : I) → B i},
  Memℓp f ⊤ → Memℓp g ⊤ → Memℓp (f * g) ⊤
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.lmarginalPartialTraj_mono : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a b : ℕ)
  {f g : ((n : ℕ) → X n) → ENNReal},
  f ≤ g →
    ∀ (x₀ : (n : ℕ) → X n),
      ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f x₀ ≤
        ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b g x₀
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_one_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.sphere 1 δ * {x} = Metric.sphere x δ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.ext.injEq : ∀ (ext₁? : Option Lean.Meta.SimpExtension) (ext₂? : Option Lean.Meta.Simp.SimprocExtension)
  (h : (ext₁?.isSome || ext₂?.isSome) = true) (ext₁?_1 : Option Lean.Meta.SimpExtension)
  (ext₂?_1 : Option Lean.Meta.Simp.SimprocExtension) (h_1 : (ext₁?_1.isSome || ext₂?_1.isSome) = true),
  (Lean.Elab.Tactic.ElabSimpArgResult.ext ext₁? ext₂? h = Lean.Elab.Tactic.ElabSimpArgResult.ext ext₁?_1 ext₂?_1 h_1) =
    (ext₁? = ext₁?_1 ∧ ext₂? = ext₂?_1)
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.coeff_derivative : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.coeff n) ((PowerSeries.derivative R) f) = (PowerSeries.coeff (n + 1)) f * (↑n + 1)
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_lt_iff_lt : ∀ {a b : ℤ} (ha₁ : Int16.minValue.toInt ≤ a) (ha₂ : a ≤ Int16.maxValue.toInt) (hb₁ : Int16.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int16.maxValue.toInt), Int16.ofIntLE a ha₁ ha₂ < Int16.ofIntLE b hb₁ hb₂ ↔ a < b
-- Mathlib.CategoryTheory.Yoneda
/-- The Coyoneda lemma asserts that the Coyoneda pairing
`(X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F)`
is naturally isomorphic to the evaluation `(X, F) ↦ F.obj X`.  -/
CategoryTheory.coyonedaLemma : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.coyonedaPairing C ≅ CategoryTheory.coyonedaEvaluation C
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, Std.ExtDTreeMap.Const.get? t k = some v ↔ ∃ (h : k ∈ t), Std.ExtDTreeMap.Const.get t k h = v
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : β a → β a},
      (Std.DHashMap.Internal.toListModel (↑(m.modify a f)).buckets).Perm
        (Std.Internal.List.modifyKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Init.Control.StateCps
StateCpsT.instMonadStateOf : {σ : Type u} → {m : Type u → Type v} → MonadStateOf σ (StateCpsT σ m)
-- Lean.Elab.MutualInductive
/-- Converts universe metavariables in the type (not the constructors) into new parameters.
The additional level parameters in `typeLMVarIds` can be promoted to level metavariables
if they appear among the constructors.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.levelMVarToParamAtInductives : List Lean.InductiveType → Array Lean.LMVarId → Lean.Elab.Command.ResultingUniverseResult✝ → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_right_convexCombPair : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist y (Convexity.convexCombPair s t hs ht h x y) = s * dist x y
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- This lemma is a special case of `Integrable.of_finite`.  -/
MeasureTheory.Integrable.of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [Subsingleton α] [MeasureTheory.IsFiniteMeasure μ] {f : α → β}, MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.monObjMkPullbackSnd_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [inst_2 : CategoryTheory.MonObj (CategoryTheory.Over.mk f)],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback g))
      ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.one)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx!.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (x size : ℕ) (k : α) (v : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx! (Std.DTreeMap.Internal.Impl.inner size k v l r) x =
    match compare x l.size with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx! l x
    | Ordering.eq => (k, v)
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx! r (x - l.size - 1)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.fold.eq_1 : ∀ {α : Type u} {β : Type v} (s : Stream'.Seq α) (init : β) (f : β → α → β),
  s.fold init f =
    Stream'.Seq.cons init
      (Stream'.Seq.corec
        (fun x =>
          match x with
          | (acc, x) =>
            match x.destruct with
            | none => none
            | some (x, s) => some (f acc x, f acc x, s))
        (init, s))
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_scalar : ∀ (u : ℝˣ) (z : UpperHalfPlane), UpperHalfPlane.denom ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) ↑z = ↑↑u
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushOption.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Data.PNat.Factors
PNat.Prime.eq_1 : ∀ (p : ℕ+), p.Prime = Nat.Prime ↑p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiable_sin : Differentiable ℝ Real.sin
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.alterKey_nil : ∀ {α : Type u} [inst : BEq α] {β : Type v} {a : α} {f : Option β → Option β},
  Std.Internal.List.Const.alterKey a f [] =
    match f none with
    | none => []
    | some b => [⟨a, b⟩]
-- Mathlib.Data.Nat.Log
Nat.log_mono : ∀ {b c m n : ℕ}, 1 < c → c ≤ b → m ≤ n → Nat.log b m ≤ Nat.log c n
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf_principal : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (s' : Set α), (l ⊓ Filter.principal s').HasBasis p fun i => s i ∩ s'
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- If `x : R` is multiplicative for `f`, then it is multiplicative for
`seminormFromConst' c f`.  -/
seminormFromConst_isMul_of_isMul : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 →
    f c ≠ 0 →
      IsPowMul ⇑f →
        ∀ {x : R},
          (∀ (y : R), f (x * y) = f x * f y) →
            ∀ (y : R), seminormFromConst' c f (x * y) = seminormFromConst' c f x * seminormFromConst' c f y
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_iff : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsClique s ↔ s.Pairwise G.Adj
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂) {Z : HomotopicalAlgebra.CofibrantObject.HoCat C}
  (h :
    HomotopicalAlgebra.CofibrantObject.toHoCat.obj
        (HomotopicalAlgebra.CofibrantObject.mk X₂.bifibrantResolutionObj.obj) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map X₁.iBifibrantResolutionObj)
      (CategoryTheory.CategoryStruct.comp
        (HomotopicalAlgebra.CofibrantObject.toHoCat.map
          (HomotopicalAlgebra.CofibrantObject.homMk (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f).hom))
        h) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map X₂.iBifibrantResolutionObj) h)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.rcoIterator : {α : Type u_1} → {β : α → Type u_2} → [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → α → α → Std.Iter ((a : α) × β a)
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.OreLocalization.smul'.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r₁ : R) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S),
  OreLocalization.smul'✝ r₁ s₁ r₂ s₂ = OreLocalization.oreNum r₁ s₂ • r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `sum_apply`. -/
ProbabilityTheory.Kernel.finsetSum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.continuousPrelocal_pred : ∀ (X : TopCat) (T : Type u_3) [inst : TopologicalSpace T] {x : TopologicalSpace.Opens ↑X} (f : ↥x → T),
  (X.continuousPrelocal T).pred f = Continuous f
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_roi : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.size xs - (lo + 1)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.le_def : ∀ {α : Type u_1} [inst : LE α] {s t : NonemptyInterval α}, s ≤ t ↔ t.toProd.1 ≤ s.toProd.1 ∧ s.toProd.2 ≤ t.toProd.2
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.η_whiskerRight_commutator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one G)
      (CategoryTheory.GrpObj.commutator G) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G))
      CategoryTheory.MonObj.one
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_lt_one : ∀ {α : Type u} [inst : One α] [inst_1 : LT α], ⊥ < 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_erase!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.erase! k t) k = default
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.ne_zero : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R}, p.Monic → p ≠ 0
-- Mathlib.Data.Finset.Prod
/-- Given a finite set `s`, the off-diagonal, `s.offDiag` is the set of pairs `(a, b)` with `a ≠ b`
for `a, b ∈ s`.  -/
Finset.offDiag : {α : Type u_1} → Finset α → Finset (α × α)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.step_iterM_cons : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {x : β} {xs : List β},
  ((x :: xs).iterM m).step = pure (Std.Shrink.deflate ⟨Std.IterStep.yield (xs.iterM m) x, ⋯⟩)
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.uncenteredCovarianceBilinDual_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : OpensMeasurableSpace E], ProbabilityTheory.uncenteredCovarianceBilinDual 0 = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- The zero locus of a set `s` of elements of a commutative ring `A` is the set of all relevant
homogeneous prime ideals of the ring that contain the set `s`.

An element `f` of `A` can be thought of as a dependent function on the projective spectrum of `𝒜`.
At a point `x` (a homogeneous prime ideal) the function (i.e., element) `f` takes values in the
quotient ring `A` modulo the prime ideal `x`. In this manner, `zeroLocus s` is exactly the subset
of `ProjectiveSpectrum 𝒜` where all "functions" in `s` vanish simultaneously.  -/
ProjectiveSpectrum.zeroLocus : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] → (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → Set A → Set (ProjectiveSpectrum 𝒜)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_eq_zero_iff : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ), A.num = 0 ↔ A = 0
-- Mathlib.Data.Matrix.Mul
Matrix.dot_mulVec_eq_sum_sum : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : NonUnitalSemiring R]
  (v : m → R) (A : Matrix m n R) (w : n → R), v ⬝ᵥ A.mulVec w = ∑ j, ∑ i, v i * A i j * w j
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If `B / S / R` is a tower of ring extensions where `S` is integral over `R`,
then `S` maps (uniquely) into an integral closure `B / A / R`.  -/
IsIntegralClosure.lift : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R B] →
              [inst_4 : Algebra A B] →
                [IsIntegralClosure A R B] →
                  {S : Type u_4} →
                    [inst_6 : CommRing S] →
                      [inst_7 : Algebra R S] →
                        [inst_8 : Algebra S B] →
                          [IsScalarTower R S B] →
                            [inst_10 : Algebra R A] →
                              [IsScalarTower R A B] → [isIntegral : Algebra.IsIntegral R S] → S →ₐ[R] A
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instHasDistribNeg : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → HasDistribNeg ↑(Metric.ball 0 1)
-- Mathlib.RepresentationTheory.Basic
Representation.ofModule.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] (M : Type u_4) [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra k G) M],
  Representation.ofModule M =
    (MonoidAlgebra.lift k (RestrictScalars k (MonoidAlgebra k G) M →ₗ[k] RestrictScalars k (MonoidAlgebra k G) M)
          G).symm
      (RestrictScalars.lsmul k (MonoidAlgebra k G) M)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- In the case of a discrete category, `WithTerminal` is the same category as `WidePullbackShape`

TODO: Should we simply replace `WidePullbackShape J` with `WithTerminal (Discrete J)` everywhere?  -/
CategoryTheory.WithTerminal.widePullbackShapeEquiv : {J : Type u_1} → CategoryTheory.Limits.WidePullbackShape J ≌ CategoryTheory.WithTerminal (CategoryTheory.Discrete J)