mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.keysArray.toList = m.keys
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_C : ∀ {R : Type u} [inst : Ring R] (r a : R), Polynomial.rootMultiplicity a (Polynomial.C r) = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.associator_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ M₃ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).hom
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.frequently_iff_seq_frequently : ∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
  (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Filter.Tendsto x Filter.atTop l ∧ ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α}, k ∈ Std.DHashMap.Const.insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.annihilator_top_inter_nonZeroDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.IsTorsion R M → (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.instEquivLike : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} → {σ : Representation A G W} → EquivLike (ρ.Equiv σ) V W
-- Batteries.Data.List.Basic
List.tails.eq_2 : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).tails = (a :: l) :: l.tails
-- Init.Data.Array.Attach
Array.pmap_reverse : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ a ∈ xs.reverse, P a),
  Array.pmap f xs.reverse H = (Array.pmap f xs ⋯).reverse
-- Mathlib.Topology.Order.Basic
induced_topology_le_preorder : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace β] [OrderTopology β]
  {f : α → β}, (∀ {x y : α}, f x < f y ↔ x < y) → TopologicalSpace.induced f inst_2 ≤ Preorder.topology α
-- Mathlib.Data.ZMod.Basic
/-- This lemma works in the case in which `ZMod n` is not infinite, i.e. `n ≠ 0`.  The version
where `a ≠ 0` is `addOrderOf_coe'`.  -/
ZMod.addOrderOf_coe : ∀ (a : ℕ) {n : ℕ}, n ≠ 0 → addOrderOf ↑a = n / n.gcd a
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulEquivOfOrderOfEq_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g'),
  (mulEquivOfOrderOfEq hg hg' h) g = g'
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.nonneg : ∀ {X : Type u_1} {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : LinearOrder R] [AddLeftStrictMono R]
  (d : PseudoMetric X R) (x y : X), 0 ≤ d x y
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {a : R},
  AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ↔ ∀ (b : R), Commute a b
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_apply_eq : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (j : n' k), Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.unique_of_ne_zero : ∀ (p q : ENNReal) {r : ENNReal} [p.HolderTriple q r] (q' : ENNReal), r ≠ 0 → ∀ [p.HolderTriple q' r], q = q'
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.one_fromCols_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq m] (A : Matrix m n R),
  (Matrix.fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal.  -/
MonoidWithZeroHomClass.ext_rat' : ∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ M₀] [MonoidWithZeroHomClass F ℚ M₀]
  {f g : F}, (∀ (m : ℤ), f ↑m = g ↑m) → f = g
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.all.eq_1 : ∀ (s : String) (p : Char → Bool), String.Legacy.all s p = !String.Legacy.any s fun c => !p c
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: a continuous function realizes its maximum on a compact set.  -/
IsCompact.exists_isMaxOn : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] {s : Set β}, IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, IsMaxOn f s x
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.fslope.eq_1 : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ), p.fslope n = (p (n + 1)).curryLeft 1
-- Init.Data.SInt.Lemmas
Int64.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < 2 ^ 63 → b < 2 ^ 63 → (Int64.ofNat a < Int64.ofNat b ↔ a < b)
-- Mathlib.Data.Multiset.Bind
Multiset.le_bind : ∀ {α : Type u_4} {β : Type u_5} {f : α → Multiset β} (S : Multiset α) {x : α}, x ∈ S → f x ≤ S.bind f
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_smul : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] {S : Type u_10} [inst_7 : TopologicalSpace W] [inst_8 : Monoid S]
  [inst_9 : DistribMulAction S W] [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] (t : S)
  (f : P →ᴬ[R] W), ⇑(t • f) = t • ⇑f
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- If two functions agree in a neighborhood of a point, then so do their Laplacians.
 -/
InnerProductSpace.laplacian_congr_nhds : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  f₁ =ᶠ[nhds x] f₂ → Laplacian.laplacian f₁ =ᶠ[nhds x] Laplacian.laplacian f₂
-- Mathlib.Data.Set.Function
Function.Semiconj.injOn_range : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → Function.Injective fa → Set.InjOn f (Set.range fa) → Set.InjOn fb (Set.range f)
-- Lean.Elab.MutualInductive
/-- Elaborates a `mutual` block, assuming the commands satisfy `Lean.Elab.Command.isMutualInductive`.
 -/
Lean.Elab.Command.elabMutualInductive : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, m.size - 1 ≤ (m.alter k f).size
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Submodule.complementedLattice : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ComplementedLattice (Submodule K V)
-- Mathlib.Order.CompleteLattice.Basic
Prod.infSet.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : InfSet α] [inst_1 : InfSet β],
  Prod.infSet α β = { sInf := fun s => (sInf (Prod.fst '' s), sInf (Prod.snd '' s)) }
