mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall g pg x r → HasFPowerSeriesOnBall (f + g) (pf + pg) x r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey!_modify_eq_minKey! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey! = t.minKey!
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_eq_fderivCLM : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {f : TestFunction Ω F n} {v x : E}, ((TestFunction.lineDerivCLM 𝕜 v) f) x = (((TestFunction.fderivCLM 𝕜 n k) f) x) v
-- Mathlib.Data.Finset.Insert
/-- A finset is nontrivial if it has at least two elements.  -/
Finset.Nontrivial : {α : Type u_1} → Finset α → Prop
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00PX](https://stacks.math.columbia.edu/tag/00PX) -/
exists_leadingCoeff_pow_smul_mem_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R),
  integralClosure R S = ⊥ →
    φ.Finite → φ p * t ∈ conductor R (φ Polynomial.X) → ∃ n, p.leadingCoeff ^ n • t ∈ conductor R (φ Polynomial.X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.negMap_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → W.negMap ⟦P⟧ = ⟦![0, 1, 0]⟧
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_update_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
  f (Function.update m i (c • x)) = c • f (Function.update m i x)
-- Mathlib.Order.Category.DistLat
DistLat.Iso.mk_hom : ∀ {α β : DistLat} (e : ↑α ≃o ↑β), (DistLat.Iso.mk e).hom = DistLat.ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalNonAssocRingWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [NonUnitalNonAssocRing α] → NonUnitalNonAssocRing (WithConv (Matrix m n α))
-- Mathlib.Algebra.Polynomial.Div
/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree` for the general case.  -/
Polynomial.rootMultiplicity_eq_natTrailingDegree' : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R}, Polynomial.rootMultiplicity 0 p = p.natTrailingDegree
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.map_mul₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}
  (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n
-- Mathlib.Data.W.Constructions
WType.Listα.cons.inj : ∀ {γ : Type u} {a a_1 : γ}, WType.Listα.cons a = WType.Listα.cons a_1 → a = a_1
-- Mathlib.Data.Matrix.Block
Matrix.toSquareBlockProp_def : ∀ {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : m → Prop), M.toSquareBlockProp p = Matrix.of fun i j => M ↑i ↑j
-- Mathlib.Data.SProd
SProd.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → SProd α β γ
-- Init.Data.List.Lex
List.not_lt_iff_ge : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.mk_pos : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a₁ a₂ : α},
  0 < Lean.Grind.IntModule.OfNatModule.Q.mk (a₁, a₂) ↔ a₂ < a₁
-- Mathlib.Algebra.Order.Ring.Abs
/-- `abs` as a `MonoidWithZeroHom`.  -/
absHom : {α : Type u_1} → [inst : Ring α] → [inst_1 : LinearOrder α] → [IsOrderedRing α] → α →*₀ α
-- Mathlib.Analysis.SpecificLimits.Basic
/-- **Sum of a Geometric Series**  -/
NNReal.hasSum_geometric : ∀ {r : NNReal}, r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
-- Mathlib.Algebra.BigOperators.Pi
Prod.snd_prod : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Finset ι}
  {f : ι → M × N}, (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.none : Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Data.FinEnum
FinEnum.up_equiv_symm : ∀ {α : Type u} [inst : FinEnum α] (i : Fin (FinEnum.card α)), { down := FinEnum.equiv.symm i } = FinEnum.equiv.symm i
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Split a box in `ℝⁿ` into `2 ^ n` boxes by hyperplanes passing through its center.  -/
BoxIntegral.Prepartition.splitCenter : {ι : Type u_1} → [Fintype ι] → (I : BoxIntegral.Box ι) → BoxIntegral.Prepartition I
-- Init.Data.List.Lemmas
List.replicate_eq_append_iff : ∀ {α : Type u_1} {n : ℕ} {l₁ l₂ : List α} {a : α},
  List.replicate n a = l₁ ++ l₂ ↔
    l₁.length + l₂.length = n ∧ l₁ = List.replicate l₁.length a ∧ l₂ = List.replicate l₂.length a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cochain K (L⟦a⟧) n' → Cochain K L n` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cochain.rightUnshift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n' a : ℤ} →
          CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n' →
            (n : ℤ) → n' + a = n → CochainComplex.HomComplex.Cochain K L n
-- Mathlib.Analysis.Normed.Group.Basic
/-- An injective group homomorphism from a `Group` to a `NormedGroup` induces a `NormedGroup`
structure on the domain.  -/
NormedGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : Group E] →
          [inst_2 : NormedGroup F] → [MonoidHomClass 𝓕 E F] → (f : 𝓕) → Function.Injective ⇑f → NormedGroup E
