mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Nat.Count
/-- The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
minus the difference in the lengths.
 -/
List.Sublist.le_countP : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Sublist l₂ → ∀ (p : α → Bool), List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
-- Aesop.Rule.Forward
/-- If the rule is an unsafe rule, its priority is a percentage representing
the rule's success probability.  -/
Aesop.ForwardRulePriority.unsafe : Aesop.Percent → Aesop.ForwardRulePriority
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The cochain in `Cochain K L n` that is given by a single
morphism `K.X p ⟶ L.X q` and is zero otherwise. (As we do not check
that `p + n = q`, this will be the zero cochain when `p + n ≠ q`.)  -/
CochainComplex.HomComplex.Cochain.single : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} → {p q : ℤ} → (K.X p ⟶ L.X q) → (n : ℤ) → CochainComplex.HomComplex.Cochain K L n
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  T.invRotate.mor₁ =
    -CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (-1)).map T.mor₃)
        ((CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.sigmaAntidiagonalTupleEquivTuple_apply : ∀ (k : ℕ) (x : (n : ℕ) × ↥(Finset.Nat.antidiagonalTuple k n)) (a : Fin k),
  (Finset.Nat.sigmaAntidiagonalTupleEquivTuple k) x a = ↑x.snd a
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.decidableLE : {α : Type u} → (self : Std.Packages.PreorderOfLEArgs α) → DecidableLE α
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α)
  (μ : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ ↔ s.totalVariation.AbsolutelyContinuous μ.ennrealToMeasure
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.instLTTransOfLawfulUpwardEnumerableLT : {α : Type u} →
  [inst : LT α] →
    [inst_1 : Std.PRange.UpwardEnumerable α] →
      [Std.PRange.LawfulUpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerableLT α] →
          Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_3 : HSub Std.Time.Minute.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.getD a fallback
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_signedInfDist_touchpoint_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  i ≠ j → SignType.sign ((s.signedInfDist j) (s.touchpoint ∅ i)) = SignType.sign ((s.signedInfDist j) s.incenter)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.Equiv_toFun : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (e : α ≃ β) (s : HahnSeries.SummableFamily Γ R α) (b : β), (HahnSeries.SummableFamily.Equiv e s) b = s (e.symm b)
-- Mathlib.MeasureTheory.Integral.Prod
/-- Reversed version of **Fubini's Theorem**.  -/
MeasureTheory.integral_integral : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : α → β → E},
  MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
    ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : α × β), f z.1 z.2 ∂μ.prod ν
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_unsat_coeff : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.eq_unsat_coeff_cert p k = true → Int.Internal.Linear.Poly.denote' ctx p = 0 → False
-- Mathlib.Order.RelIso.Basic
RelEmbedding.instFunLike : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → FunLike (r ↪r s) α β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.map f t) k =
        (Option.map (f k') (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.Data.Ordmap.Invariants
/-- The `Balanced t` asserts that the tree `t` satisfies the balance invariants
(at every level).  -/
Ordnode.Balanced : {α : Type u_1} → Ordnode α → Prop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k : α}, t.WF → k ∈ Std.TreeMap.Raw.filter f t → k ∈ t
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.falseToCNF.eq_1 : ∀ {α : Type u_1} (output : α), Std.Sat.AIG.Decl.falseToCNF✝ output = Std.Sat.CNF.add [(output, false)] Std.Sat.CNF.empty
-- Mathlib.Topology.Algebra.Group.Basic
Pi.continuousInv : ∀ {ι : Type u_1} {C : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Inv (C i)]
  [∀ (i : ι), ContinuousInv (C i)], ContinuousInv ((i : ι) → C i)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.eq_factorization_iff : ∀ {n : ℕ} {f : ℕ →₀ ℕ},
  n ≠ 0 → (∀ p ∈ f.support, Nat.Prime p) → (f = n.factorization ↔ (f.prod fun x1 x2 => x1 ^ x2) = n)
-- Mathlib.Analysis.Seminorm
Seminorm.smul_comp : ∀ {R : Type u_1} {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜]
  [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E]
  [inst_4 : AddCommGroup E₂] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] [inst_7 : SMul R ℝ] [inst_8 : SMul R NNReal]
  [inst_9 : IsScalarTower R NNReal ℝ] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : R), (c • p).comp f = c • p.comp f
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.simproc.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Elab.Tactic.ResolveSimpIdResult.simproc declName) = 1 + sizeOf declName
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_neBot : ∀ {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Nonempty (α i)] [Nonempty ι] (f : (i : ι) → Filter (α i))
  [H : ∀ (i : ι), (f i).NeBot], (Filter.coprodᵢ f).NeBot
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toUInt16 = UInt16.ofNat n
-- Mathlib.Data.Nat.Factorization.Basic
Nat.exists_dvd_pow_iff : ∀ {n k : ℕ}, n ≠ 0 → k ≠ 0 → ((∃ m, n ∣ k ^ m) ↔ n.primeFactors ⊆ k.primeFactors)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.homRel C).FactorsThroughLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
-- Std.Http.Data.Headers
/-- Retrieves the first `Header.Value` for the given key.
 -/
