mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
ISize.toInt64_ne_minValue : ∀ (a : ISize), a ≠ ISize.minValue → a.toInt64 ≠ Int64.minValue
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `add_apply`. -/
ProbabilityTheory.Kernel.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as an `AddEquiv`.  -/
AddEquiv.lpBCF : {α : Type u_1} →
  {E : Type u_2} →
    [inst : TopologicalSpace α] →
      [DiscreteTopology α] → [inst_2 : NormedAddCommGroup E] → ↥(lp (fun x => E) ⊤) ≃+ BoundedContinuousFunction α E
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.nonzero.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  {x x_1 : Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) e},
  Mathlib.Tactic.Ring.Common.Overlap.nonzero x = Mathlib.Tactic.Ring.Common.Overlap.nonzero x_1 → x = x_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` is continuous in the topology on `X → R →ᵤ[{spectrum R a}] → R`,
and each `f` is continuous on the spectrum, then `x ↦ cfc (f x) a` is continuous.  -/
Continuous.cfc_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] [inst_10 : TopologicalSpace X] (f : X → R → R) (a : A),
  (Continuous fun x => (UniformOnFun.ofFun {spectrum R a}) (f x)) →
    autoParam (∀ (x : X), ContinuousOn (f x) (spectrum R a)) Continuous.cfc_fun._auto_1 →
      Continuous fun x => cfc (f x) a
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.invOfUnit_eq' : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k) (u : kˣ),
  MvPowerSeries.constantCoeff φ = ↑u → φ.invOfUnit u = φ⁻¹
-- Init.Data.Nat.Gcd
Nat.gcd_add_one : ∀ (x y : ℕ), (x + 1).gcd y = (y % (x + 1)).gcd (x + 1)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_bin : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.bin k v l r).size = l.size + 1 + r.size
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  Std.Internal.List.getValue? k (Std.Internal.List.insertListIfNewUnit l toInsert) =
    if Std.Internal.List.containsKey k l = true ∨ toInsert.contains k = true then some () else none
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos_of_pos_of_nonneg`.  -/
Left.add_pos_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 < a → 0 ≤ b → 0 < a + b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Embedding of a non-unital star subalgebra into the non-unital star algebra.  -/
NonUnitalStarSubalgebraClass.subtype : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Star A] →
          [inst_3 : Module R A] →
            {S : Type w''} →
              [inst_4 : SetLike S A] →
                [inst_5 : NonUnitalSubsemiringClass S A] →
                  [hSR : SMulMemClass S R A] → [inst_6 : StarMemClass S A] → (s : S) → ↥s →⋆ₙₐ[R] A
-- Mathlib.Data.ENat.Lattice
ENat.iInf_eq_natCast_iff : ∀ {ι : Sort u_1} {f : ι → ℕ∞} {n : ℕ}, ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁_ext : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.cocycles₁ A)}, (∀ (g : G), f₁ g = f₂ g) → f₁ = f₂
-- Mathlib.Order.Nucleus
/-- A nucleus is inflationary.  -/
NucleusClass.le_apply : ∀ {F : Type u_2} {X : Type u_3} {inst : SemilatticeInf X} {inst_1 : FunLike F X X} [self : NucleusClass F X] (x : X)
  (f : F), x ≤ f x
-- Lean.Meta.Basic
Lean.Meta.SavedState.mk.injEq : ∀ (core : Lean.Core.SavedState) («meta» : Lean.Meta.State) (core_1 : Lean.Core.SavedState) (meta_1 : Lean.Meta.State),
  ({ core := core, «meta» := «meta» } = { core := core_1, «meta» := meta_1 }) = (core = core_1 ∧ «meta» = meta_1)
-- Lean.Elab.App
/-- `true` if `@` modifier was used
 -/
