mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `F` and `G` are naturally isomorphic, then `Over.post F` and `Over.post G` are also naturally
isomorphic up to `Over.map`  -/
CategoryTheory.Over.postCongr : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F G : CategoryTheory.Functor T D} →
            (e : F ≅ G) →
              (CategoryTheory.Over.post F).comp (CategoryTheory.Over.map (e.hom.app X)) ≅ CategoryTheory.Over.post G
-- Mathlib.Algebra.Ring.Divisibility.Basic
Equiv.dvd_apply : ∀ {G : Type u_4} [inst : LeftCancelSemigroup G] (g a : G), ↑((Equiv.dvd g) a) = g * a
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Prod.dist_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {x y : α × β},
  dist x y = max (dist x.1 y.1) (dist x.2 y.2)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  ms.destruct = some (exp, coef, tl) → ms = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl
-- Mathlib.Algebra.Group.Action.Defs
Function.Surjective.vaddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAdd M β]
  [inst_3 : VAdd N β] [VAddCommClass M N α] {f : α → β},
  Function.Surjective f →
    (∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) → (∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) → VAddCommClass M N β
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.min_singleton : ∀ {α : Type u_1} [inst : Min α] {x : α}, #[x].min ⋯ = x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
    (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) →
      (match x with
        | Lean.Grind.CommRing.Expr.num n => h_1 n
        | Lean.Grind.CommRing.Expr.var x => h_2 x
        | x => h_3 x) =
        h_3 x
