mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- The canonical isomorphism between the domains of two Cartesian arrows
lying over the same object.  -/
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} →
            {a b : 𝒳} →
              (f : R ⟶ S) → (φ : a ⟶ b) → [p.IsCartesian f φ] → {a' : 𝒳} → (φ' : a' ⟶ b) → [p.IsCartesian f φ'] → a' ≅ a
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.unsat_of_encounteredBoth : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth →
    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) assignment
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₂_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) {i₂ i₂' : ι₂},
  c₂.Rel i₂ i₂' → ∀ (i₃ : ι₃) (j : ι₄), ⋯ = ⋯
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.mergeIdem.loop.match_1.eq_1 : ∀ (motive : ℕ → List ℕ → Sort u_1) (curr next : ℕ) (rest : List ℕ)
  (h_1 : (curr next : ℕ) → (rest : List ℕ) → motive curr (next :: rest)) (h_2 : (curr : ℕ) → motive curr []),
  (match curr, next :: rest with
    | curr, next :: rest => h_1 curr next rest
    | curr, [] => h_2 curr) =
    h_1 curr next rest
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvolutiveInvOfMulOpposite : {M : Type u_1} → [InvolutiveInv Mᵐᵒᵖ] → InvolutiveInv Mᵈᵐᵃ
-- Aesop.Stats.Basic
Aesop.Stats.mk.sizeOf_spec : ∀ (total configParsing ruleSetConstruction search ruleSelection script forwardState : Aesop.Nanos)
  (scriptGenerated : Option Aesop.ScriptGenerated) (ruleStats : Array Aesop.RuleStats)
  (goalStats : Array Aesop.GoalStats),
  sizeOf
      { total := total, configParsing := configParsing, ruleSetConstruction := ruleSetConstruction, search := search,
        ruleSelection := ruleSelection, script := script, forwardState := forwardState,
        scriptGenerated := scriptGenerated, ruleStats := ruleStats, goalStats := goalStats } =
    1 + sizeOf total + sizeOf configParsing + sizeOf ruleSetConstruction + sizeOf search + sizeOf ruleSelection +
              sizeOf script +
            sizeOf forwardState +
          sizeOf scriptGenerated +
        sizeOf ruleStats +
      sizeOf goalStats
-- Mathlib.FieldTheory.Finite.Trace
/-- The trace map from a finite field to its prime field is nondegenerate.  -/
FiniteField.trace_to_zmod_nondegenerate : ∀ (F : Type u_1) [inst : Field F] [Finite F] [inst_2 : Algebra (ZMod (ringChar F)) F] {a : F},
  a ≠ 0 → ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise_drop : ∀ {α : Type u} {R : α → α → Prop} {s : Stream'.Seq α},
  Stream'.Seq.Pairwise R s → ∀ {n : ℕ}, Stream'.Seq.Pairwise R (s.drop n)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aeval_eq_zero_of_mem_rootSet : ∀ {S : Type v} {T : Type w} [inst : CommRing T] {p : Polynomial T} [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S] {a : S}, a ∈ p.rootSet S → (Polynomial.aeval a) p = 0
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typesGlue.congr_simp : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u)
  (f f_1 : α → S.obj (Opposite.op PUnit.{u + 1})),
  f = f_1 → CategoryTheory.typesGlue S hs α f = CategoryTheory.typesGlue S hs α f_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termZ_1 : Lean.ParserDescr
-- Mathlib.ModelTheory.Basic
/-- Any element of a `HomClass` can be realized as a first order homomorphism.  -/
FirstOrder.Language.HomClass.toHom : {L : FirstOrder.Language} →
  {F : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] → [inst_2 : FunLike F M N] → [L.HomClass F M N] → F → L.Hom M N
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Rcc α → Std.DTreeMap.Internal.Const.RccSliceData α β
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.eq_def : ∀ (bytes : ByteArray) (i : ℕ),
  bytes.utf8DecodeChar? i =
    if h₀ : i < bytes.size then
      match h : ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] with
      | ByteArray.utf8DecodeChar?.FirstByte.invalid => none
      | ByteArray.utf8DecodeChar?.FirstByte.done => ByteArray.utf8DecodeChar?.assemble₁ bytes[i] h
      | ByteArray.utf8DecodeChar?.FirstByte.oneMore =>
        if h₁ : i + 1 < bytes.size then ByteArray.utf8DecodeChar?.assemble₂ bytes[i] bytes[i + 1] else none
      | ByteArray.utf8DecodeChar?.FirstByte.twoMore =>
        if h₁ : i + 2 < bytes.size then ByteArray.utf8DecodeChar?.assemble₃ bytes[i] bytes[i + 1] bytes[i + 2] else none
      | ByteArray.utf8DecodeChar?.FirstByte.threeMore =>
        if h₁ : i + 3 < bytes.size then
          ByteArray.utf8DecodeChar?.assemble₄ bytes[i] bytes[i + 1] bytes[i + 2] bytes[i + 3]
        else none
    else none
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The values of a multiplicative character `χ` such that `χ^n = 1` are contained in `ℤ[μ]` when
`μ` is a primitive `n`th root of unity.  -/
MulChar.apply_mem_algebraAdjoin_of_pow_eq_one : ∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] [IsDomain R] {χ : MulChar F R} {n : ℕ}
  [NeZero n], χ ^ n = 1 → ∀ {μ : R}, IsPrimitiveRoot μ n → ∀ (a : F), χ a ∈ ℤ[μ]
