mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Basic
le_of_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.lt.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : α) (y : β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : (x : α) → (y : β) → motive (some x) (some y))
  (h_3 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some x, some y with
    | none, some val => h_1 val
    | some x, some y => h_2 x y
    | x, x_1 => h_3 x x_1) =
    h_2 x y
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` \(inclusive\).
   -/
Std.Rci.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Rci.Sliceable α β γ] → α → Std.Rci β → γ
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_countablePartition_le_succ : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α n) ≤
    MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α (n + 1))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roc : ∀ {m n fallback : ℤ} {i : ℕ}, (m<...=n).toArray.getD i fallback = if i < (n - m).toNat then m + 1 + ↑i else fallback
-- Mathlib.Algebra.Group.Support
Function.mulSupport_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (f g : α → M),
  (Function.mulSupport fun x => f x * g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.Analysis.Normed.Group.Continuity
/-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by
a real function `a` which tends to `0`, then `f` tends to `0`. In this pair of lemmas
(`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of similar lemmas in
`Topology.MetricSpace.Pseudo.Defs` and `Topology.Algebra.Order`, the `'` version is phrased using
"eventually" and the non-`'` version is phrased absolutely.  -/
squeeze_zero_norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
  (∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
-- Mathlib.Data.EReal.Inv
EReal.div_le_div_right_of_nonneg : ∀ {a b c : EReal}, 0 ≤ c → a ≤ b → a / c ≤ b / c
-- Mathlib.GroupTheory.Congruence.Basic
Con.toSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M], Con.toSubmonoid = { coe := fun c => ↑c }
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.isBounded_image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β) (s : Set α), Bornology.IsBounded (⇑f '' s)
-- Init.Data.SInt.Lemmas
Int8.ofInt_le_iff_le : ∀ {a b : ℤ},
  Int8.minValue.toInt ≤ a →
    a ≤ Int8.maxValue.toInt → Int8.minValue.toInt ≤ b → b ≤ Int8.maxValue.toInt → (Int8.ofInt a ≤ Int8.ofInt b ↔ a ≤ b)
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT : ∀ (κ : Cardinal.{w}) (S : CategoryTheory.SmallCategoryCardinalLT κ),
  HasCardinalLT (CategoryTheory.Arrow (CategoryTheory.SmallCategoryCardinalLT.categoryFamily κ S)) κ
-- Mathlib.Topology.LocallyFinite
LocallyFinite.exists_mem_basis : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {ι' : Sort u_6},
  LocallyFinite f →
    ∀ {p : ι' → Prop} {s : ι' → Set X} {x : X}, (nhds x).HasBasis p s → ∃ i, p i ∧ {j | (f j ∩ s i).Nonempty}.Finite
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofInt : ∀ {n : ℤ}, (Int64.ofInt n).toInt8 = Int8.ofInt n
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.Iio_csSup_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α},
  IsPreconnected s → ¬BddBelow s → BddAbove s → Set.Iio (sSup s) ⊆ s
-- Mathlib.Algebra.Opposites
MulOpposite.instNontrivial : ∀ {α : Type u_1} [Nontrivial α], Nontrivial αᵐᵒᵖ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.support_esymm' : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] [Nontrivial R]
  (n : ℕ),
  (MvPolynomial.esymm σ R n).support = (Finset.powersetCard n Finset.univ).biUnion fun t => {∑ i ∈ t, fun₀ | i => 1}
-- Mathlib.Data.ZMod.Basic
ZMod.val_neg_one : ∀ (n : ℕ), (-1).val = n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.filter f t)[k]! = (Option.filter (fun x => f k' x) t[k]?).get!
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerCongr_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N)
  (r : ↥(AddSubsemigroup.center M)), ↑((AddSubmonoid.centerCongr e) r) = e ↑r
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.range_arcsin : Set.range Real.arcsin = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.GrothendieckTopology.OneHypercover.map_toPreOneHypercover : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {X : C} (E : J.OneHypercover X) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : E.IsPreservedBy F K], (E.map F K).toPreOneHypercover = E.map F
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).ord = OfNat.ofNat n
-- Init.Omega.IntList
/-- Implementation of scalar multiplication by an integer on `IntList`.  -/
Lean.Omega.IntList.smul : Lean.Omega.IntList → ℤ → Lean.Omega.IntList
-- Std.Do.PredTrans
Std.Do.PredTrans.bind_mono : ∀ {ps : Std.Do.PostShape} {α β : Type u} {x y : Std.Do.PredTrans ps α} {f : α → Std.Do.PredTrans ps β},
  x ≤ y → x >>= f ≤ y >>= f