-- Mathlib.Order.SymmDiff
inf_himp_bihimp : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b ⇨ a ⊓ b = a ⊔ b
-- Lean.Elab.App
Lean.Elab.Term.elabApp : Lean.Elab.Term.TermElab
-- Lean.Elab.PreDefinition.WF.Unfold
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.matcherPushArg : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_mul : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e e' : E ≃ₗᵢ[R] E), ⇑(e * e') = ⇑e ∘ ⇑e'
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_add : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  (x y : ↥p), ↑(x + y) = ↑x + ↑y
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.ι.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i : D.J),
  D.ι i = CategoryTheory.Limits.Multicoequalizer.π D.diagram i
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonMarkupKind : Lean.FromJson Lean.Lsp.MarkupKind
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.fstYield : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₁' : Std.IterM m β} {out : β} {it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' out) →
    Std.Iterators.Types.Append.PlausibleStep (it₁.append it₂) (Std.IterStep.yield (it₁'.append it₂) out)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
/-- The support of `factorization n` is exactly the Finset of normalized factors  -/
support_factorization : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {n : α}, (factorization n).support = (UniqueFactorizationMonoid.normalizedFactors n).toFinset
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The **Fortuin-Kasteleyn-Ginibre Inequality**.  -/
fkg : ∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f g μ : α → β) [inst_5 : Fintype α],
  0 ≤ μ →
    0 ≤ f →
      0 ≤ g →
        Monotone f →
          Monotone g →
            (∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) →
              (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a)
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_add : ∀ {K : Type u_1} [inst : RCLike K] (r s : ℝ), ↑(r + s) = ↑r + ↑s
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.addEquivOp_symm_apply_coe : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (b : ↥S.op),
  ↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.none : Lean.Meta.Grind.SplitCandidate✝
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.splitter : {n : ℕ} →
  (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) →
    (x x_1 : Fin (n + 1 + 1)) →
      (x_2 : x ≤ x_1) →
        ((isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x) →
          ((isLt : 0 < n + 1 + 1) →
              (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x) →
            ((isLt : 0 < n + 1 + 1) →
                (j : ℕ) →
                  (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x) →
              ((i : ℕ) →
                  (hi : i + 1 < n + 1 + 1) →
                    (j : ℕ) →
                      (hj : j + 1 < n + 1 + 1) →
                        (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij) →
                motive x x_1 x_2
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingDown'Add_f : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b x : A),
  (ComplexShape.embeddingDown'Add a b).f x = x + b
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLattice.toSupSet : {α : Type u_5} → [self : ConditionallyCompleteLattice α] → SupSet α
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_toRight_atTop : ∀ {α : Type u_3} {β : Type u_4}, Filter.Tendsto Finset.toRight Filter.atTop Filter.atTop
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_setWidth_of_lt : ∀ {w : ℕ} {x : BitVec w} {hi lo v : ℕ},
  lo + hi < v → BitVec.extractLsb hi lo (BitVec.setWidth v x) = BitVec.extractLsb hi lo x
-- Batteries.Data.List.Basic
List.forDiagM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → α → m PUnit.{u_1 + 1}),
  List.forDiagM f [] = pure PUnit.unit
-- Std.Time.Format.DateFormat
/-- Two-letter abbreviated weekday names (7 elements, index 0 = Mo).
Used by `EEEEEE`, `eeeeee`, `cccccc`.
 -/
Std.Time.DateFormatSymbols.weekdayTwoLetter : Std.Time.DateFormatSymbols → Vector String 7
-- Mathlib.GroupTheory.Nilpotent
/-- A sequence of additive subgroups of `G` is an ascending central series if `H 0` is
trivial and `⁅H (n + 1), G⁆ ⊆ H n` for all `n`. We do not require that `H n = G` for some `n`.  -/
AddSubgroup.IsAscendingCentralSeries : {G : Type u_1} → [inst : AddGroup G] → (ℕ → AddSubgroup G) → Prop
-- Std.Internal.Do.WP.Basic
/-- `EStateM ε σ`'s `WP` interpretation combining state and exceptions.  -/
Std.Internal.Do.EStateM.wpInst : {ε σ α : Type} → Std.Internal.Do.WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop)
-- Mathlib.Data.Finset.Defs
Finset.ssubset_iff_subset_ne : ∀ {α : Type u_1} {s t : Finset α}, s ⊂ t ↔ s ⊆ t ∧ s ≠ t
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.injective_codRestrict : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  Function.Injective ⇑(f.codRestrict S hf) ↔ Function.Injective ⇑f
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntNegInst : Lean.Meta.Simp.DSimproc
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `ε₀` is the limit of `0`, `ω ^ 0`, `ω ^ ω ^ 0`, …  -/
Ordinal.lt_epsilon_zero : ∀ {o : Ordinal.{u}}, o < Ordinal.epsilon 0 ↔ ∃ n, o < (fun a => Ordinal.omega0 ^ a)^[n] 0
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {p : α → Prop}, (∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | ¬p a} = 0
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_inv_cancel_left : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → ∀ (b : α), a * (a⁻¹ * b) = b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' fallback : α} {f : Option (β k) → Option (β k)},
  m.WF →
    (m.alter k f).getKeyD k' fallback =
      if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toArray_take_zip : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂]
  [Std.Iterators.Productive α₁ Id] [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β₁} {it₂ : Std.Iter β₂} {n : ℕ},
  (Std.Iter.take n (it₁.zip it₂)).toArray = ((Std.Iter.take n it₁).toList.zip (Std.Iter.take n it₂).toList).toArray
-- Mathlib.Order.Monotone.Monovary
antivary_comm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g ↔ Antivary g f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → α × β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : ℕ) →
          (x_2 : α × β) →
            ((x : ℕ) → (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf x fallback) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (n : ℕ) →
                          (fallback : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback) →
                motive x x_1 x_2
-- Mathlib.Logic.Function.Basic
Function.instTotalOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Total r], Std.Total (Function.onFun r f)
-- Mathlib.Data.Num.Lemmas
Num.le_iff_cmp : ∀ {m n : Num}, m ≤ n ↔ m.cmp n ≠ Ordering.gt
-- Mathlib.Algebra.Free
FreeAddMagma.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add β],
  FreeAddMagma.lift =
    { toFun := fun f => { toFun := FreeAddMagma.liftAux f, map_add' := ⋯ }, invFun := fun F => ⇑F ∘ FreeAddMagma.of,
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.keepAliveTimeout : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Option Std.Time.Millisecond.Offset
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.splitter : {σ : String.Slice → Type} →
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
    {s : String.Slice} →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (motive : searcher.Step → Sort u_1) →
          (x : searcher.Step) →
            ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                (startPos endPos : s.Pos) →
                  (hps :
                      searcher.IsPlausibleStep
                        (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
                    x = ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ →
                      motive
                        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩) →
              ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                  (startPos endPos : s.Pos) →
                    (hps :
                        searcher.IsPlausibleStep
                          (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
                      x =
                          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos),
                            hps⟩ →
                        motive
                          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos),
                            hps⟩) →
                ((searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher')) →
                      x = ⟨Std.IterStep.skip searcher', hps⟩ → motive ⟨Std.IterStep.skip searcher', hps⟩) →
                  ((property : searcher.IsPlausibleStep Std.IterStep.done) →
                      x = ⟨Std.IterStep.done, property⟩ → motive ⟨Std.IterStep.done, property⟩) →
                    motive x
-- Mathlib.RingTheory.Teichmuller
Perfection.mk_comp_teichmuller₀ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R],
  (MonoidWithZeroHom.ofClass (Ideal.Quotient.mk I)).comp (Perfection.teichmuller₀ p I) =
    MonoidWithZeroHom.ofClass (Perfection.coeff (R ⧸ I) p 0)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.evenToNeg_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q Q' : QuadraticForm R M) (h : Q' = -Q) (m₁ m₂ : M),
  (CliffordAlgebra.evenToNeg Q Q' h) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) =
    -((CliffordAlgebra.even.ι Q').bilin m₁) m₂
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- Continuously complex-differentiable functions on ℂ are harmonic.
 -/
ContDiffAt.harmonicAt : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F} {x : ℂ},
  ContDiffAt ℂ 2 f x → InnerProductSpace.HarmonicAt f x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {he : t.modify k f ≠ ∅}, (t.modify k f).maxKey he = t.maxKey ⋯
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_unique : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : Unique α]
  {f : α →₀ M} {g : α → M → N}, (f default = 0 → g default 0 = 0) → f.sum g = g default (f default)
-- Init.Data.Array.Basic
/-- Applies a function to each element of the array along with the index at which that element is found,
returning the array of results. In addition to the index, the function is also provided with a proof
that the index is valid.

`Array.mapIdx` is a variant that does not provide the function with evidence that the index is
valid.
 -/
Array.mapFinIdx : {α : Type u} → {β : Type v} → (as : Array α) → ((i : ℕ) → α → i < as.size → β) → Array β
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentSpace.vectorBundle : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M],
  VectorBundle 𝕜 E (TangentSpace I)
-- Mathlib.Analysis.Convex.Cone.Closure
PointedCone.closure_eq : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] {E : Type u_2}
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : ContinuousAdd E] [inst_6 : Module 𝕜 E]
  [inst_7 : ContinuousConstSMul 𝕜 E] {K L : PointedCone 𝕜 E}, K.closure = L ↔ closure ↑K = ↑L
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommMonoid β] → [ContinuousAdd β] → AddCommMonoid (CompactlySupportedContinuousMap α β)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_eq_forIn'_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [inst_6 : Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ}
  {f : (out : β) → out ∈ it → γ → m (ForInStep γ)},
  forIn' it init f = forIn' it.toList init fun out h acc => f out ⋯ acc
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- If `it` plausibly terminates in its immediate next step (`.done`), then `.done` is a plausible
`n`-th output step for arbitrary `n`.
 -/
