mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Rotate
List.isRotated_reverse_iff : ∀ {α : Type u} {l l' : List α}, l.reverse ~r l'.reverse ↔ l ~r l'
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_iff : ∀ (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p], ↑n = z ↔ ∃ k, n = ↑z.val + ↑p * k
-- Init.Data.Vector.Attach
Vector.pmap_append' : ∀ {α : Type u_1} {β : Type u_2} {n m : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {ys : Vector α m}
  (h₁ : ∀ a ∈ xs, p a) (h₂ : ∀ a ∈ ys, p a), Vector.pmap f (xs ++ ys) ⋯ = Vector.pmap f xs h₁ ++ Vector.pmap f ys h₂
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instFaithfulIndYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.Ind.yoneda.Faithful
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.inv_liminf : ∀ {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι}, (Filter.liminf x l)⁻¹ = Filter.limsup (fun i => (x i)⁻¹) l
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.image_coe_edgeSet_coe : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h) I.subschemeι = J.subschemeι
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, (m.insertMany l).contains k = (m.contains k || l.contains k)
-- Mathlib.RingTheory.Smooth.Kaehler
sectionOfRetractionKerToTensor.congr_simp : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l l_1 : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (e_l : l = l_1) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥)
  (hf : Function.Surjective ⇑(algebraMap P S)),
  sectionOfRetractionKerToTensor l hl hf' hf = sectionOfRetractionKerToTensor l_1 ⋯ hf' hf
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- To show a property is true on the even parts, it suffices to show it is true on the
scalars, closed under addition, and under left-multiplication by a pair of vectors.  -/
CliffordAlgebra.even_induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 0 → Prop},
  (∀ (r : R), motive ((algebraMap R (CliffordAlgebra Q)) r) ⋯) →
    (∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0) (hy : y ∈ CliffordAlgebra.evenOdd Q 0),
        motive x hx → motive y hy → motive (x + y) ⋯) →
      (∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0),
          motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
        ∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0), motive x hx
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] (q : X ⟶ X)
  (w :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp q f),
  CategoryTheory.Limits.cokernel.map f f q (CategoryTheory.CategoryStruct.id Y) w =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.cokernel f)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instLTOffset : LT Std.Time.Week.Offset
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isMaximal_iff : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α},
  I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.addPolynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x y ℓ : R),
  W'.addPolynomial x y ℓ = Polynomial.eval (WeierstrassCurve.Affine.linePolynomial x y ℓ) W'.polynomial
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.con_ker_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Con.ker Monoid.Coprod.mk = Monoid.coprodCon M N
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_comp_id_right_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {l' : a ⟶ b} {r' : b ⟶ a}
  (adj' : CategoryTheory.Bicategory.Adjunction l' r') (φ : l' ⟶ l),
  (CategoryTheory.Bicategory.conjugateEquiv adj (adj'.comp (CategoryTheory.Bicategory.Adjunction.id b)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor l').hom φ) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj adj') φ)
      (CategoryTheory.Bicategory.leftUnitor r').inv
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The standard simplex identifies to the nerve to the preordered type
`ULift (Fin (n + 1))`.  -/
SSet.stdSimplex.isoNerve : (n : ℕ) → SSet.stdSimplex.obj { len := n } ≅ CategoryTheory.nerve (ULift.{u, 0} (Fin (n + 1)))
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- If `A : Subcomplex X`, this is the inclusion `A ⟶ X` in the category `SSet`.  -/
SSet.Subcomplex.ι : {X : SSet} → (A : X.Subcomplex) → A.toSSet ⟶ X
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_subset_nsmul_right : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} {m n : ℕ}, 0 ∈ s → m ≤ n → m • s ⊆ n • s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg_of_nonpos_of_neg`.  -/
Right.add_neg_of_nonpos_of_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, a ≤ 0 → b < 0 → a + b < 0
-- Mathlib.Analysis.Convex.Combination
convexHull_range_eq_exists_affineCombination : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (v : ι → E),
  (convexHull R) (Set.range v) = {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (Finset.affineCombination R s v) w = x}
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_single : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) (r : k) (x y : G),
  (f * SkewMonoidAlgebra.single x r).coeff y = f.coeff (y * x⁻¹) * (y * x⁻¹) • r
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle.eq_1 : ∀ {T : ℝ}, AddCircle.toCircle = ⋯.lift
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_ext_iff : ∀ {M N : MonCat} {f g : M ⟶ N}, f = g ↔ MonCat.Hom.hom f = MonCat.Hom.hom g
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOfVector_over : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector f v)
      (AlgebraicGeometry.AffineSpace n S ↘ S) =
    f
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_right' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Ici ↑n)) (nhds ↑n)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.prodMk : ∀ {α : Type u} {β : Type v} {γ : Type w} {l : Filter α} {f f' : α → β},
  f =ᶠ[l] f' → ∀ {g g' : α → γ}, g =ᶠ[l] g' → (fun x => (f x, g x)) =ᶠ[l] fun x => (f' x, g' x)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- `MvPolynomial.rename` induces an isomorphism between the symmetric subalgebras.  -/
MvPolynomial.renameSymmetricSubalgebra : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_3} →
      [inst : CommSemiring R] →
        σ ≃ τ → ↥(MvPolynomial.symmetricSubalgebra σ R) ≃ₐ[R] ↥(MvPolynomial.symmetricSubalgebra τ R)
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_empty_of_ne_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {n : μ}, n ≠ 0 → ∅.piAntidiag n = ∅
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_mono_of_forall_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {ι' : Sort u_5} [Nonempty ι'] {f : ι → α}
  {g : ι' → α}, BddBelow (Set.range f) → (∀ (i' : ι'), ∃ i, f i ≤ g i') → ⨅ i, f i ≤ ⨅ i', g i'
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listDecode_encode_list : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List (L.Term α)),
  FirstOrder.Language.Term.listDecode (List.flatMap FirstOrder.Language.Term.listEncode l) = l
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.coe_neg : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : NegZeroClass N] (f : ZeroHom M N), ⇑(-f) = -⇑f
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeffAddEquiv`.