-- Mathlib.RingTheory.Etale.QuasiFinite
PrimeSpectrum.preimageEquivFiber.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R),
  PrimeSpectrum.preimageEquivFiber R S p =
    {
      toFun := fun q =>
        {
          asIdeal :=
            RingHom.ker
              (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯)
                  (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
          isPrime := ⋯ },
      invFun := fun q => ⟨PrimeSpectrum.comap Algebra.TensorProduct.includeRight.toRingHom q, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function is at most another is Diophantine.  -/
Dioph.«term_D≤_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.mk.injEq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} (f : R.X₁ ⟶ R'.X₁)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f) = R'.w)
      CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam)
  (f_1 : R.X₁ ⟶ R'.X₁)
  (comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f_1) = R'.w)
      CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  {inv : Std.Do.PostCond β ps},
  (∀ (x : α) (hx : x ∈ xs) (b : β),
      ⦃inv.1 b⦄
        f x hx b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 b'
          | ForInStep.done b' => inv.1 b',
          inv.2)⦄) →
    ⦃inv.1 init⦄ forIn' xs init f ⦃inv⦄
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.BisimO.match_1.eq_3 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (x x_1 : α ⊕ Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_2 : α ⊕ Computation α) → motive x x_2),
  (∀ (a a' : α), x = Sum.inl a → x_1 = Sum.inl a' → False) →
    (∀ (s s' : Computation α), x = Sum.inr s → x_1 = Sum.inr s' → False) →
      (match x, x_1 with
        | Sum.inl a, Sum.inl a' => h_1 a a'
        | Sum.inr s, Sum.inr s' => h_2 s s'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- For `A B` two nonempty finite sets, there always exist `a0 ∈ A, b0 ∈ B` such that
`UniqueAdd A B a0 b0`  -/
UniqueSums.uniqueAdd_of_nonempty : ∀ {G : Type u_1} {inst : Add G} [self : UniqueSums G] {A B : Finset G},
  A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueAdd A B a0 b0
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.neg_hom_apply : ∀ {M N : AddCommMonCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.Data.Fin.Lemmas
Fin.cast_mk : ∀ {n m : ℕ} (h : n = m) (i : ℕ) (hn : i < n), Fin.cast h ⟨i, hn⟩ = ⟨i, ⋯⟩
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.throwNoGoalsToBeSolved : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Analysis.Calculus.Deriv.ZPow
hasDerivWithinAt_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜),
  x ≠ 0 ∨ 0 ≤ m → ∀ (s : Set 𝕜), HasDerivWithinAt (fun x => x ^ m) (↑m * x ^ (m - 1)) s x
-- Init.Data.Array.Lemmas
Array.toList_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {xs : Array α} {ys : Array β},
  (Array.zipWith f xs ys).toList = List.zipWith f xs.toList ys.toList
-- Init.Data.UInt.Bitwise
UInt8.and_eq_neg_one_iff : ∀ {a b : UInt8}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
/-- A morphism property stable under tensoring, associators, and unitors.  -/
CategoryTheory.MorphismProperty.IsMonoidalStable : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → [CategoryTheory.MonoidalCategory C] → Prop
-- Mathlib.Data.Nat.ModEq
Nat.instDecidableModEq : {n a b : ℕ} → Decidable (a ≡ b [MOD n])
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit : {α : Type u} → Std.Sat.Literal α → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.strongEpi_of_effectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f],
  CategoryTheory.StrongEpi f
-- Mathlib.Order.Category.BddDistLat
BddDistLat.coe_of : ∀ (α : Type u_1) [inst : DistribLattice α] [inst_1 : BoundedOrder α], ↑(BddDistLat.of α).toDistLat = α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The Galois coinsertion between ideal sheaves and arbitrary families of ideals.  -/
AlgebraicGeometry.Scheme.IdealSheafData.gci : {X : AlgebraicGeometry.Scheme} →
  GaloisCoinsertion AlgebraicGeometry.Scheme.IdealSheafData.ideal AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalPresentable X κ] (J : Type u₃) [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [CategoryTheory.EssentiallySmall.{w, v₃, u₃} J] [CategoryTheory.IsCardinalFiltered J κ],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The second projection of a pullback cone.  -/
CategoryTheory.Limits.PullbackCone.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Z} → {g : Y ⟶ Z} → (t : CategoryTheory.Limits.PullbackCone f g) → t.pt ⟶ Y
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices.  -/
Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {b : α} [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b
-- Mathlib.RingTheory.Coprime.Lemmas
exists_sum_eq_one_iff_pairwise_coprime' : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {s : I → R} [inst_1 : Fintype I] [Nonempty I]
  [inst_3 : DecidableEq I], (∃ μ, ∑ i, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (Function.onFun IsCoprime s)
-- Mathlib.RingTheory.WittVector.Frobenius
/-- If `R` has characteristic `p`, then there is a ring endomorphism
that raises `r : R` to the power `p`.
By applying `WittVector.map` to this endomorphism,
we obtain a ring endomorphism `frobenius R p : 𝕎 R →+* 𝕎 R`.

The underlying function of this morphism is `WittVector.frobeniusFun`.
 -/
WittVector.frobenius : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [inst : CommRing R] → WittVector p R →+* WittVector p R
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.instLinearLocalization' : (R : Type w) →
  [inst : Ring R] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          (W : CategoryTheory.MorphismProperty C) →
            [CategoryTheory.Linear R C] →
              [inst_4 : W.HasLocalization] →
                [inst_5 : CategoryTheory.Preadditive W.Localization'] →
                  [W.Q'.Additive] → CategoryTheory.Linear R W.Localization'
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupPart : Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty → Lean.Doc.DocM (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.toNonneg.eq_1 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] (a : α), Nonneg.toNonneg a = ⟨a ⊔ 0, ⋯⟩
-- Mathlib.Condensed.Light.Basic
LightCondSet.hom_naturality_apply : ∀ {X Y : LightCondSet} (f : X ⟶ Y) {S T : LightProfiniteᵒᵖ} (g : S ⟶ T) (x : X.obj.obj S),
  (CategoryTheory.ConcreteCategory.hom (f.hom.app T)) ((CategoryTheory.ConcreteCategory.hom (X.obj.map g)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.obj.map g)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app S)) x)
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedMonoid.mul_le_mul_left : ∀ {α : Type u_2} {inst : CommMonoid α} {inst_1 : Preorder α} [self : IsOrderedMonoid α] (a b : α),
  a ≤ b → ∀ (c : α), a * c ≤ b * c
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.i₀_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.Precylinder A),
  CategoryTheory.CategoryStruct.comp self.i₀ self.π = CategoryTheory.CategoryStruct.id A
-- Batteries.Data.List.Lemmas
List.filterMap.match_1.congr_eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : Unit → motive none)
  (h_2 : (b : β) → motive (some b)),
  x = none →
    (match x with
      | none => h_1 ()
      | some b => h_2 b) ≍
      h_1 ()
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.nonneg : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {K : ℝ} {A B : Set X},
  CovBySMul M K A B → 0 ≤ K
-- Aesop.Forward.RuleInfo
/-- The rule's number of premises.  -/
Aesop.ForwardRuleInfo.numPremises : Aesop.ForwardRuleInfo → ℕ
-- Mathlib.Algebra.Group.Action.Defs
MulDistribMulAction.ext : ∀ {M : Type u_9} {N : Type u_10} {inst : Monoid M} {inst_1 : Monoid N} {x y : MulDistribMulAction M N},
  SMul.smul = SMul.smul → x = y
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMkMor₁BicategoryM : Mathlib.Tactic.BicategoryLike.MkMor₁ Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Topology.MetricSpace.Similarity
/-- Families with at most a single point are always similar.  -/
Similar.of_subsingleton_index : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂] [Subsingleton ι], Similar v₁ v₂
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.atEnd.eq_1 : ∀ (x : String.Pos.Raw) (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.atEnd x = (x.offsetBy b == stopPos)
-- Mathlib.Data.DFinsupp.BigOperators
/-- The `DFinsupp` version of `Finsupp.liftAddHom_comp_single`  -/
DFinsupp.liftAddHom_comp_single : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι),
  (DFinsupp.liftAddHom f).comp (DFinsupp.singleAddHom β i) = f i
