mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Dilation
/-- Alternative `Dilation` constructor when the distance hypothesis is over `dist`  -/
Dilation.mkOfDistEq : {α : Type u_5} →
  {β : Type u_6} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (f : α → β) → (∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) → α →ᵈ β
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.right_act_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp M.actRight (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.hom B.X)
      (CategoryTheory.CategoryStruct.comp N.actRight h)
-- Mathlib.MeasureTheory.Order.Lattice
/-- **Alias** of `Measurable.sup`. -/
Measurable.sup' : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Max M]
  [MeasurableSup₂ M], Measurable f → Measurable g → Measurable (f ⊔ g)
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.filter_collapse_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α},
  a ∉ s →
    ∀ (𝒜 : Finset (Finset α)),
      {t ∈ 𝒜 | t.erase a = s} =
        if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k}, k' ∈ t.modify k f ↔ k' ∈ t
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoEToCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), CategoryTheory.Mono (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂)
-- Init.Grind.Ordered.Rat
Lean.Grind.instOrderedRingRat : Lean.Grind.OrderedRing ℚ
-- Mathlib.Topology.Algebra.Order.UpperLower
/-- Ad hoc class stating that the closure of an upper set is an upper set. This is used to state
lemmas that do not mention algebraic operations for both the additive and multiplicative versions
simultaneously. If you find a satisfying replacement for this typeclass, please remove it!  -/
HasUpperLowerClosure : (α : Type u_1) → [TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The `CorepresentableBy` structure asserting that the Type-valued functor
`Y ↦ (F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ Y)` is corepresented by
`F ⊛ G ⊛ H`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F G H : CategoryTheory.Functor C V) →
              [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution G H] →
                [inst_5 :
                    CategoryTheory.MonoidalCategory.DayConvolution F
                      (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                              (CategoryTheory.MonoidalCategory.tensor C)).comp
                          (((CategoryTheory.Functor.whiskeringLeft (C × C × C) (C × C) V).obj
                                ((CategoryTheory.Functor.id C).prod (CategoryTheory.MonoidalCategory.tensor C))).comp
                            (CategoryTheory.coyoneda.obj
                              (Opposite.op
                                (CategoryTheory.MonoidalCategory.externalProduct F
                                  (CategoryTheory.MonoidalCategory.externalProduct G H)))))).CorepresentableBy
                      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H))
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instAddGroup : {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → AddGroup (AddMonoid.Coprod G H)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.le_ker_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y.Hom Z),
  g.ker ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- Copy of a convex cone with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
ConvexCone.copy : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → (C : ConvexCone R M) → (s : Set M) → s = ↑C → ConvexCone R M
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀ : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : AddMonoid M]
  [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → M},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ProbabilityTheory.IndepFun f g μ →
        MeasureTheory.Measure.map (f + g) μ = (MeasureTheory.Measure.map f μ).conv (MeasureTheory.Measure.map g μ)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℤ), preNormEDS b c d n = ↑n.sign * preNormEDS' b c d n.natAbs
-- Mathlib.GroupTheory.Index
/-- Finite index implies finite quotient.  -/
AddSubgroup.fintypeOfIndexNeZero : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → H.index ≠ 0 → Fintype (G ⧸ H)
-- Init.Data.Order.LemmasExtra
Std.instOrientedOrdOfLawfulOrderOrd : ∀ {α : Type u} [inst : LE α] [inst_1 : Ord α] [Std.LawfulOrderOrd α], Std.OrientedOrd α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) {X Y : (SimplexCategory.Truncated n)ᵒᵖ} (f : X ⟶ Y),
  (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).obj F).map f = H.map (F.map f)
-- Mathlib.Order.Hom.Basic
OrderIso.apply_eq_iff_eq_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (x : α) (y : β), e x = y ↔ x = e.symm y
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.mk.inj : ∀ {R : Type u} {inst : Ring R} {Q : Type v} {inst_1 : AddCommGroup Q} {inst_2 : Module R Q} {M : Type u_1}
  {N : Type u_2} {inst_3 : AddCommGroup M} {inst_4 : AddCommGroup N} {inst_5 : Module R M} {inst_6 : Module R N}
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {toLinearPMap : N →ₗ.[R] Q} {le : i.range ≤ toLinearPMap.domain}
  {is_extension : ∀ (m : M), f m = ↑toLinearPMap ⟨i m, ⋯⟩} {toLinearPMap_1 : N →ₗ.[R] Q}
  {le_1 : i.range ≤ toLinearPMap_1.domain} {is_extension_1 : ∀ (m : M), f m = ↑toLinearPMap_1 ⟨i m, ⋯⟩},
  { toLinearPMap := toLinearPMap, le := le, is_extension := is_extension } =
      { toLinearPMap := toLinearPMap_1, le := le_1, is_extension := is_extension_1 } →
    toLinearPMap = toLinearPMap_1
