mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor `CommRingObjCat C ⥤ RingObjCat C` is fully faithful.  -/
CategoryTheory.CommRingObjCat.fullyFaithfulForget₂RingObjCat : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.CommRingObjCat.forget₂RingObjCat C).FullyFaithful
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instVAddCoeOfVAddMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            {G : Type u_4} →
              [inst_1 : (i : ι) → VAdd G (R i)] →
                [∀ (i : ι), VAddMemClass (S i) G (R i)] → VAdd G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Data.Num.Basic
ZNum.decidableLE : DecidableLE ZNum
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `AddMonoidAlgebra.sum_coeff_single`. -/
AddMonoidAlgebra.sum_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f : AddMonoidAlgebra R M), f.coeff.sum AddMonoidAlgebra.single = f
-- Mathlib.MeasureTheory.Integral.CircleIntegral
norm_cauchyPowerSeries_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ),
  ‖cauchyPowerSeries f c R n‖ ≤ ((2 * Real.pi)⁻¹ * ∫ (θ : ℝ) in 0..2 * Real.pi, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.pow : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w → ℕ
-- Init.Control.StateCps
StateCpsT.runK_bind_lift : ∀ {α σ : Type u} {m : Type u → Type v} {β γ : Type u} [inst : Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ)
  (k : β → σ → m γ),
  (StateCpsT.lift x >>= f).runK s k = do
    let a ← x
    (f a).runK s k
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → ContinuousAt f x
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffWithinAt_proj : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  {s : Set (Bundle.TotalSpace F E)} {p : Bundle.TotalSpace F E},
  ContMDiffWithinAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj s p
-- Std.Data.TreeSet.Raw.Basic
/-- Compares two tree sets using Boolean equality on keys.

Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
Std.TreeSet.Raw.beq : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Bool
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.recvSelector.registerAux : {α : Type} → Std.CloseableChannel.Bounded✝ α → Std.Async.Waiter (Option α) → IO Unit
-- Init.Data.List.Find
List.mem_of_find?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ l
-- Init.Data.SInt.Lemmas
Int32.toBitVec_zero : Int32.toBitVec 0 = 0#32
-- Mathlib.Dynamics.FixedPoints.Support
/-- A self-map `f : X → X` of a preregular space `X` has compact fixed support if and only if `f`
fixes the complement of a compact set.  -/
Function.HasCompactFixedSupport_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → X} [R1Space X],
  Function.HasCompactFixedSupport f ↔ ∃ K, IsCompact K ∧ (Function.fixedPoints f)ᶜ ⊆ K
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L → ∀ [Algebra.IsAlgebraic F L], Module.rank L ↥(IntermediateField.adjoin L ↑A) = Module.rank F ↥A
-- Mathlib.Order.Concept
Concept.ofAttributes_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r}, Concept.ofAttributes r c.intent = c
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.isUnit_iff_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] {φ : MvPowerSeries σ R},
  IsUnit φ ↔ IsUnit (MvPowerSeries.constantCoeff φ)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup M) (f : M →ₙ* N),
  Function.Injective ⇑f → Subsemigroup.map f (S ⊓ T) = Subsemigroup.map f S ⊓ Subsemigroup.map f T
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractible_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (X : Cᵒᵖ),
  CategoryTheory.Pretriangulated.contractibleTriangle X ∈
    CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit_addSubgroup_subset : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (H : AddSubgroup G) (a : α),
  AddAction.orbit (↥H) a ⊆ AddAction.orbit G a
-- Mathlib.Data.Matrix.Basic
Matrix.diagonalRingHom_apply : ∀ (n : Type u_3) (α : Type u_11) [inst : NonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (d : n → α),
  (Matrix.diagonalRingHom n α) d = Matrix.diagonal d
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
instHasEnoughRootsOfUnityOfNatNat : ∀ {M : Type u_1} [inst : CommMonoid M], HasEnoughRootsOfUnity M 1
-- Init.Data.Bool
Bool.not_or_self : ∀ (x : Bool), (!x || x) = true
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.ofTwoCocycle_proj_apply : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] [inst_6 : LieRingModule L M]
  [inst_7 : LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M))
  (x : (LieAlgebra.Extension.ofTwoCocycle c).L), (LieAlgebra.Extension.ofTwoCocycle c).proj x = x.carrier.1