-- Init.Data.UInt.Bitwise
UInt32.shiftRight_or : ∀ {a b c : UInt32}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Init.Data.UInt.IntToBitVec
USize.le_iff_toBitVec64_le : ∀ {a b : USize} (h : System.Platform.numBits = 64), a ≤ b ↔ a.toBitVec64 h ≤ b.toBitVec64 h
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.zero_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), Representation.IntertwiningMap.toLinearMap 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iio_add_Iic_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iio a + Finset.Iic b ⊆ Finset.Iio (a + b)
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- `R` is a right adjoint  -/
CategoryTheory.Reflective.adj : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {R : CategoryTheory.Functor D C} → [self : CategoryTheory.Reflective R] → CategoryTheory.Reflective.L R ⊣ R
-- Init.Data.FloatArray.Basic
FloatArray.toList : FloatArray → List Float
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The type of finite measures is a measurable space when equipped with the Giry monad.  -/
MeasureTheory.FiniteMeasure.instMeasurableSpace : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasurableSpace (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.Algebra.Ring.Commute
Commute.sub_sq : ∀ {R : Type u} [inst : Ring R] {a b : R}, Commute a b → (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.property : Lean.Lsp.SymbolKind
-- Init.Data.SInt.Lemmas
Int64.not_maxValue_lt : ∀ {a : Int64}, ¬Int64.maxValue < a
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_domDomCongr : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (f : M [⋀^ι]→ₗ[R] N) (σ : ι ≃ ι'),
  ↑(AlternatingMap.domDomCongr σ f) = MultilinearMap.domDomCongr σ ↑f
-- Mathlib.Data.Nat.DvdSequence
smul_dvd_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : SMul α β] [IsScalarTower α β β]
  [IsScalarTower α α β] [SMulCommClass α β β] {a b : α} {c d : β}, a ∣ b → c ∣ d → a • c ∣ b • d
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_add : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p q : Polynomial R}
  (x : A), (Polynomial.aeval x) (p + q) = (Polynomial.aeval x) p + (Polynomial.aeval x) q
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α β : Type u_1} →
    [inst : Std.Iterator α m β] →
      (it : Std.IterM m β) →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.LinearAlgebra.Matrix.Trace
/-- The trace of a square matrix. For more bundled versions, see:
* `Matrix.traceAddMonoidHom`
* `Matrix.traceLinearMap`
 -/
Matrix.trace : {n : Type u_3} → {R : Type u_6} → [Fintype n] → [AddCommMonoid R] → Matrix n n R → R
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- Note that if `n = m = 0` then `resultant = 1` but `f` and `g` aren't necessarily coprime.  -/
Polynomial.exists_mul_add_mul_eq_C_resultant : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  f.natDegree ≤ m →
    g.natDegree ≤ n →
      m ≠ 0 ∨ n ≠ 0 → ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = Polynomial.C (f.resultant g m n)
-- Mathlib.Algebra.Group.Ideal
/-- The additive semigroup ideal generated by a set `s`.  -/
AddSemigroupIdeal.closure : {M : Type u_1} → [inst : Add M] → Set M → AddSemigroupIdeal M
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_of_top_eq_bot : ∀ (G : Type u_1) [inst : Group G], ⊤ = ⊥ → Group.IsSolvable G
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseIdList : Std.Internal.Parsec.ByteArray.Parser (Array ℕ)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character is nontrivial as a multiplicative character
when the domain has odd characteristic.  -/
quadraticChar_ne_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], ringChar F ≠ 2 → quadraticChar F ≠ 1
-- Mathlib.Order.PropInstances
Prop.isCompl_iff : ∀ {P Q : Prop}, IsCompl P Q ↔ ¬(P ↔ Q)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂ δ).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ((δ.app X₁).app X₂) (F.obj X₃)
-- Init.Data.Int.OfNat
Nat.ToInt.toNat_nonneg : ∀ (x : ℕ), -1 * ↑x ≤ 0
-- Mathlib.RingTheory.Algebraic.Integral
Transcendental.extendScalars_of_isIntegral : ∀ {R : Type u_1} (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] {a : A},
  Transcendental R a → ∀ [Algebra.IsIntegral R S], Transcendental S a
-- Mathlib.Algebra.GCDMonoid.Multiset
Mathlib.Tactic.TermCongr.cHole.congr_simp : ∀ {α : Sort u} (val val_1 : α), val = val_1 → ∀ {p p_1 : Prop} (e_p : p = p_1) (_pf : p), val = val_1
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.seq_apply : ∀ {α : Type u_1} {β : Type u_2} (q : PMF (α → β)) (p : PMF α) (b : β),
  (q.seq p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mkIso'_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom], (CategoryTheory.AddMon.mkIso' e).inv.hom = e.inv
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α} {fallback : β},
  (↑m).WF →
    ∀ {f : Option β → Option β},
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k fallback =
        (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence. We denote it `α →ᵤ β`.  -/
UniformConvergence.«term_→ᵤ_» : Lean.TrailingParserDescr
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.toMul : {α : Type u} → [self : Lean.Grind.Semiring α] → Mul α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_card_nsmul : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} {b : M},
  (∀ a ∈ s, f a = b) → ∑ a ∈ s, f a = s.card • b