-- Init.Data.Array.Lemmas
Array.any_push : ∀ {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool}, (xs.push a).any p = (xs.any p || p a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k fallback : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Raw.Const.get m x ⋯)).getD fallback
-- Mathlib.Order.Circular
Set.cIoo.eq_1 : ∀ {α : Type u_1} [inst : CircularPreorder α] (a b : α), Set.cIoo a b = {x | sbtw a x b}
-- Init.Sym.Lemmas
Lean.Sym.UInt32.eq_eq_true : ∀ (a b : UInt32), decide (a = b) = true → (a = b) = True
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], OfNat.ofNat n = ↑(OfNat.ofNat n)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_sub_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x y : K)
  (hx : 0 ≤ ArchimedeanClass.mk x) (hy : 0 ≤ ArchimedeanClass.mk y),
  ArchimedeanClass.FiniteElement.mk x hx - ArchimedeanClass.FiniteElement.mk y hy =
    ArchimedeanClass.FiniteElement.mk (x - y) ⋯
-- Mathlib.Algebra.Module.Shrink
/-- Shrinking `α` to a smaller universe preserves module structure.  -/
Shrink.linearEquiv : (R : Type u_1) →
  (α : Type u_2) →
    [inst : Small.{v, u_2} α] →
      [inst_1 : Semiring R] → [inst_2 : AddCommMonoid α] → [inst_3 : Module R α] → Shrink.{v, u_2} α ≃ₗ[R] α
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousOn.nnnorm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun x => ‖f x‖₊) s
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.not_isBigO : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {g' : α → F'} {f'' : α → E''} {l : Filter α}, f'' =o[l] g' → (∃ᶠ (x : α) in l, f'' x ≠ 0) → ¬g' =O[l] f''
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_id : ∀ (V : Type u_1) [inst : SeminormedAddCommGroup V], ⇑(NormedAddGroupHom.id V) = id
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.supClosed : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α), SupClosed ↑L
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a commutative Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero,
`NormedSpace.exp (x+y) = (NormedSpace.exp x) * (NormedSpace.exp y)`
for all `x`, `y` in the disk of convergence.  -/
NormedSpace.exp_add_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x y : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    y ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
      NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategory} (e : Δ' ⟶ Δ)
  [inst_3 : CategoryTheory.Epi e] {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj (Opposite.op Δ') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map e.op) h) =
    CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e))
      h
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_comp_neg : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {β : Type u_4} [inst_2 : InvolutiveNeg β]
  (f : β → α), ∏' (d : β), f (-d) = ∏' (d : β), f d
-- Mathlib.Combinatorics.Matroid.Basic
/-- A predicate `P` on sets satisfies the **exchange property** if,
for all `X` and `Y` satisfying `P` and all `a ∈ X \ Y`, there exists `b ∈ Y \ X` so that
swapping `a` for `b` in `X` maintains `P`.  -/
Matroid.ExchangeProperty : {α : Type u_1} → (Set α → Prop) → Prop
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensor_injective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [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] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CochainComplex.mkHom.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : CochainComplex V ℕ) (zero zero_1 : P.X 0 ⟶ Q.X 0) (e_zero : zero = zero_1) (one one_1 : P.X 1 ⟶ Q.X 1)
  (e_one : one = one_1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one)
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f''),
  succ = succ_1 → P.mkHom Q zero one one_zero_comm succ = P.mkHom Q zero_1 one_1 ⋯ succ_1
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_int8ToBitVec : ∀ (x : Int8), Int32.ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.pmap.match_1.eq_2 : ∀ {α : Type u_1} {P : α → Prop} (motive : (x : List α) → (∀ a ∈ x, P a) → Sort u_2) (a : α) (l : List α)
  (H : ∀ a_1 ∈ a :: l, P a_1) (h_1 : (x : ∀ a ∈ [], P a) → motive [] x)
  (h_2 : (a : α) → (l : List α) → (H : ∀ a_1 ∈ a :: l, P a_1) → motive (a :: l) H),
  (match a :: l, H with
    | [], x => h_1 x
    | a :: l, H => h_2 a l H) =
    h_2 a l H
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.mulOppositeEquiv_symm_apply_apply : ∀ {M : Type u_2} [inst : Monoid M] (m x : M), (MulActionHom.End.mulOppositeEquiv.symm m) x = m * x
-- Lean.Meta.LazyDiscrTree
/-- Navigate to a key path and return all values in that subtree, then drop them.  -/
Lean.Meta.LazyDiscrTree.extractKeyAux : {α : Type} →
  Lean.Meta.LazyDiscrTree.TrieIndex → List Lean.Meta.LazyDiscrTree.Key → Lean.Meta.LazyDiscrTree.MatchM α (Array α)