-- Mathlib.Data.Fintype.EquivFin
/-- Construct an equivalence from functions that are inverse to each other.  -/
Equiv.ofRightInverseOfCardLE : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] →
        Fintype.card α ≤ Fintype.card β → (f : α → β) → (g : β → α) → Function.RightInverse g f → α ≃ β
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- A version of `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`
in terms of the value of the series.  -/
EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →* F},
  Summable ⇑f → ∀ (s : Finset ℕ), ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹ = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.p : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Grind.Linarith.Poly
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- A graded ring homomorphism descends to an additive homomorphism on each indexed component.  -/
GradedRingHom.gradedAddHom : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  {𝒜 : ι → σ} →
                    {ℬ : ι → τ} →
                      [inst_4 : AddSubmonoidClass σ A] →
                        [inst_5 : AddSubmonoidClass τ B] → (𝒜 →+*ᵍ ℬ) → (i : ι) → ↥(𝒜 i) →+ ↥(ℬ i)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `F` and `G` are naturally isomorphic, then `Under.post F` and `Under.post G` are also
naturally isomorphic up to `Under.map`  -/
CategoryTheory.Under.postCongr : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F G : CategoryTheory.Functor T D} →
            (e : F ≅ G) →
              CategoryTheory.Under.post F ≅ (CategoryTheory.Under.post G).comp (CategoryTheory.Under.map (e.hom.app X))
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resComp_inv : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] {K : Type u_6} [inst_8 : Monoid K]
  [inst_9 : TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K),
  (ContAction.resComp V f h).inv =
    { app := fun X => CategoryTheory.CategoryStruct.id ((ContAction.res V (h.comp f)).obj X), naturality := ⋯ }
-- Mathlib.Algebra.Group.Defs
AddCommSemigroup.mk : {G : Type u} → [toAddSemigroup : AddSemigroup G] → (∀ (a b : G), a + b = b + a) → AddCommSemigroup G
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.existsUnique_path : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → ∀ (v w : V), ∃! p, p.IsPath
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformGroup.of_compactSpace : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [ContinuousDiv β] [CompactSpace β], IsUniformGroup β
-- Mathlib.Order.Defs.PartialOrder
/-- The relation `≤` on a preorder is transitive.  -/
le_trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Analysis.MellinTransform
/-- The Mellin inverse transform of a function `f`, defined as `1 / (2π)` times
the integral of `y ↦ x ^ -(σ + yi) • f (σ + yi)`.  -/
mellinInv : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ℝ → (ℂ → E) → ℝ → E
-- Mathlib.RingTheory.KrullDimension.Field
ringKrullDim_eq_zero_of_isField : ∀ {F : Type u_1} [inst : CommRing F], IsField F → ringKrullDim F = 0
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.add_comm : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.add a b = Lean.Grind.Ring.OfSemiring.add b a
-- Mathlib.RingTheory.SimpleModule.InjectiveProjective
Module.injective_of_isSemisimpleRing : ∀ (R : Type u_1) [inst : Ring R] [IsSemisimpleRing R] (M : Type u_2) [inst_2 : AddCommGroup M] [inst_3 : Module R M],
  Module.Injective R M
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.image2_subset_map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N),
  Set.image2 (fun m n => (f m) n) ↑p ↑q ⊆ ↑(Submodule.map₂ f p q)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∈ m₂ → (m₁ ∩ m₂)[k]! = m₁[k]!
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr_trans : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  [inst_13 : Star A₁] [inst_14 : Star A₂] [inst_15 : Star A₃] [inst_16 : Star A₁'] [inst_17 : Star A₂']
  [inst_18 : Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₁' : A₁' ≃⋆ₐ[R] A₂') (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃'),
  (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
-- Mathlib.Combinatorics.Hindman
Hindman.FS.head' : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M), Hindman.FS a a.head
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_ext : ∀ {A B : ProfiniteGrp.{u}} {f g : A ⟶ B}, ProfiniteGrp.Hom.hom f = ProfiniteGrp.Hom.hom g → f = g
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_pi_lambda : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {δ : Type u_6} {X : δ → Type u_7}
  {mX : (a : δ) → MeasurableSpace (X a)} [Countable δ] (f : α → (a : δ) → X a),
  (∀ (a : δ), AEMeasurable (fun c => f c a) μ) → AEMeasurable f μ
-- Mathlib.Data.Finset.Basic
Finset.filter_union : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s₁ s₂ : Finset α),
  Finset.filter p (s₁ ∪ s₂) = Finset.filter p s₁ ∪ Finset.filter p s₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_head_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.minKey he = t.keys.head ⋯