Std.IterM.IsPlausibleNthOutputStep.done : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {n : ℕ} {it : Std.IterM m β},
  it.IsPlausibleStep Std.IterStep.done → Std.IterM.IsPlausibleNthOutputStep n it Std.IterStep.done
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set equals `a` inserted into the strict subset `s'`.  -/
Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s : Q(Finset «$α»)} →
      (a : Q(«$α»)) →
        (s' : Q(Finset «$α»)) →
          (h : Q(«$a» ∉ «$s'»)) → Q(«$s» = Finset.cons «$a» «$s'» «$h») → Mathlib.Meta.Finset.ProveEmptyOrConsResult s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_η_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.OplaxMonoidal] [inst_9 : G.OplaxMonoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η (F.prod G)).1 = CategoryTheory.Functor.OplaxMonoidal.η F
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ₄_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ₄.natDegree ≤ 6
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.maxD fallback = t_1.maxD fallback_1
-- Mathlib.Algebra.Ring.Basic
/-- Left multiplication by an element of a (semi)ring is an `AddMonoidHom`  -/
AddMonoidHom.mulLeft : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R → R →+ R
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongLimit.ne_zero : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → c ≠ 0
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instGroup : {α : Type u_1} → [Group α] → Group (Lex α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.category_id_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (B : CategoryTheory.Limits.BinaryBicone P Q),
  (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).isEmpty = true → (↑(m₁.inter m₂)).isEmpty = true
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.firstIndexPos : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_mul : ∀ {b c : ENNReal} (a : ENNReal), b ≠ 0 ∨ c ≠ 0 → b ≠ ⊤ ∨ c ≠ ⊤ → a / b * c = a / (b / c)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.limit_topology : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasLimit F],
  (CategoryTheory.Limits.limit F).str =
    ⨅ j,
      TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)))
        (F.obj j).str
-- Mathlib.Data.FinEnum
ULift.instFinEnum : {α : Type u} → [FinEnum α] → FinEnum (ULift.{u_1, u} α)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_le : ∀ {Ω : Type u_1} {a b : ℝ} {N : ℕ} (f : ℕ → Ω → ℝ) (ω : Ω), a < b → MeasureTheory.upcrossingsBefore a b f N ω ≤ N
-- Init.Data.String.Basic
String.Pos.toSlice_lt : ∀ {s : String} {p q : s.Pos}, p.toSlice < q.toSlice ↔ p < q
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ≥0)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
Metric.exists_continuous_nnreal_forall_closedEBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x ↑(δ x) ⊆ U i
-- Init.Data.Int.Lemmas
Int.add_mul : ∀ (a b c : ℤ), (a + b) * c = a * c + b * c
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s s' : Set α} {p : Filter ι},
  UniformCauchySeqOn F p s → s' ⊆ s → UniformCauchySeqOn F p s'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.map f t).getKey! k = t.getKey! k
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_algebraMap : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : PartialOrder A] [inst_5 : StarOrderedRing A] [inst_6 : Algebra 𝕜 A] [inst_7 : Algebra ℝ A]
  [inst_8 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarModule 𝕜 A] [StarModule ℝ A] [IsScalarTower ℝ 𝕜 A]
  (c : 𝕜), CFC.abs ((algebraMap 𝕜 A) c) = (algebraMap ℝ A) ‖c‖
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.pow_zero_pos : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] (a : α), 0 < a ^ 0