-- Init.Data.Ord.Basic
Ordering.then_eq_gt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = Ordering.gt ↔ o₁ = Ordering.gt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.gt
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.instHasRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F],
  L.HasRightKanExtension F
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and nonnegative weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` with nonzero
weight are all equal (and in fact all equal to their center of mass w.r.t. `w`).  -/
StrictConvexOn.map_sum_eq_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i)
-- Mathlib.Computability.Partrec
Decidable.Partrec.const' : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] (s : Part σ) [Decidable s.Dom],
  Partrec fun x => s
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- Monotone circle maps form a lattice with respect to the pointwise order  -/
CircleDeg1Lift.instLattice : Lattice CircleDeg1Lift
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G},
  0 < A.addConvolution B x ↔ x ∈ A + B
-- Mathlib.Algebra.Order.Kleene
pow_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α} {n : ℕ}, a ^ n ≤ KStar.kstar a
-- Mathlib.Algebra.GroupWithZero.NeZero
inv_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ ≠ 0
-- Lean.Elab.InfoTree.Types
/-- The children contain information for nested term elaboration and tactic evaluation  -/
Lean.Elab.InfoTree.node : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Init.Data.Fin.Basic
Fin.val_add_one_le_of_gt : ∀ {n : ℕ} {a b : Fin n}, a > b → ↑b + 1 ≤ ↑a
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The supremum of two elements in a preordered type is a binary coproduct
in the category associated to this preorder.  -/
Preorder.isColimitBinaryCofan : {C : Type u} →
  [inst : SemilatticeSup C] →
    (X Y : C) →
      CategoryTheory.Limits.IsColimit
        (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯))
-- Mathlib.Data.Nat.Bits
Nat.div2_bit0 : ∀ (n : ℕ), (2 * n).div2 = n
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustId : Lean.Option Bool
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.piUnique_symm_apply : ∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)],
  ⇑(LinearEquiv.piUnique R f).symm = (Equiv.piUnique f).invFun
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `additive_of_total`.

---

If a binary function from a type equipped with a total
relation `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in
order to show it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and
`r b c` are satisfied. We allow restricting to a subset specified by a predicate `p`.  -/
additive_of_isTotal : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (r : α → α → Prop) [Std.Total r] (f : α → α → β) (p : α → Prop),
  (∀ {a b : α}, p a → p b → f a b + f b a = 0) →
    (∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b + f b c) →
      ∀ {a b c : α}, p a → p b → p c → f a c = f a b + f b c
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions_unionProd_ι' : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  SSet.innerAnodyneExtensions A.ι → SSet.innerAnodyneExtensions (A.unionProd B).ι
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.zero₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : 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_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (j j' : J), ¬c.Rel j' j → HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' = 0
-- Init.Data.List.Lemmas
List.reverse_eq_concat : ∀ {α : Type u_1} {xs ys : List α} {a : α}, xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If `f : u ⟶ v` and `g : v ⟶ w` are morphisms in `Arrow V` such that `f ≫ g` is right
homotopic to `0`, this is the morphism from the "candidate cokernel" of `f` to `w` defined
from the right homotopy.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.desc : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] →
        {u v : CategoryTheory.Arrow V} →
          (f : u ⟶ v) →
            {w : CategoryTheory.Arrow V} →
              (g : v ⟶ w) →
                CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f g) 0 →
                  (CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel f ⟶ w)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The ring homomorphism associated to an inclusion of subsemirings.  -/
Subsemiring.inclusion : {R : Type u} → [inst : NonAssocSemiring R] → {S T : Subsemiring R} → S ≤ T → ↥S →+* ↥T
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atBot → Set.Iic (f a) ⊆ f '' Set.Iic a
-- Init.Data.Array.Lemmas
Array.foldl_empty : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β}, Array.foldl f init #[] = init
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.apply_eq_iff_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) {x y : M}, e x = e y ↔ x = y
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_swap : ∀ {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} (μ : MeasureTheory.Measure (α × β)),
  MeasureTheory.Measure.comap Prod.swap μ = MeasureTheory.Measure.map Prod.swap μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.grevlex_k : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Init.Data.List.Count
List.count_cons_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a (a :: l) = List.count a l + 1
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ioi_sdiff_Ici`. -/
Set.Ioi_diff_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ici b = Set.Ioo a b
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo.mk.inj : ∀ {declName : Lean.Name} {stackSz? : Option ℕ} {autoGroupArgs : Bool} {declName_1 : Lean.Name} {stackSz?_1 : Option ℕ}
  {autoGroupArgs_1 : Bool},
  { declName := declName, stackSz? := stackSz?, autoGroupArgs := autoGroupArgs } =
      { declName := declName_1, stackSz? := stackSz?_1, autoGroupArgs := autoGroupArgs_1 } →
    declName = declName_1 ∧ stackSz? = stackSz?_1 ∧ autoGroupArgs = autoGroupArgs_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprPower.repr : Lean.Grind.CommRing.Power → ℕ → Std.Format