Lean.Elab.Term.ElabAppArgs.Context.explicit : Lean.Elab.Term.ElabAppArgs.Context → Bool
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.brecOn.eq : ∀ {α : Type u_1} {motive : RBTree.RBNode.Stream α → Sort u} (t : RBTree.RBNode.Stream α)
  (F_1 : (t : RBTree.RBNode.Stream α) → RBTree.RBNode.Stream.below t → motive t),
  RBTree.RBNode.Stream.brecOn t F_1 = F_1 t (RBTree.RBNode.Stream.brecOn.go t F_1).2
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.norm_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F),
  ‖ContinuousLinearMap.adjoint A ∘SL A‖ = ‖A‖ * ‖A‖
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.one =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
      (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)
-- Mathlib.Algebra.Group.Units.Defs
divp_divp_eq_divp_mul : ∀ {α : Type u} [inst : Monoid α] (x : α) (u₁ u₂ : αˣ), x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
-- Mathlib.NumberTheory.Modular
/-- If `|z| < 1`, then applying `S` strictly decreases `im`.  -/
ModularGroup.im_lt_im_S_smul : ∀ {z : UpperHalfPlane}, Complex.normSq ↑z < 1 → z.im < (ModularGroup.S • z).im
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, l.contains k = false → k ∈ m.insertMany l → k ∈ m
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The identity morphism on a locally ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.id : (X : AlgebraicGeometry.LocallyRingedSpace) → X.Hom X
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.append_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)),
  FreeAddGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.orderRingIso_symm_apply : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w)
  (x : WithVal w), h.orderRingIso.symm x = WithVal.toVal v x.ofVal
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq_iff_eventuallyEq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α}, nhdsWithin x s = nhdsWithin x t ↔ s =ᶠ[nhds x] t
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.forIn.match_1.eq_1 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.done d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_1 d
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Clear the instances from the given application.
This is used to deal with classes that have instance parameters.
For example, if you have a local instance of `ContinuousAdd α` and `IsTopologicalAddGroup α`,
then the two `ContinuousAdd α` instances may have slightly different `[Add α]` arguments.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.eraseInstances : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_sub_ofNat : ∀ (r : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], ⌈r - OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ - OfNat.ofNat n
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.mk.injEq : ∀ (toBoundingSieve : BoundingSieve) (level : ℝ) (one_le_level : 1 ≤ level) (toBoundingSieve_1 : BoundingSieve)
  (level_1 : ℝ) (one_le_level_1 : 1 ≤ level_1),
  ({ toBoundingSieve := toBoundingSieve, level := level, one_le_level := one_le_level } =
      { toBoundingSieve := toBoundingSieve_1, level := level_1, one_le_level := one_le_level_1 }) =
    (toBoundingSieve = toBoundingSieve_1 ∧ level = level_1)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.int : ℤ → Lean.Lsp.DiagnosticCode
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Const.minEntry? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → Option (α × β)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.d.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (i j : ℕ),
  s.d i j =
    CategoryTheory.CategoryStruct.comp
      ((s.cofan (Opposite.op { len := i })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := i })))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).d i j)
        (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := j }))))
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (k : ℕ),
  (∀ (m : ℕ), n + k ≤ m → p m = 0) →
    HasFiniteFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 n ⊤
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.getKey? a = m_1.getKey? a_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp_i : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ)
      (groupHomology.shortComplexH1 B).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (groupHomology.chainsMap₁ f φ)
-- Mathlib.Order.Monotone.Defs
antitoneOn_iff_forall_lt : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f a
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_3 : CategoryTheory.HomIsOver f S],
  CategoryTheory.OverClass.asOverHom S f = CategoryTheory.OverClass.asOverHom S f_1
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.ext : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {h h' : Diffeomorph I I' M M' n}, (∀ (x : M), h x = h' x) → h = h'
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.forgetToRingCat_map_hom : ∀ {R S : CommRingCat} (f : R ⟶ S),
  RingCat.Hom.hom ((CategoryTheory.forget₂ CommRingCat RingCat).map f) = CommRingCat.Hom.hom f
-- Mathlib.Data.Finset.PiInduction
/-- Given a predicate on functions `∀ i, Finset (α i)` defined on a finite type, it is true on all
maps provided that it is true on `fun _ ↦ ∅` and for any function `g : ∀ i, Finset (α i)`, an index
`i : ι`, and an element `x : α i` that is strictly less than all elements of `g i`, `p g` implies
`p (update g i (insert x (g i)))`.