-- Mathlib.Algebra.GCDMonoid.Nat
Int.normalize_of_nonneg : ∀ {z : ℤ}, 0 ≤ z → normalize z = z
-- Mathlib.Algebra.Module.ZMod
AddSubgroup.mem_toZModSubmodule : ∀ (n : ℕ) {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M] {x : M} {S : AddSubgroup M},
  x ∈ (AddSubgroup.toZModSubmodule n) S ↔ x ∈ S
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (p₁ p₂ : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core a b p₁ p₂) = 1 + sizeOf a + sizeOf b + sizeOf p₁ + sizeOf p₂
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_self : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⁅H, H⁆ ≤ H
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_def : ∀ {R : Type u_1} [inst : CommSemiring R] (p n : ℕ) [inst_1 : ExpChar R p] (x : R),
  (iterateFrobenius R p n) x = x ^ p ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.even_add_odd : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousAdd M] {f : ℕ → M},
  HasSum (fun k => f (2 * k)) m → HasSum (fun k => f (2 * k + 1)) m' → HasSum f (m + m')
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).trailingDegree = p.trailingDegree
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_g'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C}
  (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.g' h) =
    CategoryTheory.CategoryStruct.comp h₁.g' (CategoryTheory.CategoryStruct.comp φ.τ₃ h)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac._auto_1)
  [h₁ : (hS.sc k ⋯).HasRightHomology] [h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (hS.sc k ⋯).pOpcycles
      (CategoryTheory.CategoryStruct.comp (hS.opcyclesIsoCycles k ⋯).hom (hS.sc (k + 1) ⋯).iCycles) =
    S.map' (k + 1) (k + 2) ⋯ ⋯
-- Init.Grind.Lemmas
Lean.Grind.intro_with_eq' : (p p' : Prop) → (q : p → Sort u) → (he : p = p') → ((h : p') → q ⋯) → (h : p) → q h
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.comp : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.Monic → q.natDegree ≠ 0 → (p.comp q).Monic
-- Init.Data.Rat.Lemmas
Rat.not_lt : ∀ {a b : ℚ}, ¬a < b ↔ b ≤ a
-- Mathlib.Algebra.Module.SnakeLemma
/-- Suppose we have an exact commutative diagram
```
                K₃
                |
                ι₃
                ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|       |
π₁      π₂
↓       ↓
C₁ -G-→ C₂

```
such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`, and `π₁` is surjective, then `K₃ -δ→ C₁ -G→ C₂` is exact.
 -/
SnakeLemma.exact_δ_left : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (σ : M₃ → M₂) (hσ : ⇑f₂ ∘ σ = id) (ρ : N₂ → N₁)
  (hρ : ρ ∘ ⇑g₁ = id) {K₃ : Type u_9} {C₁ : Type u_10} {C₂ : Type u_11} [inst_13 : AddCommGroup K₃]
  [inst_14 : Module R K₃] [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁] [inst_17 : AddCommGroup C₂]
  [inst_18 : Module R C₂] (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ : N₁ →ₗ[R] C₁)
  (hπ₁ : Function.Exact ⇑i₁ ⇑π₁) (π₂ : N₂ →ₗ[R] C₂), Function.Exact ⋯ ⋯ → ∀ (G : ⋯), ⋯
-- Mathlib.Analysis.Convex.Function
ConcaveOn.add_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E} {f : E → β}
  [IsOrderedAddMonoid β], ConcaveOn 𝕜 s f → ∀ (b : β), ConcaveOn 𝕜 s (f + fun x => b)
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- Let `S` be a nontrivial subgroup in an archimedean linear ordered multiplicative commutative
group `G` with order topology. If the set of elements of `S` that are greater than one
does not have a minimal element, then `S` is dense `G`.  -/
Subgroup.dense_of_no_min : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] (S : Subgroup G), S ≠ ⊥ → (¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a) → Dense ↑S
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryMidEquiv_apply : ∀ (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G),
  (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p) f = ContinuousMultilinearMap.curryMid p f
-- Mathlib.Data.ENNReal.Basic
ENNReal.instPartialOrder : PartialOrder ENNReal
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, t.contains k = true → t.getKey? k = some k
-- Mathlib.Order.Hom.Basic
OrderEmbedding.wellFounded : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β),
  (WellFounded fun x1 x2 => x1 < x2) → WellFounded fun x1 x2 => x1 < x2
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseFooter : Std.Internal.Parsec.ByteArray.Parser (Option String)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
UniqueFactorizationMonoid.moebius.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a a_1 : α),
  a = a_1 → UniqueFactorizationMonoid.moebius a = UniqueFactorizationMonoid.moebius a_1
-- Init.Data.SInt.Lemmas
Int64.neg_zero : -0 = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.mono'_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε} {g : α → ENNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a) → MeasureTheory.MemLp f p μ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insert.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.insert a = m_1.insert a_1
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_range : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] (f : M →* P)
  (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)), (f.noncommCoprod g comm).range = f.range ⊔ g.range
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over `P Q : C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.BinaryBiproductData : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → C → Type (max uC uC')
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat(_)» : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α}
  {fallback : β}, (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l).getD k fallback = fallback
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolutionExists_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [inst_9 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant],
  HasCompactSupport f → Continuous f → MeasureTheory.LocallyIntegrable g μ → MeasureTheory.ConvolutionExists f g L μ
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_eq_coeff : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (n : ℕ),
  ⇑(Perfection.coeffMonoidHom R p n) = ⇑(Perfection.coeff R p n)