Std.Http.Headers.get : (headers : Std.Http.Headers) → (name : Std.Http.Header.Name) → name ∈ headers → Std.Http.Header.Value
-- Mathlib.CategoryTheory.Whiskering
/-- If `α : G ≅ H` then
`isoWhiskerRight α F : (G ⋙ F) ≅ (H ⋙ F)` has components `F.map_iso (α.app X)`.
 -/
CategoryTheory.Functor.isoWhiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {G H : CategoryTheory.Functor C D} → (G ≅ H) → (F : CategoryTheory.Functor D E) → G.comp F ≅ H.comp F
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_smul_linearMap : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M] [inst_9 : SMulCommClass S A M]
  (r : S) (D : Derivation R A M), ↑(r • D) = r • ↑D
-- Mathlib.Data.Num.Basic
/-- Multiplication of two `Num`s.  -/
Num.mul : Num → Num → Num
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.map.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (g g_1 : (i : ι) → G i →+* G' i) (e_g : g = g_1)
  (hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)),
  Ring.DirectLimit.map g hg = Ring.DirectLimit.map g_1 ⋯
-- Lean.Parser.Extra
Lean.Parser.mkAntiquotSplice.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom : ∀ {X Y : AlgebraicGeometry.Scheme} (toLRSHom' : X.Hom Y.toLocallyRingedSpace),
  AlgebraicGeometry.Scheme.Hom.toLRSHom
      (AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace.preimage toLRSHom') =
    toLRSHom'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
commute_iff_mul_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Module ℝ A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a b : A},
  0 ≤ a → 0 ≤ b → (Commute a b ↔ 0 ≤ a * b)
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.mapM f` is another iterator that applies a monadic
function `f` to all values emitted by `it` and emits the result.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a
`MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.map` can be used instead.

**Marble diagram (without monadic effects):**

```text
it          ---a --b --c --d -e ----⊥
it.mapM     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = pure a'`, `f b = pure b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.mapM` will be finite even if `it` isn't. In such cases, the termination
proof needs to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.Iter.mapM : {α β γ : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} → [inst : Monad m] → [inst_1 : MonadAttach m] → (f : β → m γ) → Std.Iter β → Std.IterM m γ
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valuedCompletion : {K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [hv : Valued K Γ₀] → Valued (UniformSpace.Completion K) Γ₀
-- Mathlib.CategoryTheory.Groupoid.Basic
/-- A subgroupoid is totally disconnected if it only has loops.  -/
CategoryTheory.Groupoid.IsTotallyDisconnected : (C : Type u_1) → [CategoryTheory.Groupoid C] → Prop
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.tendsto_meas_smul_symmDiff_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.SMulInvariantMeasure G X μ],
  IsFoelner G μ (↑u) F → ∀ (g h : G), Filter.Tendsto (fun i => μ (symmDiff (g • F i) (h • F i)) / μ (F i)) (↑u) (nhds 0)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.Icc i j = Set.Icc (i.addNat m) (j.addNat m)
-- Mathlib.Order.Defs.LinearOrder
/-- Construct a bundled `LinOrd` from the underlying type and typeclass.  -/
LinOrd.of : (carrier : Type u_2) → [str : LinearOrder carrier] → LinOrd
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through
`weakKernel.ι f` via `weakKernel.lift : W ⟶ weakKernel f`.  -/
CategoryTheory.Limits.weakKernel.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasWeakKernel f] →
            {W : C} →
              (k : W ⟶ X) → CategoryTheory.CategoryStruct.comp k f = 0 → (W ⟶ CategoryTheory.Limits.weakKernel f)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- The property of scheme morphisms `Smooth` is associated with the ring
