mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.UnsatProof
-- Mathlib.Algebra.Module.Torsion.Basic
/-- Quotienting by the torsion submodule gives a torsion-free module.  -/
Submodule.QuotientTorsion.torsion_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Submodule.torsion R (M ⧸ Submodule.torsion R M) = ⊥
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ),
  (↑(CochainComplex.cocycleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ)
            (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ))).v
      p (p + 1) ⋯ =
    -φ.f (p + { as := 1 }.as)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.eq_of_mem_uIcc_of_mem_uIcc' : ∀ {α : Type u_1} [inst : DistribLattice α] {a b c : α}, b ∈ Set.uIcc a c → c ∈ Set.uIcc a b → b = c
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'Aux_eq : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁), M.toBilin'Aux = Matrix.toBilin' M
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Permuting rows and columns with two equivalences does not change the absolute value of the
determinant.  -/
Matrix.abs_det_submatrix_equiv_equiv : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type u_3} [inst_4 : CommRing R] [inst_5 : LinearOrder R] [IsStrictOrderedRing R]
  (e₁ e₂ : n ≃ m) (A : Matrix m m R), |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|
-- Init.Data.String.Slice
String.Slice.instDecidableLt : (x y : String.Slice) → Decidable (x < y)
-- Mathlib.Algebra.Group.Prod
Prod.instSemigroup.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Semigroup M] [inst_1 : Semigroup N],
  Prod.instSemigroup = { toMul := Prod.instMul, mul_assoc := ⋯ }