-- Mathlib.Topology.LocallyFinsupp
/-- A function with locally finite support within `U` is a triple as specified below.  -/
Function.locallyFinsuppWithin : {X : Type u_1} → [TopologicalSpace X] → Set X → (Y : Type u_2) → [Zero Y] → Type (max u_1 u_2)
-- Mathlib.Data.Finset.Image
Equiv.finsetCongr_refl : ∀ {α : Type u_1}, (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Natural isomorphisms between functors lift to monoid objects.  -/
CategoryTheory.Functor.mapCommMonNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F F' : CategoryTheory.Functor C D} →
                  [inst_6 : F.LaxBraided] →
                    [inst_7 : F'.LaxBraided] →
                      (e : F ≅ F') → [CategoryTheory.NatTrans.IsMonoidal e.hom] → F.mapCommMon ≅ F'.mapCommMon
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.of_succ : ∀ {𝕜 : 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} {n : WithTop ℕ∞},
  ContMDiffAt I I' (n + 1) f x → ContMDiffAt I I' n f x
-- Aesop.Script.CtorNames
Aesop.ctorNamesToRCasesPats : Array Aesop.CtorNames → Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ),
  sq.unop.X₄ = Opposite.unop sq.X₁
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.le_pre : ∀ {X : Type u_2} [inst : EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {μ : MeasureTheory.OuterMeasure X},
  μ ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r ↔ ∀ (s : Set X), Metric.ediam s ≤ r → μ s ≤ m s
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.deflate : {α : Type v} → [small : Std.Internal.Small α] → α → Std.Internal.USquash α
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `contravariant_sequence_exact₂`  -/
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (Y : C) (n : ℕ),
      { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₃ Y n),
          X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₂ Y n),
          X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₁ Y n),
          f := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯),
          g := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp Y ⋯), zero := ⋯ }.Exact
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_div_le : ∀ {M : Type u_2} [inst : DivInvMonoid M] {s t : Set M}, Cardinal.mk ↑(s / t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.instIsClosedUnderIsomorphismsIsCardinalFiltered : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular], (PartOrdEmb.isCardinalFiltered κ).IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
NonnegSpectrumClass.mk : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NonUnitalRing A]
  [inst_3 : PartialOrder A] [inst_4 : Module 𝕜 A],
  (∀ (a : A), 0 ≤ a → ∀ x ∈ quasispectrum 𝕜 a, 0 ≤ x) → NonnegSpectrumClass 𝕜 A
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lowerEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : C} {B : D} (e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B),
  (CategoryTheory.Subobject.lowerEquivalence e).counitIso = CategoryTheory.eqToIso ⋯