-- Mathlib.Tactic.Attr.Register
/-- `mon_tauto` is a simp set to prove tautologies about morphisms from some (tensor) power of `M`
to `M`, where `M` is a (commutative) monoid object in a (braided) monoidal category.

**This `simp` set is incompatible with the standard simp set.**
If you want to use it, make sure to add the following to your simp call to disable the problematic
default simp lemmas:
```
-MonoidalCategory.whiskerLeft_id, -MonoidalCategory.id_whiskerRight,
-MonoidalCategory.tensor_comp, -MonoidalCategory.tensor_comp_assoc,
-MonObj.mul_assoc, -MonObj.mul_assoc_assoc
```

The general algorithm it follows is to push the associators `α_` and commutators `β_` inwards until
they cancel against the right sequence of multiplications.

This approach is justified by the fact that a tautology in the language of (commutative) monoid
objects "remembers" how it was proved: Every use of a (commutative) monoid object axiom inserts a
unitor, associator or commutator, and proving a tautology simply amounts to undoing those moves as
prescribed by the presence of unitors, associators and commutators in its expression.

This simp set is opinionated about its normal form, which is why it cannot be used concurrently with
some of the simp lemmas in the standard simp set:
* It eliminates all mentions of whiskers by rewriting them to tensored homs,
  which goes against `whiskerLeft_id` and `id_whiskerRight`:
  `X ◁ f = 𝟙 X ⊗ₘ f`, `f ▷ X = 𝟙 X ⊗ₘ f`.
  This goes against `whiskerLeft_id` and `id_whiskerRight` in the standard simp set.
* It collapses compositions of tensored homs to the tensored hom of the compositions,
  which goes against `tensor_comp`:
  `(f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂)`. TODO: Isn't this direction Just Better?
* It cancels the associators against multiplications,
  which goes against `mul_assoc`:
  `(α_ M M M).hom ≫ (𝟙 M ⊗ₘ μ) ≫ μ = (μ ⊗ₘ 𝟙 M) ≫ μ`,
  `(α_ M M M).inv ≫ (μ ⊗ₘ 𝟙 M) ≫ μ = (𝟙 M ⊗ₘ μ) ≫ μ`
* It unfolds non-primitive coherence isomorphisms, like the tensor strengths `tensorμ`, `tensorδ`.
 -/
Parser.Attr.mon_tauto : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Dual.Defs
/-- A reflexive module is one for which the natural map to its double dual is a bijection.

Any finitely-generated projective module (and thus any finite-dimensional vector space)
is reflexive. See `Module.instIsReflexiveOfFiniteOfProjective`.  -/
Module.IsReflexive : (R : Type u_3) → (M : Type u_4) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Algebra.Homology.Precylinder
/-- The pre-path object of a homological complex that is given by
`HomologicalComplex.pathObject`.  -/
HomologicalComplex.prepathObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          [DecidableRel c.Rel] →
            (K : HomologicalComplex C c) →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [K.HasPathObject] → HomotopicalAlgebra.PrepathObject K
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_add' : ∀ {α : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α] (f : α → M) (a b c : α),
  ∑ x ∈ Finset.Ico a b, f (x + c) = ∑ x ∈ Finset.Ico (a + c) (b + c), f x
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- A lifting of a morphism `f : X ⟶ Y` on cofibrant resolutions.
(This is functorial only up to homotopy, see `HoCat.resolution`.)  -/
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        (X ⟶ Y) →
          (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X ⟶
            HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj Y)