---

Group isomorphism between `SkewMonoidAlgebra k G` and `G →₀ k`.  -/
SkewMonoidAlgebra.toFinsuppAddEquiv : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → SkewMonoidAlgebra k G ≃+ (G →₀ k)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A divisor `d` of `n` belongs to the conductor set of `χ` if and only if the conductor of `χ`
divides `d`.  -/
DirichletCharacter.mem_conductorSet_iff_conductor_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} [NeZero n],
  d ∣ n → (d ∈ χ.conductorSet ↔ χ.conductor ∣ d)
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.fromCompletion_apply_coe : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f : α →SL[σ] β) (e : α), f.fromCompletion ↑e = f e
-- Batteries.Logic
Function.id_def : ∀ {α : Sort u_1}, id = fun x => x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_toSheafedSpace : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.LocallyRingedSpace)
  (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f).toSheafedSpace =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y.toSheafedSpace f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k a : α} {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Mathlib.Computability.RegularExpressions
/-- Map the alphabet of a regular expression.  -/
RegularExpression.map : {α : Type u_1} → {β : Type u_2} → (α → β) → RegularExpression α → RegularExpression β
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.card_inter_lt_of_cliqueFree : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.CliqueFree (r + 2) → k < r
-- Init.Data.String.PosRaw
String.Pos.Raw.le_iff : ∀ {i₁ i₂ : String.Pos.Raw}, i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The left homotopy in the opposite category that is deduced from a right homotopy.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {P : HomotopicalAlgebra.PrepathObject Y} → {f g : X ⟶ Y} → P.RightHomotopy f g → P.op.LeftHomotopy f.op g.op
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.mk.inj : ∀ {origin : Lean.Meta.Grind.Origin} {proof : Lean.Expr} {origin_1 : Lean.Meta.Grind.Origin} {proof_1 : Lean.Expr},
  { origin := origin, proof := proof } = { origin := origin_1, proof := proof_1 } → origin = origin_1 ∧ proof = proof_1
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.continuousOn_const_smul_iff : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] [inst_4 : TopologicalSpace β] {f : β → α} {c : M} {s : Set β},
  IsUnit c → (ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s)
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_left_pure_sub_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto Int.floor (nhdsWithin (↑n) (Set.Iio ↑n)) (pure (n - 1))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_subset_pow_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α} {n : ℕ}, s ⊆ t → s ^ n ⊆ t ^ n
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturalityᵣ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n n' : M}
  (g : n ⟶ n') (X : C) [inst_3 : F.LaxMonoidal] {Z : C}
  (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n')).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n').app X) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m g)).app X) h)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n),
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
      (CochainComplex.mappingCone.descCochain φ α β h) ⋯ =
    β
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.Exact.isIso_imageToKernel' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact → CategoryTheory.IsIso (imageToKernel' S.f S.g ⋯)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).inv =
    CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `AddMonoidAlgebra.mem_span_support_coeff`.