-- Mathlib.Topology.Spectral.Hom
SpectralMap.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.FunctorToTypes.binaryProductIso F G =
    CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.FunctorToTypes.binaryProductLimitCone F G)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_div_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t : Finset α}, s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_product'`.  -/
Finset.prod_product : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β),
  ∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y)
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_le : ∀ (m n : ℕ), m >>> n ≤ m
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.coe_decomposeTensor_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  [inst_6 : DirectSum.Decomposition ℳ] (x : DirectSum ι fun i => ↥(DirectSum.decomposeTensor ℳ N i)),
  (DirectSum.coeAddMonoidHom (DirectSum.decomposeTensor ℳ N)) x =
    (LinearEquiv.rTensor N (DirectSum.decomposeLinearEquiv ℳ).symm)
      ((TensorProduct.directSumLeft R R (fun i => ↥(ℳ i)) N).symm
        ((DirectSum.congrLinearEquiv (DirectSum.decomposeTensorEquiv ℳ N)).symm x))
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.lt.sizeOf_spec : sizeOf Mathlib.Meta.Positivity.OrderRel.lt✝ = 1
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.restrict : ∀ {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}
  {p : Submodule R M} (hp : p ∈ f.invtSubmodule), f.IsSemisimple → Module.End.IsSemisimple (LinearMap.restrict f hp)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Ici : ∀ {n : ℕ} (a : Fin n), Finset.map Fin.valEmbedding (Finset.Ici a) = Finset.Ico (↑a) n
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  [inst_1 : SizeOf G] (toReducedWord : HNNExtension.NormalWord.ReducedWord G A B)
  (mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u),
  sizeOf { toReducedWord := toReducedWord, mem_set := mem_set } = 1 + sizeOf toReducedWord
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.inter_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.next.injEq : ∀ (guard : Lean.Expr) (pending : List Lean.Meta.Grind.TheoremGuard) (guard_1 : Lean.Expr)
  (pending_1 : List Lean.Meta.Grind.TheoremGuard),
  (Lean.Meta.Grind.ActivateNextGuardResult.next guard pending =
      Lean.Meta.Grind.ActivateNextGuardResult.next guard_1 pending_1) =
    (guard = guard_1 ∧ pending = pending_1)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_monomial : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {n : ℕ} {a : R},
  Polynomial.map f ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
-- Init.Data.BitVec.Lemmas
BitVec.reverse.eq_def : ∀ (x : ℕ) (x_1 : BitVec x),
  x_1.reverse =
    match x, x_1 with
    | 0, x => x
    | w.succ, x => (BitVec.truncate w x).reverse.concat x.msb
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The identity equivalence of a root pairing.  -/
RootPairing.Equiv.id : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.Equiv P
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.bot_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {b : WithBot α}, b ≠ 0 → ⊥ * b = ⊥