-- Mathlib.Topology.Spectral.Prespectral
prespectralSpace_iff : ∀ (X : Type u_3) [inst : TopologicalSpace X],
  PrespectralSpace X ↔ TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If `G` acts on `X` continuously, the set `s +ᵥ t` is closed when `s : Set G` is *compact* and
`t : Set X` is *closed*.

See also `IsClosed.vadd_right_of_isCompact` for a version with the assumptions on `s` and `t`
reversed, assuming that the action is *proper*.  -/
IsClosed.vadd_left_of_isCompact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup α]
  [inst_3 : AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {s : Set α} {t : Set β},
  IsClosed t → IsCompact s → IsClosed (s +ᵥ t)
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Given a connected free groupoid, its generating quiver is rooted-connected.  -/
IsFreeGroupoid.generators_connected : ∀ (G : Type u) [inst : CategoryTheory.Groupoid G] [CategoryTheory.IsConnected G] [inst_2 : IsFreeGroupoid G] (r : G),
  Quiver.RootedConnected (IsFreeGroupoid.symgen✝ r)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ext_iff : ∀ {x y : DyckWord}, x = y ↔ ↑x = ↑y
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S),
  p ∣ q → Polynomial.eval₂ f x p = 0 → Polynomial.eval₂ f x q = 0
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.op_smul_eq_vecMul : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  (A : (Matrix n n R)ᵐᵒᵖ) (v : n → R), A • v = Matrix.vecMul v (MulOpposite.unop A)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.toLocallyRingedSpace : AlgebraicGeometry.Scheme → AlgebraicGeometry.LocallyRingedSpace
-- Lean.Parser.Attr
Lean.Parser.Attr.simple : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Dimension.Free
/-- If a finite module of `finrank 1` has a basis, then this basis has a unique element.  -/
Module.Basis.nonempty_unique_index_of_finrank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R] {ι : Type u_2} (b : Module.Basis ι R M), Module.finrank R M = 1 → Nonempty (Unique ι)
-- Lean.Meta.DiscrTree.Main
/-- Return the root symbol for `e`, and the number of arguments after `reduceDT`.
 -/
Lean.Meta.DiscrTree.getMatchKeyRootFor : Lean.Expr → Lean.MetaM (Lean.Meta.DiscrTree.Key × ℕ)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis.cardinalMk_sdiff_comm : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Mathlib.Tactic.Find
_private.Mathlib.Tactic.Find.0.Mathlib.Tactic.Find.isBlackListed : Lean.Name → Lean.MetaM Bool
-- Lean.Meta.Basic
Lean.Meta.mapErrorImp : {α : Type} → Lean.MetaM α → (Lean.MessageData → Lean.MessageData) → Lean.MetaM α
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (s : ↥M), IsLocalization.mk' S 0 s = 0
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_apply : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : Mul α] (A B : Matrix m n α) (i : m) (j : n),
  A.hadamard B i j = A i j * B i j
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.one_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.MonObj M],
  1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
-- Mathlib.Data.Vector.Basic
/-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl`
of the underlying `List` of the original `Vector`.
 -/
List.Vector.scanl_val : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) {v : List.Vector α n},
  ↑(List.Vector.scanl f b v) = List.scanl f b ↑v
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_neg_iff : ∀ (a : ℤ) {b : ℕ}, b ≠ 0 → (mkRat a b < 0 ↔ a < 0)
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.exists_notMem_of_gt : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α},
  s.PartiallyWellOrderedOn r → ∀ {f : ℕ → α}, (∀ (m n : ℕ), m < n → ¬r (f m) (f n)) → ∃ k, ∀ (m : ℕ), k < m → f m ∉ s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, k ∈ m.insert k v
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Processed equations.  -/
Lean.Meta.Grind.AC.Struct.basis : Lean.Meta.Grind.AC.Struct → List Lean.Meta.Grind.AC.EqCnstr
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f` is circle integrable and `g` is continuous on the circle `sphere c |R|`, then `f * g` is
circle integrable.
 -/
CircleIntegrable.mul_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (f * g) c R
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → FunLike (PseudoEpimorphism α β) α β