homomorphism property `Smooth`.  -/
AlgebraicGeometry.instHasRingHomPropertySmoothSmooth : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.Smooth fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOp_right : CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.right =
  Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.right
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] [inst_3 : CompleteLattice δ] (f : FrameHom γ δ) (g : FrameHom β γ) (h : FrameHom α β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.Separation.Basic
tendsto_const_nhds_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] {l : Filter Y} [l.NeBot] {c d : X},
  Filter.Tendsto (fun x => c) l (nhds d) ↔ c = d
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- The subgroup generated by a cycle is in bijection with its support  -/
Equiv.Perm.IsCycle.zpowersEquivSupport : {α : Type u_2} →
  [inst : DecidableEq α] → [inst_1 : Fintype α] → {σ : Equiv.Perm α} → σ.IsCycle → ↥(Subgroup.zpowers σ) ≃ ↥σ.support
-- Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
/-- A multicoequalizer for `I : MultispanIndex J C` is also
a pushout when `J` is essentially `.ofLinearOrder ι` where
`ι` contains exactly two elements.  -/
CategoryTheory.Limits.Multicofork.IsColimit.isPushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Limits.MultispanShape}
  [inst_1 : Unique J.L] {I : CategoryTheory.Limits.MultispanIndex J C} (c : CategoryTheory.Limits.Multicofork I),
  {J.fst default, J.snd default} = Set.univ →
    J.fst default ≠ J.snd default →
      ∀ (hc : CategoryTheory.Limits.IsColimit c),
        CategoryTheory.IsPushout (I.fst default) (I.snd default) (c.π (J.fst default)) (c.π (J.snd default))
-- Mathlib.RingTheory.RegularLocalRing.Defs
isRegularRing_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R],
  IsRegularRing R ↔ ∀ (p : Ideal R) [inst_2 : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)
-- Mathlib.Algebra.Group.Hom.Basic
/-- Makes a group homomorphism from a proof that the map preserves right division
`fun x y => x * y⁻¹`. See also `MonoidHom.of_map_div` for a version using `fun x y => x / y`.
 -/
MonoidHom.ofMapMulInv : {G : Type u_5} →
  [inst : Group G] →
    {H : Type u_8} → [inst_1 : Group H] → (f : G → H) → (∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) → G →* H
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.csInf_le_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s t : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s →
    DirectedOn (fun x1 x2 => x2 ≤ x1) t → BddBelow t → s.Nonempty → s ⊆ t → sInf t ≤ sInf s
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₂.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.isExistential : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsExistential
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- If `e : A ≃ₐ[R] B` is an isomorphism of `R`-algebras, then so is `map e`.  -/
MvPolynomial.mapAlgEquiv : {R : Type u} →
  (σ : Type u_1) →
    [inst : CommSemiring R] →
      {A₁ : Type u_2} →
        {A₂ : Type u_3} →
          [inst_1 : CommSemiring A₁] →
            [inst_2 : CommSemiring A₂] →
              [inst_3 : Algebra R A₁] →
                [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → MvPolynomial σ A₁ ≃ₐ[R] MvPolynomial σ A₂
-- Mathlib.Data.Real.Basic
Real.cauchy_neg : ∀ (a : ℝ), (-a).cauchy = -a.cauchy
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- Summing `a ^ #t * b ^ (n - #t)` over all finite subsets `t` of a finset `s`
gives `(a + b) ^ #s`.  -/
Finset.sum_pow_mul_eq_add_pow : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] (a b : R) (s : Finset ι),
  ∑ t ∈ s.powerset, a ^ t.card * b ^ (s.card - t.card) = (a + b) ^ s.card
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (∀ (a : α), m₁.contains a = true → m₂.contains a = true) → (↑(m₁.inter m₂)).size = (↑m₁).size
-- Mathlib.Topology.Convenient.Category
/-- The counit of the adjunction `ContinuousGeneratedByCat.adj` between
the categories `ContinuousGeneratedByCat X` and `TopCat`.  -/
ContinuousGeneratedByCat.adjCounit : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (TopCat.toContinuousGeneratedByCat X).comp (ContinuousGeneratedByCat.toTopCat X) ⟶
        CategoryTheory.Functor.id TopCat