-- Init.Data.Rat.Basic
/-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is
`@[irreducible]` because you don't want to unfold it. Use `Rat.ofScientific_def`,
`Rat.ofScientific_true_def`, or `Rat.ofScientific_false_def` instead.)  -/
Rat.ofScientific : ℕ → Bool → ℕ → ℚ
-- Mathlib.Analysis.Convex.Extreme
/-- A point `x` is an extreme point of a set `A` if `x` belongs to no open segment with ends in
`A`, except for the obvious `openSegment x x`.  -/
Set.extremePoints : (𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Set E
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul.sizeOf_spec : ∀ (a? : Option Lean.Expr) (cs : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a? cs) = 1 + sizeOf a? + sizeOf cs
-- Lean.Util.Sorry
Lean.Declaration.hasSyntheticSorry : Lean.Declaration → Bool
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.projectionOnto_of_proj`. -/
LinearMap.linearProjOfIsCompl_of_proj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  (f : E →ₗ[R] ↥p) (hf : ∀ (x : ↥p), f ↑x = x), p.projectionOnto f.ker ⋯ = f
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_image2_eq_csInf_csInf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sInf s) (sInf t)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_eq_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α], m.WF → ∀ {a : α} {h : a ∈ m}, Std.DHashMap.Raw.Const.get m a h = m.get a h
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.not_gt_of_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b → ¬Std.PRange.UpwardEnumerable.LT b a
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instCompactSpaceSubtypeMem : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] (H : ClosedAddSubgroup G),
  CompactSpace ↥H
-- Mathlib.Data.Seq.Defs
/-- The sequence of natural numbers some 0, some 1, ...  -/
Stream'.Seq.nats : Stream'.Seq ℕ
-- Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
CategoryTheory.Functor.PushoutObjObj.flipTensor_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}
  (sq : (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂), sq.flipTensor.pt = sq.pt
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ε : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  (Std.Do.wp (MonadLift.monadLift x)).apply Q = (Std.Do.wp x).apply (fun a => Q.1 a, Q.2.2)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.hasNum : Lean.Name → Bool
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`.
Let `f : ℂ → E` be a function such that

* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |im z|))` on `U` for some `c < π / (b - a)`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of `U`.

Then `‖f z‖` is bounded by the same constant on the closed strip
`{z : ℂ | a ≤ re z ≤ b}`. Moreover, it suffices to verify the second assumption
only for sufficiently large values of `|im z|`.
 -/
PhragmenLindelof.vertical_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.im|))) →
      (∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C) → a ≤ z.re → z.re ≤ b → ‖f z‖ ≤ C
-- Mathlib.Control.Fold
Traversable.Free.map_eq_map : ∀ {α β : Type u} (f : α → β) (xs : List α), f <$> xs = FreeMonoid.toList ((FreeMonoid.map f) (FreeMonoid.ofList xs))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.refl : ∀ {α : Type u_2} (f : Equiv.Perm α) (x : α), f.SameCycle x x
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_sUnion : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (a : α) (S : Set (Set β)), a • ⋃₀ S = ⋃ s ∈ S, a • s
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_ExceptT_eq : ∀ {m : Type u_1 → Type u_2} {α ρ : Type u_1} {p : α → Prop} {x : ExceptT ρ m α} [inst : Monad m] [LawfulMonad m],
  SatisfiesM p x ↔ SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x.run
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (X : CategoryTheory.Functor C V),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.functorL₁.map f = f.f₁
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff_pow_le : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) [NoZeroDivisors R] (n : ℕ),
  I.leadingCoeff ^ n ≤ (I ^ n).leadingCoeff
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasis'_gen : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic),
  (AdjoinRoot.powerBasis' hg).gen = AdjoinRoot.root g
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_insert_closure_eq : ∀ {α : Type u_1} (M : Matroid α) (e : α) (X : Set α), M.eRk (insert e (M.closure X)) = M.eRk (insert e X)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeCheckInstances : Lean.Options → Bool
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.addLeft_apply : ∀ {α : Type u_2} [inst : Add α] [inst_1 : LinearOrder α] [inst_2 : AddLeftStrictMono α] (m n : α),
  (OrderEmbedding.addLeft m) n = m + n
-- Mathlib.Data.Nat.Pairing
Nat.pair_lt_pair_right : ∀ (a : ℕ) {b₁ b₂ : ℕ}, b₁ < b₂ → Nat.pair a b₁ < Nat.pair a b₂
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_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}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c')
  {Z : D} (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d' c' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d' g) h)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The kernel of the norm map on `ℤ√d` equals the submonoid of unitary elements.  -/
Zsqrtd.mker_norm_eq_unitary : ∀ {d : ℤ}, MonoidHom.mker Zsqrtd.normMonoidHom = unitary (ℤ√d)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [LawfulMonad m] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ},
  (Std.Iter.mapWithPostcondition f it).toList = List.mapM (fun x => (f x).run) it.toList
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_of_edge : ∀ {V : SSet.Truncated 2} {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e : SSet.Truncated.Edge x y),
  SSet.Truncated.HomotopyCategory.morphismPropertyHomMk V (SSet.Truncated.HomotopyCategory.homMk e)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → p.reverse.IsPath
-- Lean.Meta.Tactic.Try.Collect
/-- Function induction candidates  -/
Lean.Meta.Try.Collector.Result.funIndCandidates : Lean.Meta.Try.Collector.Result → Lean.Meta.FunInd.SeenCalls
-- Init.Data.Int.Order
Int.succ_ofNat_pos : ∀ (n : ℕ), 0 < ↑n + 1
-- Mathlib.CategoryTheory.Products.Basic
/-- The product `F.prod' G` followed by projection on the second component is isomorphic to `G`  -/
CategoryTheory.Functor.prod'CompSnd : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor A C) → (F.prod' G).comp (CategoryTheory.Prod.snd B C) ≅ G
-- Aesop.Stats.Basic
Aesop.MonadStats.modifyGetStats : {m : Type → Type} → [self : Aesop.MonadStats m] → {α : Type} → (Aesop.Stats → α × Aesop.Stats) → m α
-- Mathlib.Data.Nat.Factorization.Defs
Nat.dvd_iff_exists_le_factorization : ∀ {n d : ℕ}, d ≠ 0 → n ≠ 0 → (d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 => x1 ^ x2)
-- Mathlib.Data.ENat.Basic
instCommSemiringENat : CommSemiring ℕ∞
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.mem_verticalStrip_iff : ∀ (A B : ℝ) (z : UpperHalfPlane), z ∈ UpperHalfPlane.verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im
-- Init.Data.Nat.Gcd
Nat.gcd_ne_zero_right : ∀ {n m : ℕ}, n ≠ 0 → m.gcd n ≠ 0
-- Mathlib.MeasureTheory.SetAlgebra
/-- If a family of sets `𝒜` is contained in `ℬ`, then the algebra of sets generated by `𝒜`
is contained in the one generated by `ℬ`.  -/
MeasureTheory.generateSetAlgebra_mono : ∀ {α : Type u_1} {𝒜 ℬ : Set (Set α)}, 𝒜 ⊆ ℬ → MeasureTheory.generateSetAlgebra 𝒜 ⊆ MeasureTheory.generateSetAlgebra ℬ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The complex sine function is everywhere differentiable, with the derivative `cos x`.  -/
Complex.hasDerivAt_sin : ∀ (x : ℂ), HasDerivAt Complex.sin (Complex.cos x) x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'.go : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Mon → α → α
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_comp_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom) h)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_id : ∀ {σ : Type u_1} {S : Type u_2} [inst : CommSemiring S], MvPolynomial.aevalTower (AlgHom.id S S) = MvPolynomial.aeval
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.null : Lean.Lsp.SymbolKind
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toLimitFun_continuous : ∀ (P : ProfiniteGrp.{u}), Continuous ⇑P.toLimitFun
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceAddOpposite : {α : Type ua} → [UniformSpace α] → UniformSpace αᵃᵒᵖ
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.le_zpowers_iff : ∀ {G : Type u_2} [inst : Group G] (g : G) (H : Subgroup G), H ≤ Subgroup.zpowers g ↔ ∃ n, H = Subgroup.zpowers (g ^ n)
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- This condition alongside the others is enough to conclude `o.cof.ord = a`, see
`IsFundamentalSeq.ord_cof`.  -/
Ordinal.IsFundamentalSeq.le_ord_cof : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → a ≤ o.cof.ord
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RooSliceData α β)) Id (Std.DTreeMap.Internal.RxoIterator α β)
        ((a : α) × β a)