---

An element of `k[G]` is in the submodule generated by its support.  -/
AddMonoidAlgebra.mem_span_support : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (f : AddMonoidAlgebra k G),
  f ∈ Submodule.span k (AddMonoidAlgebra.of' k G '' ↑f.coeff.support)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSubNegAddMonoid : {α : Type u_1} → [SubNegMonoid α] → SubNegMonoid (Lex α)
-- Mathlib.Order.Cover
wcovBy_of_le_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → b ≤ a → a ⩿ b
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  [inst_3 : HasDerivedCategory C]
  (x : CochainComplex.HomComplex.Cocycle ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n),
  (R.extEquivCohomologyClass.symm (CochainComplex.HomComplex.CohomologyClass.mk x)).hom =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((CategoryTheory.ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (DerivedCategory.Q.map R.ι'))
            ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)))
        ⋯)
      ⋯
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.prodToProdTop_obj : ∀ (A : TopCat) (B : TopCat)
  (g :
    ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) × ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)),
  (FundamentalGroupoidFunctor.prodToProdTop A B).obj g = { as := (g.1.as, g.2.as) }
-- Init.Data.Int.Order
Int.le_rfl : ∀ {a : ℤ}, a ≤ a
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of `isClosed_setOfPred_map_neg`. -/
isClosed_setOf_map_neg : ∀ (G₁ : Type u_2) (G₂ : Type u_3) [inst : TopologicalSpace G₂] [T2Space G₂] [inst_2 : Neg G₁] [inst_3 : Neg G₂]
  [ContinuousNeg G₂], IsClosed {f | ∀ (x : G₁), f (-x) = -f x}