-- Mathlib.Algebra.GroupWithZero.Range
/-- For a morphism of monoids with zero `f`, this is the smallest subgroup of the invertible
elements in the codomain containing the range of `f`.  -/
MonoidWithZeroHom.valueGroup : {A : Type u_1} → {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : MonoidWithZero B] → (A →*₀ B) → Subgroup Bˣ
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_lift_OptionT_apply_eq : ∀ {Pred : Type u} {EPred : Type u_1} {ε : Type u} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {α : Type u} {post : α → Pred}
  {epost : EPost.Cons✝ Pred EPred} (x : OptionT m α) (h : ε → OptionT m α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost =
    Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.toList : {α : Type u} → {β : α → Type v} → Std.DHashMap.Internal.AssocList α β → List ((a : α) × β a)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofMacroExpansionInfo : Lean.Elab.MacroExpansionInfo → Lean.Elab.Info
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_self_of_mem`. -/
Set.insert_diff_self_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → insert a (s \ {a}) = s
-- Init.Data.Nat.Basic
Nat.sub_add_eq : ∀ (a b c : ℕ), a - (b + c) = a - b - c
-- Std.Data.DHashMap.Basic
/-- Returns a list of all keys present in the hash map in some order.  -/
Std.DHashMap.keys : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → List α
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The projection from `φ` to `S ⊗[R] M`.  -/
PolynomialLaw.π : (R : Type u) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type v) →
            [inst_3 : CommSemiring S] → [inst_4 : Algebra R S] → PolynomialLaw.lifts R M S → TensorProduct R S M
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.coverPreserving : ∀ {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] (F : CategoryTheory.Functor C D) [inst_2 : F.PreservesEffectiveEpis]
  [inst_3 : F.ReflectsEffectiveEpis] [inst_4 : F.Full] [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough]
  [inst_7 : CategoryTheory.Preregular D],
  CategoryTheory.CoverPreserving (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D) F
-- Std.Do.PostCond
Std.Do.ExceptConds.and_imp : ∀ {ps : Std.Do.PostShape} {x₁ x₂ : Std.Do.ExceptConds ps}, (x₁ ∧ₑ (x₁ →ₑ x₂)).entails (x₁ ∧ₑ x₂)
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.root : Lean.Elab.ConfigEval.ConfigItem → Lean.Syntax
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- Abbreviation for face maps in the `n`-truncated simplex category.  -/
SimplexCategory.Truncated.δ : (m : ℕ) →
  {n : ℕ} →
    Fin (n + 2) →
      (hn : autoParam ({ len := n }.len ≤ m) SimplexCategory.Truncated.δ._auto_1) →
        (hn' : autoParam ({ len := n + 1 }.len ≤ m) SimplexCategory.Truncated.δ._auto_3) →
          { obj := { len := n }, property := hn } ⟶ { obj := { len := n + 1 }, property := hn' }
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_arrow_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.IsEquivalence] [R.IsInduced] [L.functor.IsEquivalence]
  [W₂'.RespectsIso] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.arrow.HasLeftResolutions ↔ B.arrow.HasLeftResolutions
-- Mathlib.Topology.Sheaves.Stalks
/-- Let `F` and `G` be sheaves valued in a concrete category, whose forgetful functor reflects
isomorphisms, preserves limits and filtered colimits. Then if the stalk maps of a morphism
`f : F ⟶ G` are all isomorphisms, `f` must be an isomorphism.
 -/
TopCat.Presheaf.isIso_of_stalkFunctor_map_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G)
  [∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.hom)], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.homOfLe_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  {G G' : CategoryTheory.Subfunctor F} (h : G ≤ G'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe h) G'.ι = G.ι
-- Mathlib.Order.Filter.Finite
/-- Any filter on a finite type is principal.  -/
Filter.eq_principal_of_finite : ∀ {α : Type u} [Finite α] (f : Filter α), ∃ s, f = Filter.principal s
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ →
    P.IsPrime →
      P ≠ ⊥ →
        p.ramificationIdx' P =
          Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) p))
-- Mathlib.Algebra.Ring.SumsOfSquares
NonUnitalSubsemiring.mem_sumSq : ∀ {T : Type u_2} [inst : NonUnitalCommSemiring T] {s : T}, s ∈ NonUnitalSubsemiring.sumSq T ↔ IsSumSq s
-- Batteries.Lean.PersistentHashMap
/-- Builds a `PersistentHashMap` from a list of key-value pairs. Values of
duplicated keys are replaced by their respective last occurrences.
 -/
Lean.PersistentHashMap.ofList : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → List (α × β) → Lean.PersistentHashMap α β
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.ext : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  {x y : B.IsBilimit}, x.isLimit = y.isLimit → x.isColimit = y.isColimit → x = y
-- Mathlib.Combinatorics.Matroid.Constructions
/-- The `Matroid α` with ground set `E` whose only base is `E`.  -/
Matroid.freeOn : {α : Type u_1} → Set α → Matroid α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- For 0 < x, we have sin x < x.  -/
Real.sin_lt : ∀ {x : ℝ}, 0 < x → Real.sin x < x