-- Mathlib.Data.Set.Image
Set.subset_image_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Surjective f → (f '' s)ᶜ ⊆ f '' sᶜ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.cellFrontier n i ∪ Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.closedCell n i
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} → {b : H} → (toFun : G → H) → (∀ (x : G), toFun (x + a) = toFun x + b) → AddConstMap G H a b
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.limsup_const_sub : ∀ {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) {c : ENNReal},
  c ≠ ⊤ → Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
-- Mathlib.Order.Disjoint
disjoint_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a : α}, Disjoint a ⊤ ↔ a = ⊥
-- Init.Guard
/-- Default-reducibility defeq matching for `guard_hyp` values  -/
Lean.Parser.colonEqD : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.Q (q + 1) =
    AlgebraicTopology.DoldKan.Q q -
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (AlgebraicTopology.DoldKan.Hσ q)
-- Mathlib.Algebra.Ring.Defs
Ring.toNonUnitalRing : {α : Type u} → [Ring α] → NonUnitalRing α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimits.has_colimits_of_shape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (J : Type v)
  [inst_2 : CategoryTheory.Category.{v, v} J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
measurableSet_insert : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {a : α} {s : Set α},
  MeasurableSet (insert a s) ↔ MeasurableSet s
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.smul_starProjection_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : E} (w : E), ↑(‖v‖ ^ 2) • (𝕜 ∙ v).starProjection w = inner 𝕜 v w • v
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.algebraMap_mem_iff : ∀ (S : Type u_1) {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : A} {r : R},
  (algebraMap R S) r ∈ spectrum S a ↔ r ∈ spectrum R a
-- Mathlib.Data.List.Rotate
List.IsRotated.symm : ∀ {α : Type u} {l l' : List α}, l ~r l' → l' ~r l
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.getSimpMatchContext : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Algebra.Group.AddChar
MonoidHom.compAddChar_injective_left : ∀ {A : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddMonoid A] [inst_1 : Monoid M] [inst_2 : Monoid N]
  (ψ : AddChar A M), Function.Surjective ⇑ψ → Function.Injective fun f => f.compAddChar ψ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.alter_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} (f : Option (β k) → Option (β k)), (↑(m₁.alter k f)).Equiv ↑(m₂.alter k f)
-- Mathlib.RingTheory.Localization.Module
LinearEquiv.extendScalarsOfIsLocalizationEquiv_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (e : M ≃ₗ[R] N),
  (LinearEquiv.extendScalarsOfIsLocalizationEquiv S A) e = LinearEquiv.extendScalarsOfIsLocalization S A e
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_le_beth : ∀ (o : Ordinal.{u_1}), Cardinal.preBeth o ≤ Cardinal.beth o
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X : B} (M : P.Obj X),
  (P.mapId X).hom.app M = CategoryTheory.ObjectProperty.homMk ((F.mapId X).hom.toNatTrans.app M.obj)
-- Lean.Parser.Extra
Lean.Parser.rawIdent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_iSup_of_directed : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} [Nonempty ι] {S : ι → AddSubgroup G},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_sum_type : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid M]
  (f : α₁ ⊕ α₂ → M), ∑ x, f x = ∑ a₁, f (Sum.inl a₁) + ∑ a₂, f (Sum.inr a₂)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in any chart containing that point. Version requiring differentiability
in the target instead of `range I`.  -/
mdifferentiableWithinAt_iff_of_mem_source' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'] {x' : M} {y : M'},
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (MDiffAt[s] f x' ↔
        ContinuousWithinAt f s x' ∧
          DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
            (↑(extChartAt I x) x'))
-- Init.Data.String.Lemmas.FindPos
String.posLE_eq_posLE_toSlice : ∀ {s : String} {p : String.Pos.Raw}, s.posLE p = String.Pos.ofToSlice (s.toSlice.posLE p)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKey? k = none
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- If `f` lies in a closed convex set `s` a.e., then `μ[f | m]` lies in `s` a.e.  -/
Convex.condExp_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable f μ → IsClosed s → Convex ℝ s → (∀ᵐ (a : α) ∂μ, f a ∈ s) → ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
-- Init.Grind.Norm
Lean.Grind.bne_eq_decide_not_eq : ∀ {α : Type u_1} {x : BEq α} [LawfulBEq α] [inst : DecidableEq α] (a b : α), (a != b) = decide ¬a = b
-- Mathlib.RingTheory.ReesAlgebra
mem_reesAlgebra_iff : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (f : Polynomial R), f ∈ reesAlgebra I ↔ ∀ (i : ℕ), f.coeff i ∈ I ^ i
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstLENat : Lean.Expr → Lean.MetaM Bool
-- Std.Http.Data.Status
Std.Http.Status.alreadyReported.sizeOf_spec : sizeOf Std.Http.Status.alreadyReported = 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
TopologicalSpace.Opens.map.eq_1 : ∀ {X Y : TopCat} (f : X ⟶ Y), TopologicalSpace.Opens.map f = (↑(TopCat.Hom.frameHom f)).toFunctor