-- Init.Data.List.MapIdx
/-- Auxiliary for `mapIdx`:
`mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]`  -/
List.mapIdx.go : {α : Type u_1} → {β : Type u_2} → (ℕ → α → β) → List α → Array β → List β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_toList_rcc : ∀ {m n : ℕ}, (m<...=n).toList = ((m + 1)...=n).toList
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} [inst_3 : Preorder ι]
  {u : ι → α}, CauchySeq u → CauchySeq u⁻¹
-- Mathlib.Algebra.Group.Finsupp
Finsupp.uniqueAddEquiv.congr_simp : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (i i_1 : ι),
  i = i_1 → ∀ [inst_1 : Subsingleton ι], Finsupp.uniqueAddEquiv i = Finsupp.uniqueAddEquiv i_1
-- Mathlib.Analysis.LocallyConvex.AbsConvex
totallyBounded_absConvexHull : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : UniformSpace E]
  [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E],
  TotallyBounded ((absConvexHull ℝ) s) ↔ TotallyBounded s
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.instIsPrimeSupport : ∀ {F : Type u_2} [inst : Field F] (P : RingPreordering F), P.support.IsPrime
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_1 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.zero' x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' x)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Eta-expanded form of `ContinuousAt.const_smul` -/
ContinuousAt.fun_const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β}, ContinuousAt g b → ∀ (c : M), ContinuousAt (fun i => c • g i) b
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.sum : ∀ {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ},
  (∀ i ∈ S, LSeriesSummable (f i) s) → LSeriesSummable (∑ i ∈ S, f i) s
-- Mathlib.Logic.Relation
Relation.SymmGen.of_le : ∀ {α : Type u_7} [inst : LE α] {a b : α}, a ≤ b → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.mk.inj : ∀ {mvarId : Lean.MVarId} {indicesFVarIds : Array Lean.FVarId} {fvarId : Lean.FVarId} {numEqs : ℕ}
  {mvarId_1 : Lean.MVarId} {indicesFVarIds_1 : Array Lean.FVarId} {fvarId_1 : Lean.FVarId} {numEqs_1 : ℕ},
  { mvarId := mvarId, indicesFVarIds := indicesFVarIds, fvarId := fvarId, numEqs := numEqs } =
      { mvarId := mvarId_1, indicesFVarIds := indicesFVarIds_1, fvarId := fvarId_1, numEqs := numEqs_1 } →
    mvarId = mvarId_1 ∧ indicesFVarIds = indicesFVarIds_1 ∧ fvarId = fvarId_1 ∧ numEqs = numEqs_1
-- Init.Data.List.Count
List.not_mem_of_count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a l = 0 → a ∉ l
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.hasBreakContinue : Lean.Elab.Term.Do.Code → Bool