This lemma requires `LinearOrder` instances on all `α i`. See also `Finset.induction_on_pi` for a
version that needs `x ∉ g i` and does not need `∀ i, LinearOrder (α i)`.  -/
Finset.induction_on_pi_min : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
  (p fun x => ∅) →
    (∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
        (∀ y ∈ g i, x < y) → p g → p (Function.update g i (insert x (g i)))) →
      p f
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDocumentFilter : Lean.ToJson Lean.Lsp.DocumentFilter
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augment_X_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0),
  (C.augment f w).X 0 = X
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.Lean.Order.Classical.some_spec₂ : ∀ {α : Sort u_1} {p : α → Prop} {h : ∃ a, p a} (q : α → Prop), (∀ (a : α), p a → q a) → q (Classical.choose h)
-- Mathlib.RingTheory.WittVector.Truncated
/-- The universal property of `𝕎 R` as projective limit of truncated Witt vector rings.  -/
WittVector.liftEquiv : {p : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] →
        {S : Type u_2} →
          [inst_2 : Semiring S] →
            { f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ } ≃
              (S →+* WittVector p R)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join_cons : ∀ {α : Type u} (a : α) (s : Stream'.Seq α) (S : Stream'.Seq (Stream'.Seq1 α)),
  (Stream'.Seq.cons (a, s) S).join = Stream'.Seq.cons a (s.append S.join)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.inclusion_injective : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K), Function.Injective ⇑(AddSubgroup.inclusion h)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.mk.inj : ∀ {support : Finset ℕ} {prodPrimes : ℕ} {prodPrimes_squarefree : Squarefree prodPrimes} {weights : ℕ → ℝ}
  {weights_nonneg : ∀ (n : ℕ), 0 ≤ weights n} {totalMass : ℝ} {nu : ArithmeticFunction ℝ}
  {nu_mult : nu.IsMultiplicative} {nu_pos_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → 0 < nu p}
  {nu_lt_one_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → nu p < 1} {support_1 : Finset ℕ} {prodPrimes_1 : ℕ}
  {prodPrimes_squarefree_1 : Squarefree prodPrimes_1} {weights_1 : ℕ → ℝ}
  {weights_nonneg_1 : ∀ (n : ℕ), 0 ≤ weights_1 n} {totalMass_1 : ℝ} {nu_1 : ArithmeticFunction ℝ}
  {nu_mult_1 : nu_1.IsMultiplicative} {nu_pos_of_prime_1 : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes_1 → 0 < nu_1 p}
  {nu_lt_one_of_prime_1 : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes_1 → nu_1 p < 1},
  { support := support, prodPrimes := prodPrimes, prodPrimes_squarefree := prodPrimes_squarefree, weights := weights,
        weights_nonneg := weights_nonneg, totalMass := totalMass, nu := nu, nu_mult := nu_mult,
        nu_pos_of_prime := nu_pos_of_prime, nu_lt_one_of_prime := nu_lt_one_of_prime } =
      { support := support_1, prodPrimes := prodPrimes_1, prodPrimes_squarefree := prodPrimes_squarefree_1,
        weights := weights_1, weights_nonneg := weights_nonneg_1, totalMass := totalMass_1, nu := nu_1,
        nu_mult := nu_mult_1, nu_pos_of_prime := nu_pos_of_prime_1, nu_lt_one_of_prime := nu_lt_one_of_prime_1 } →
    support = support_1 ∧ prodPrimes = prodPrimes_1 ∧ weights = weights_1 ∧ totalMass = totalMass_1 ∧ nu = nu_1
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_map_equiv : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G ≃+ N} {K : AddSubgroup G} {x : N},
  x ∈ AddSubgroup.map f.toAddMonoidHom K ↔ f.symm x ∈ K
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.theory_model : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {T : L.Theory} [h : M ⊨ T]
  {S : L.ElementarySubstructure M}, ↥S ⊨ T
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk₂.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : List Γ),
  Turing.Tape.mk₂ L R = Turing.Tape.mk' (Turing.ListBlank.mk L) (Turing.ListBlank.mk R)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.mk.injEq : ∀ (expr : Lean.Expr) (proof? : Option Lean.Expr) (cache : Bool) (expr_1 : Lean.Expr) (proof?_1 : Option Lean.Expr)
  (cache_1 : Bool),
  ({ expr := expr, proof? := proof?, cache := cache } = { expr := expr_1, proof? := proof?_1, cache := cache_1 }) =
    (expr = expr_1 ∧ proof? = proof?_1 ∧ cache = cache_1)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.LaxFunctor B C) → Inhabited (CategoryTheory.Lax.StrongTrans F F)
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.npow : {n : ℕ} → [NeZero n] → Fin n → ℕ → Fin n
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.enorm_apply_le_semivariation_of_subset : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s t : Set X}, s ⊆ t → ‖μ s‖ₑ ≤ μ.semivariation t
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.refl_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.HomotopyEquiv.refl S).hom = CategoryTheory.CategoryStruct.id S
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.modByMonic_eq_mod : ∀ {R : Type u} [inst : Field R] {q : Polynomial R} (p : Polynomial R), q.Monic → p %ₘ q = p % q
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (a : ℕ) → motive (Int.negSucc a) 0)
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc a, 0 => h_3 a
    | Int.negSucc m, Int.ofNat n.succ => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_2 m n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp.sizeOf_spec : ∀ (k₁ : ℤ) (c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp k₁ c₁ k₂ m₂ c₂) =
    1 + sizeOf k₁ + sizeOf c₁ + sizeOf k₂ + sizeOf m₂ + sizeOf c₂
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.shrink : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M]
  [inst_4 : Small.{u, u_4} M], Module.Finite R (Shrink.{u, u_4} M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Init.Data.UInt.Lemmas
UInt16.ofFin_uint8ToFin : ∀ (n : UInt8), UInt16.ofFin (Fin.castLE UInt8.toFin_toUInt16._proof_1 n.toFin) = n.toUInt16
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.transition : Mathlib.Meta.FunProp.GeneralTheorem → Mathlib.Meta.FunProp.Theorem
-- Mathlib.Algebra.Module.PUnit
PUnit.instIsCentralScalar : ∀ {R : Type u_1}, IsCentralScalar R PUnit.{u_3 + 1}
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.instInhabited : {R : Type u_2} →
  {A : Type u_3} → [inst : Add A] → [inst_1 : Mul A] → [inst_2 : SMul R A] → [inst_3 : Star A] → Inhabited (A ≃⋆ₐ[R] A)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R], JacobsonSpace ↥(AlgebraicGeometry.Spec (CommRingCat.of R))
-- Mathlib.Algebra.Group.Defs
zpow_eq_pow : ∀ {G : Type u_1} [inst : DivInvMonoid G] (n : ℤ) (x : G), ZPow.zpow n x = x ^ n
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.toLinearEquiv_quotientEquivOrthogonal : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  K.quotientEquivOrthogonal.toLinearEquiv = K.quotientEquivOfIsCompl Kᗮ ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (szl : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' l'' : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                Std.DTreeMap.Internal.Impl.Tree α β
                    ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
                  Sort u_3) →
              (x :
                  Std.DTreeMap.Internal.Impl.Tree α β
                    ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size)) →
                ((ℓ : Std.DTreeMap.Internal.Impl α β) →
                    (hℓ₁ : ℓ.Balanced) →
                      (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
                        motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
                  motive x
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.Icc i j = Set.Icc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Data.PNat.Prime
PNat.gcd_coe : ∀ (n m : ℕ+), ↑(n.gcd m) = (↑n).gcd ↑m
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- `a` semiconjugates `x` to `a + x + -a`.  -/
AddSemiconjBy.addConj_mk : ∀ {G : Type u_3} [inst : AddGroup G] (a x : G), AddSemiconjBy a x (a + x + -a)