-- Mathlib.MeasureTheory.Group.Arithmetic
Units.instMeasurableSpace.eq_1 : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : MeasurableSpace M],
  Units.instMeasurableSpace = MeasurableSpace.comap Units.val inst_1
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.State.visited : Lean.Expr.FoldConstsImpl.State → Lean.PtrSet Lean.Expr
-- Init.Data.Array.Lemmas
Array.swapAt!_def : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v : α} (h : i < xs.size), xs.swapAt! i v = (xs[i], xs.set i v h)
-- Mathlib.Algebra.Homology.Bifunctor
/-- The bifunctor on cochain complexes that is induced by a bifunctor.  -/
CategoryTheory.Functor.map₂CochainComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [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.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    [inst_6 : F.PreservesZeroMorphisms] →
                      [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                        [∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ),
                              HomologicalComplex.HasMapBifunctor K₁ K₂ F (ComplexShape.up ℤ)] →
                          CategoryTheory.Functor (CochainComplex C₁ ℤ)
                            (CategoryTheory.Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ))
-- Mathlib.Algebra.Module.NatInt
/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
structure.
See note [reducible non-instances].  -/
Module.addCommMonoidToAddCommGroup : (R : Type u_1) → {M : Type u_3} → [inst : Ring R] → [inst_1 : AddCommMonoid M] → [Module R M] → AddCommGroup M
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq_lem3 : ∀ {a : ℕ} (a1 : 1 < a) {i n : ℕ},
  0 < n →
    ∀ {j : ℕ},
      i < j →
        j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → Pell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaObject_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (x : C),
  (CategoryTheory.WithTerminal.mkCommaObject F).hom.app x =
    F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x))
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- If `P` is a point on the line `AB` and `Q` is equidistant from `A` and `B`, then
`AP * BP = abs (BQ ^ 2 - PQ ^ 2)`.  -/
EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b p q : P},
  p ∈ line[ℝ, a, b] → dist a q = dist b q → dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- An infinite place is complex if it is defined by a complex (i.e. not real) embedding.  -/
NumberField.InfinitePlace.IsComplex : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → Prop
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExists.add_distrib : ∀ {𝕜 : 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 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 : NormedSpace ℝ F]
  [inst_9 : AddGroup G],
  MeasureTheory.ConvolutionExists f g L μ →
    MeasureTheory.ConvolutionExists f' g L μ →
      MeasureTheory.convolution (f + f') g L μ = MeasureTheory.convolution f g L μ + MeasureTheory.convolution f' g L μ
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is purely inseparable, then `Field.Emb F E` has exactly one element.  -/
instUniqueEmbOfIsPurelyInseparable : (F : Type u) →
  (E : Type v) →
    [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → [IsPurelyInseparable F E] → Unique (Field.Emb F E)
-- Mathlib.Order.Heyting.Basic
compl_inf_eq_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, aᶜ ⊓ a = ⊥
-- Mathlib.Data.List.Basic
List.mem_dropLast_of_mem_of_ne_getLast : ∀ {α : Type u} {l : List α} {a : α} (ha : a ∈ l), a ≠ l.getLast ⋯ → a ∈ l.dropLast
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_mem_find?_decide : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ i, p i), Fin.find p h ∈ Fin.find? fun b => decide (p b)