-- Mathlib.Analysis.Polynomial.CauchyBound
/-- `cauchyBound` is a bound on the norm of polynomial roots.
 -/
Polynomial.IsRoot.norm_lt_cauchyBound : ∀ {K : Type u_1} [inst : NormedDivisionRing K] {p : Polynomial K}, p ≠ 0 → ∀ {a : K}, p.IsRoot a → ‖a‖₊ < p.cauchyBound
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.rfl : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} {f : α → E}, f =Θ[𝕜; l] f
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.le_antisymm : ∀ {α : Type u} (self : Std.Packages.PartialOrderOfLEArgs α),
  let this := self.le;
  ∀ (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.Computability.EpsilonNFA
/-- Starting states.  -/
εNFA.start : {α : Type u} → {σ : Type v} → εNFA α σ → Set σ
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.mem_nonZeroDivisorsRight_of_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ : MvPowerSeries σ R},
  MvPowerSeries.constantCoeff φ ∈ nonZeroDivisorsRight R → φ ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, UpperSemicontinuousOn (f i) s) → UpperSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.mk.sizeOf_spec : ∀ (visitedFVars : Lean.FVarIdSet) (visitedMVars : Lean.MVarIdSet) (result : Array Lean.Expr),
  sizeOf { visitedFVars := visitedFVars, visitedMVars := visitedMVars, result := result } =
    1 + sizeOf visitedFVars + sizeOf visitedMVars + sizeOf result
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion`.

---

The `v`-adic completion of `K` is a normed field.  -/
NumberField.HeightOneSpectrum.NumberField.instNormedFieldValuedAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                [Module.Finite ℤ R] →
                  [Module.Free ℤ R] → NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Aesop.Tree.Data
Aesop.Rapp.setChildren : Array Aesop.MVarClusterRef → Aesop.Rapp → Aesop.Rapp
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.FinitaryExtensive D] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [F.ReflectsIsomorphisms], CategoryTheory.FinitaryExtensive C
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.mem_range : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f : R →ₙ+* S} {y : S},
  y ∈ f.range ↔ ∃ x, f x = y
-- Lean.Meta.Hint
Lean.Meta.Hint.instCoeSuggestionTextSuggestion : Coe Lean.Meta.Tactic.TryThis.SuggestionText Lean.Meta.Hint.Suggestion
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n)
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'),
  (CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn').symm γ = γ.rightUnshift n hn'
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mapCotangent_surjective_of_comap_eq : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  Function.Surjective ⇑(algebraMap A B) →
    ∀ {I : Ideal B} {J : Ideal A} (eq : Ideal.comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J),
      Function.Surjective ⇑(J.mapCotangent I (Algebra.ofId A B) ⋯)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableWithinAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x → DifferentiableWithinAt ℂ (fun x => Complex.cosh (f x)) s x
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ Φ_1 : LinearMap.BilinForm R M) (e_Φ : Φ = Φ_1)
  (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N N_1 : LieSubmodule R L M),
  N = N_1 → LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N = LieAlgebra.InvariantForm.orthogonal Φ_1 ⋯ N_1
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.coe_invFun : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  (↑φ.toContinuousLinearEquiv).invFun = ⇑φ.symm
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.hom z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.inv z) h) =
    h
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mk.injEq : ∀ {G : Type w} [inst : TopologicalSpace G] (toFun : TopologicalSpace.Compacts G → NNReal)
  (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂)
  (sup_disjoint' :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂)
  (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂)
  (toFun_1 : TopologicalSpace.Compacts G → NNReal)
  (mono'_1 : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun_1 K₁ ≤ toFun_1 K₂)
  (sup_disjoint'_1 :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun_1 (K₁ ⊔ K₂) = toFun_1 K₁ + toFun_1 K₂)
  (sup_le'_1 : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun_1 (K₁ ⊔ K₂) ≤ toFun_1 K₁ + toFun_1 K₂),
  ({ toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } =
      { toFun := toFun_1, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 }) =
    (toFun = toFun_1)
-- Init.Prelude
Nat.modCore.go : (y : ℕ) → 0 < y → (fuel x : ℕ) → x < fuel → ℕ
-- Mathlib.MeasureTheory.Integral.CompactlySupported
CompactlySupportedContinuousMap.integralPositiveLinearMap_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (μ : MeasureTheory.Measure X) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (f : CompactlySupportedContinuousMap X ℝ),
  (CompactlySupportedContinuousMap.integralPositiveLinearMap μ) f = ∫ (x : X), f x ∂μ
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
MeasurableEquiv.coe_toLp : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], ⇑(MeasurableEquiv.toLp p X) = WithLp.toLp p
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_lt_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α}, a⁻¹ * b < 1 ↔ b < a
-- Mathlib.Data.List.Sym
List.dedup_sym2 : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α), xs.sym2.dedup = xs.dedup.sym2
-- Std.Data.String.ToNat
String.Slice.toNat?_eq_some_ofDigitChars : ∀ {s : String.Slice},
  s.isNat = true → s.toNat? = some (Nat.ofDigitChars 10 (List.filter (fun x => x != '_') s.copy.toList) 0)
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Rco.Sliceable.mkSlice xs lo...hi).array = xs
-- Lean.Meta.Sym.AlphaShareCommon
/-- When `true`, `shareCommonAlpha` and `shareCommonAlphaInc` throw when hash-consing
a new kernel projection (`Expr.proj`), which the `foldProjs` preprocessing step
should have folded.
 -/
Lean.Meta.Sym.AlphaShareCommon.Context.checkProj : Lean.Meta.Sym.AlphaShareCommon.Context → Bool
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set equals `a` inserted into the strict subset `s'`.  -/
Mathlib.Meta.List.ProveNilOrConsResult.cons : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s : Q(List «$α»)} →
      (a : Q(«$α»)) → (s' : Q(List «$α»)) → Q(«$s» = «$a» :: «$s'») → Mathlib.Meta.List.ProveNilOrConsResult s
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.isInteger_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {a b : S},
  IsLocalization.IsInteger R a → IsLocalization.IsInteger R b → IsLocalization.IsInteger R (a * b)
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.finTwoProd_zero : ∀ (R : Type u_7) [inst : Semiring R], (Module.Basis.finTwoProd R) 0 = (1, 0)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_C_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (a : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff m (MvPolynomial.C a * p) = a * MvPolynomial.coeff m p
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Opens.complOrderIso_apply : ∀ (α : Type u_2) [inst : TopologicalSpace α] (a : TopologicalSpace.Opens α),
  (TopologicalSpace.Opens.complOrderIso α) a = (⇑OrderDual.toDual ∘ TopologicalSpace.Opens.compl) a
-- Plausible.Gen
/-- Error thrown on generation failure, e.g. because you've run out of resources.  -/
Plausible.GenError : Type
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α],
  AddOpposite.instAddSemigroup = { toAdd := AddOpposite.instAdd, add_assoc := ⋯ }
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sZMod.eq_1 : ∀ (p : ℕ), LucasLehmer.sZMod p 0 = 4
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` is a group, then any function from `α` to `α` extends uniquely to a homomorphism from the
free group over `α` to `α`. This is the additive version of `Prod`.  -/
FreeGroup.sum : {α : Type u} → [AddGroup α] → FreeGroup α → α
-- Mathlib.Algebra.Lie.Solvable
_private.Mathlib.Algebra.Lie.Solvable.0.LieAlgebra.derivedAbelianOfIdeal.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvironmentHeader.mk.sizeOf_spec : ∀ (trustLevel : UInt32) (mainModule : Lean.Name) (isModule : Bool) (imports : Array Lean.Import)
  (regions : Array Lean.CompactedRegion) (modules : Array Lean.EffectiveImport)
  (moduleName2Idx : Std.HashMap Lean.Name Lean.ModuleIdx) (importAllModules : Array Lean.EffectiveImport)
  (moduleData : Array Lean.ModuleData),
  sizeOf
      { trustLevel := trustLevel, mainModule := mainModule, isModule := isModule, imports := imports,
        regions := regions, modules := modules, moduleName2Idx := moduleName2Idx, importAllModules := importAllModules,
        moduleData := moduleData } =
    1 + sizeOf trustLevel + sizeOf mainModule + sizeOf isModule + sizeOf imports + sizeOf regions + sizeOf modules +
          sizeOf moduleName2Idx +
        sizeOf importAllModules +
      sizeOf moduleData
-- Init.Data.List.Pairwise
List.Pairwise.filter : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} (p : α → Bool), List.Pairwise R l → List.Pairwise R (List.filter p l)
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.add_eq_add : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G},
  IsCorner A x₁ y₁ x₂ y₂ → x₁ + y₂ = x₂ + y₁
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_sub_mk : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] [inst_2 : Sub α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y),
  ⟨x, hx⟩ - ⟨y, hy⟩ = Nonneg.toNonneg (x - y)
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizationMonoid.mk : {α : Type u_2} →
  [inst : MonoidWithZero α] →
    (normUnit : α → αˣ) →
      normUnit 0 = 1 →
        normUnit 1 = 1 → (∀ {a : α} (u : αˣ), a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a) → NormalizationMonoid α
-- Mathlib.Data.Finsupp.AList
AList.singleton_lookupFinsupp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (m : M), (AList.singleton a m).lookupFinsupp = fun₀ | a => m
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.arrowCongrEquiv_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  {M₄ : Type u_7} [inst_12 : TopologicalSpace M₄] [inst_13 : AddCommMonoid M₄] [inst_14 : Module R₁ M₁]
  [inst_15 : Module R₂ M₂] [inst_16 : Module R₃ M₃] {R₄ : Type u_8} [inst_17 : Semiring R₄] [inst_18 : Module R₄ M₄]
  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [inst_19 : RingHomInvPair σ₃₄ σ₄₃] [inst_20 : RingHomInvPair σ₄₃ σ₃₄]
  {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [inst_21 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
  [inst_22 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_23 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂)
  (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₂ →SL[σ₂₃] M₃), (e₁₂.arrowCongrEquiv e₄₃).symm f = ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.fstX.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j),
  HomologicalComplex.homotopyCofiber.fstX φ i j hij = HomologicalComplex.homotopyCofiber.fstX φ i j hij
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepFun.symm : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'},
  ProbabilityTheory.CondIndepFun m' hm' f g μ → ProbabilityTheory.CondIndepFun m' hm' g f μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filterMap f t) k =
    (Std.ExtDTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
SSet.Subcomplex.evaluation_map : ∀ (X : SSet) (j : SimplexCategoryᵒᵖ) {X_1 Y : X.Subcomplex} (f : X_1 ⟶ Y),
  (SSet.Subcomplex.evaluation X j).map f = CategoryTheory.homOfLE ⋯
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ofHom_apply : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : DistribLattice Y]
  [inst_3 : BoundedOrder Y] (f : BoundedLatticeHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (BddDistLat.ofHom f)) x = f x
-- Mathlib.Order.Filter.Pointwise
/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`.  -/
Filter.mulDistribMulActionFilter : {α : Type u_2} →
  {β : Type u_3} → [inst : Monoid α] → [inst_1 : Monoid β] → [MulDistribMulAction α β] → MulDistribMulAction α (Set β)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.sub : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, f.NeBot → g.NeBot → (f - g).NeBot
-- Mathlib.Order.Bounds.Image
BddBelow.range_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] (g : α → β) {f : α → β},
  (∀ (a : α), g a ≤ f a) → BddBelow (Set.range g) → BddBelow (Set.range f)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.integrable_pow_mul : ∀ {D : Type u_4} {V : Type u_9} [inst : NormedAddCommGroup D] [inst_1 : NormedSpace ℝ D] [inst_2 : NormedAddCommGroup V]
  [inst_3 : NormedSpace ℝ V] [inst_4 : MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth]
  [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) (k : ℕ),
  MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_pow : ∀ {m : Type u_2} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : DecidableEq m] [inst_2 : Fintype o]
  [inst_3 : Fintype m] [inst_4 : Semiring α] (M : o → Matrix m m α) (n : ℕ),
  Matrix.blockDiagonal (M ^ n) = Matrix.blockDiagonal M ^ n