-- Init.Data.Fin.Basic
Fin.val_neg' : ∀ {n : ℕ} (a : Fin n), ↑(-a) = (n - ↑a) % n
-- Mathlib.CategoryTheory.Localization.Quotient
/-- If `homRel : HomRel C` satisfies `homRel.FactorsThroughLocalization W` and
that the class of morphisms `W` induces a class of morphisms `W'` on the quotient category,
then `Quotient.functor homRel ⋙ W'.Q` satisfies the universal property of the
localization. This is used in `HomRel.FactorsThroughLocalization.isLocalizedEquivalence`
in order to show that as a localizer morphism, the quotient functor induces an
equivalence on localized categories.  -/
HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {homRel : HomRel C} →
      {W : CategoryTheory.MorphismProperty C} →
        homRel.FactorsThroughLocalization W →
          {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} →
            W = W'.inverseImage (CategoryTheory.Quotient.functor homRel) →
              (E : Type u_3) →
                [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
                  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget
                    ((CategoryTheory.Quotient.functor homRel).comp W'.Q) W E
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The Euler characteristic of a homological complex as a sum over all indices using `finsum`.
The sign at each index is determined by the `ComplexShape.EulerCharSigns` instance.
Defaults to 0 if the support of the ranks is infinite.  -/
HomologicalComplex.eulerChar : {R : Type u_1} →
  [inst : Ring R] → {ι : Type u_2} → {c : ComplexShape ι} → [c.EulerCharSigns] → HomologicalComplex (ModuleCat R) c → ℤ
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.imCLM_norm : ‖Complex.imCLM‖ = 1
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instModelLinearOrderTheoryOfDlo : ∀ (L : FirstOrder.Language) {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [h : M ⊨ L.dlo],
  M ⊨ L.linearOrderTheory
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_eq_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
-- Init.Data.SInt.Lemmas
Int16.lt_trans : ∀ {a b c : Int16}, a < b → b < c → a < c
-- Mathlib.Order.SupClosed
IsSublattice.supClosed : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice s → SupClosed s
-- Std.Time.DateTime.PlainDateTime
Std.Time.instOrdPlainDateTime : Ord Std.Time.PlainDateTime
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgBool : Lean.Doc.FromDocArg Bool
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.instInhabitedPrequotient : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → Inhabited (MonCat.Colimits.Prequotient F)
-- Mathlib.Tactic.Tauto
/-- Implementation of the `tauto` tactic.  -/
Mathlib.Tactic.Tauto.tautology : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppLanUnit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) (X : C)
  [L.HasPointwiseLeftKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  CategoryTheory.IsIso ((L.lanUnit.app F).app X)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`.  -/
MeasureTheory.integral_Ioi_deriv_mul_eq_sub : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a : ℝ} {a' b' : A} {u v u' v' : ℝ → A}
  [CompleteSpace A],
  (∀ x ∈ Set.Ioi a, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.Ioi a, HasDerivAt v (v' x) x) →
      MeasureTheory.IntegrableOn (u' * v + u * v') (Set.Ioi a) MeasureTheory.volume →
        Filter.Tendsto (u * v) (nhdsWithin a (Set.Ioi a)) (nhds a') →
          Filter.Tendsto (u * v) Filter.atTop (nhds b') → ∫ (x : ℝ) in Set.Ioi a, u' x * v x + u x * v' x = b' - a'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.eq_of_toPolyC_nc_eq : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (a b : Lean.Grind.CommRing.Expr),
  (a.toPolyC_nc c == b.toPolyC_nc c) = true →
    Lean.Grind.CommRing.Expr.denote ctx a = Lean.Grind.CommRing.Expr.denote ctx b
-- Mathlib.FieldTheory.Normal.Defs
IntermediateField.restrictScalars_normal : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {L : Type u_3}
  [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra K L] [inst_6 : IsScalarTower F K L]
  {E : IntermediateField K L}, Normal F ↥(IntermediateField.restrictScalars F E) ↔ Normal F ↥E
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- If `h : P ≤ P'`, then `ιOfLE h` is fully faithful.  -/
CategoryTheory.ObjectProperty.fullyFaithfulιOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P P' : CategoryTheory.ObjectProperty C} → (h : P ≤ P') → (CategoryTheory.ObjectProperty.ιOfLE h).FullyFaithful
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.commutatorMap_apply : ∀ {G : Type u_2} (φ : G → G) [inst : Div G] (g : G), MonoidHom.commutatorMap φ g = g / φ g
-- Mathlib.MeasureTheory.PiSystem
generateFrom_piiUnionInter_le : ∀ {α : Type u_3} {ι : Type u_4} {m : MeasurableSpace α} (π : ι → Set (Set α)),
  (∀ (n : ι), MeasurableSpace.generateFrom (π n) ≤ m) →
    ∀ (S : Set ι), MeasurableSpace.generateFrom (piiUnionInter π S) ≤ m
-- Mathlib.Data.Vector3
/-- Insert `a` into `v` at index `i`.  -/
Vector3.insert : {α : Type u_1} → {n : ℕ} → α → Vector3 α n → Fin2 (n + 1) → Vector3 α (n + 1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.or.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.or = 1