mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filterMap_eq_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a},
  Std.ExtDTreeMap.filterMap (fun k v => some (f k v)) t = Std.ExtDTreeMap.map f t
-- Mathlib.Logic.Relation
Relation.transGen_iff : ∀ {α : Sort u} (r : α → α → Prop) (a a_1 : α),
  Relation.TransGen r a a_1 ↔ r a a_1 ∨ ∃ b, Relation.TransGen r a b ∧ r b a_1
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι)
  (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n : ℤ) (hn : n = data.deg pq),
  X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n hn =
    X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n hn
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.ciSup_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Set ι},
  s.Finite → (∃ x ∈ s, sSup ∅ ≤ f x) → ⨆ i ∈ s, f i ∈ f '' s
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.orderBot : {α : Type u_1} → OrderBot (MeasureTheory.OuterMeasure α)
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.positive : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(GroupWithZero «$M»)} →
      (iM' : Q(PartialOrder «$M»)) →
        Q(PosMulStrictMono «$M») →
          Q(PosMulReflectLT «$M») → Q(ZeroLEOneClass «$M») → Mathlib.Tactic.FieldSimp.DenomCondition iM
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty →
    ∀ {K : Set G} (h1K : IsCompact K),
      (interior K).Nonempty → 0 < MeasureTheory.Measure.haar.prehaar (↑K₀) U { carrier := K, isCompact' := h1K }
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C], CategoryTheory.IsPushout f g h i → ∀ [CategoryTheory.Mono f], CategoryTheory.Mono i
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.symm_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.symm.source = e.target
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : List (α × β)}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).size ≤ (↑m).size + l.length
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_intro_r : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊢ₛ Q) → P ⊢ₛ P ∧ Q
-- Mathlib.Algebra.Order.Floor.Div
le_smul_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] {a : α} {b : β},
  0 < a → b ≤ a • (b ⌈/⌉ a)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Simultaneous multiplication on the left and right is a linear map.  -/
LinearMap.mulLeftRight : (R : Type u_14) →
  {A : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → A × A → A →ₗ[R] A
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  ((CategoryTheory.Idempotents.toKaroubi C).obj X).decompId_p =
    CategoryTheory.CategoryStruct.id
      { X := ((CategoryTheory.Idempotents.toKaroubi C).obj X).X,
        p := CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X).X, idem := ⋯ }
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.other.inj : ∀ {key key_1 : Lean.Name}, Mathlib.Notation3.DelabKey.other key = Mathlib.Notation3.DelabKey.other key_1 → key = key_1
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atBot_prod_self' : ∀ {α : Type u_3} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {p : α × α → Prop},
  (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_lt_prod_of_subset' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s t : Finset ι} [MulLeftStrictMono M],
  s ⊆ t → ∀ {i : ι}, i ∈ t → i ∉ s → 1 < f i → (∀ j ∈ t, j ∉ s → 1 ≤ f j) → ∏ j ∈ s, f j < ∏ j ∈ t, f j
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instInfSet.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instInfSet =
    {
      sInf := fun S =>
        { toTopologicalSpace := sInf (GroupTopology.toTopologicalSpace '' S), toIsTopologicalGroup := ⋯ } }
-- Mathlib.Order.Hom.Bounded
BotHomClass.toBotHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Bot α] [inst_2 : Bot β]
  [inst_3 : BotHomClass F α β] (f : F), ↑f = { toFun := ⇑f, map_bot' := ⋯ }
-- Init.Data.Iterators.Basic
/-- The constructor has been renamed.  -/
Std.IterM.mk' : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → α → Std.IterM m β
-- Mathlib.Data.Rat.Lemmas
Rat.sub_ofNat_den : ∀ (q : ℚ) (n : ℕ), (q - OfNat.ofNat n).den = q.den
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.zpow : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f : α → 𝕜} {g : α → 𝕜'}, f =Θ[l] g → ∀ (n : ℤ), (fun x => f x ^ n) =Θ[l] fun x => g x ^ n
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition that a functor `F` has a pointwise left Kan extension along `L`: it means
that it has a pointwise left Kan extension at any object.  -/
CategoryTheory.Functor.HasPointwiseLeftKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → Prop
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.smulAux.eq_1 : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  UpperHalfPlane.smulAux g z = { coe := UpperHalfPlane.smulAux' g ↑z, coe_im_pos := ⋯ }
-- Mathlib.Tactic.Push.Attr
/-- The type for a constant to be pushed by `push`.  -/
Mathlib.Tactic.Push.Head : Type
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftMinusInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.minus.IsStableUnderShift ℤ
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_const_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (b : β),
  ‖BoundedContinuousFunction.const α b‖₊ ≤ ‖b‖₊
-- Mathlib.Algebra.Ring.ULift
ULift.up_intCast : ∀ {R : Type u} [inst : IntCast R] (n : ℤ), { down := ↑n } = ↑n
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.down_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.AsSmall C} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : C} (h : Z.down ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).down h =
    CategoryTheory.CategoryStruct.comp f.down (CategoryTheory.CategoryStruct.comp g.down h)
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.eulerPoint_mem_ninePointCircle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.eulerPoint i ∈ s.ninePointCircle
-- Init.Data.Nat.Div.Lemmas
Nat.div_le_div : ∀ {a b c d : ℕ}, a ≤ b → d ≤ c → d ≠ 0 → a / c ≤ b / d
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.not_dvd_one : ∀ {p : ℕ}, Nat.Prime p → ¬p ∣ 1
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.succ.match_1.splitter : {n : ℕ} → (motive : Fin n → Sort u_1) → (x : Fin n) → ((i : ℕ) → (h : i < n) → motive ⟨i, h⟩) → motive x
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- The power series for `1 / (u - x)`.  -/
PowerSeries.invUnitsSub : {R : Type u_1} → [inst : Ring R] → Rˣ → PowerSeries R
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.mkPureUnit : Lean.MacroM Lean.Syntax
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote'_eq_denote : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote ctx p
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.Data.Rat.Floor
Rat.isNat_intCeil : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat ⌈r⌉ m
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- If `p` lies on the perpendicular bisector of `ab` and `b` is strictly between `a` and `c`,
then `p` is closer to `b` than to `c`.  -/
EuclideanGeometry.dist_lt_of_sbtw_of_mem_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p : P}, Sbtw ℝ a b c → p ∈ AffineSubspace.perpBisector a b → dist p b < dist p c
-- Mathlib.Algebra.Order.Group.Defs
inv_lt_self_iff : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a⁻¹ < a ↔ 1 < a
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `smul_lt_smul_of_pos_left` instead.  -/
PosSMulStrictMono.smul_lt_smul_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  [self : PosSMulStrictMono α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, b₁ < b₂ → a • b₁ < a • b₂
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f g : α → E),
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) → f =ᵐ[μ] g
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.drop_of_drop : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n k : ℕ} {p : G.Walk u v}, (p.drop k).IsPath → k ≤ n → (p.drop n).IsPath
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If `p₃` bisects the angle `∡ p₁ p₂ p₄`, and `p₃` and `p₄` lie on opposite sides of the line
`p₁ p₂`, then the unoriented angle `∠ p₁ p₂ p₃` is `π` minus half `∠ p₁ p₂ p₄`.  -/
EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  p₁ ≠ p₂ →
    EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ →
      line[ℝ, p₁, p₂].SOppSide p₃ p₄ → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi - EuclideanGeometry.angle p₁ p₂ p₄ / 2
-- Mathlib.Data.Set.Prod
Set.update_mem_pi_iff_of_mem : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [inst : DecidableEq ι] {a : (i : ι) → α i}
  {i : ι} {b : α i}, a ∈ s.pi t → (Function.update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive.go.match_1.splitter : (motive : Option ℕ → Sort u_1) →
  (x : Option ℕ) →
    ((val : ℕ) → motive (some val)) → ((x : Option ℕ) → (∀ (val : ℕ), x = some val → False) → motive x) → motive x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.commIsometry_trans_ridIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (TensorProduct.commIsometry 𝕜 𝕜 E).trans (TensorProduct.ridIsometry 𝕜 E) = TensorProduct.lidIsometry 𝕜 E
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_prod : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R),
  MvPolynomial.eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, MvPolynomial.eval₂ f g (p x)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d),
  ∃! i,
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (y.cast ⋯).simplex =
      (x.cast hd).simplex
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fractRestrict.eq_1 : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (x : E), ZSpan.fractRestrict b x = ⟨ZSpan.fract b x, ⋯⟩
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.instCoalgebra : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Module R A] → [Coalgebra R A] → Coalgebra R (LaurentPolynomial A)
-- Mathlib.Tactic.CongrExclamation
/-- Whether to use a special congruence lemma for `BEq` instances.
This synthesizes `LawfulBEq` instances to discharge equalities of `BEq` instances.  -/
Congr!.Config.beqEq : Congr!.Config → Bool
-- Mathlib.Combinatorics.Graph.Simple
Graph.Loopless.anti : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β} [hG : G.Loopless], H ≤ G → H.Loopless
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.visitedToken : Lean.PrettyPrinter.Parenthesizer.State → Bool
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.erase.match_1.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : Option (Fin as.size) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (i : Fin as.size) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv.eq_1 : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R],
  MvPolynomial.sumAlgEquiv R S₁ S₂ =
    (AddMonoidAlgebra.domCongr R R Finsupp.sumFinsuppAddEquivProdFinsupp).trans (AddMonoidAlgebra.curryAlgEquiv R)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instDecidableEqDecl : {α : Type} → [DecidableEq α] → DecidableEq (Std.Sat.AIG.Decl α)
-- Init.Data.Format.Basic
Std.Format.instBEqFlattenAllowability.beq : Std.Format.FlattenAllowability → Std.Format.FlattenAllowability → Bool
-- Mathlib.Data.Finset.Basic
Finset.disjoint_of_erase_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ t → Disjoint (s.erase a) t → Disjoint s t
-- Mathlib.Topology.Order.LeftRight
nhdsGE_sup_nhdsLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Ici a) ⊔ nhdsWithin a (Set.Iic a) = nhds a
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eventualRange_eq_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J}
  [CategoryTheory.IsCofilteredOrEmpty J] {f : i ⟶ j},
  F.eventualRange j = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⊆
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp g f)))
-- Init.Data.UInt.Lemmas
UInt8.lt_add_one : ∀ {c : UInt8}, c ≠ -1 → c < c + 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.filter! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).WF
-- Lean.Data.Position
Lean.Position.column : Lean.Position → ℕ
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- Variant of `Pseudofunctor.LocallyDiscreteOpToCat.pullHom` when we have
chosen pullbacks.  -/
CategoryTheory.Pseudofunctor.DescentData'.pullHom' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })} →
                  ((i j : ι) →
                      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶
                        (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)) →
                    ⦃Y : C⦄ →
                      (q : Y ⟶ S) →
                        ⦃i₁ i₂ : ι⦄ →
                          (f₁ : Y ⟶ X i₁) →
                            (f₂ : Y ⟶ X i₂) →
                              autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                                  CategoryTheory.Pseudofunctor.DescentData'.pullHom'._auto_1 →
                                autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                                    CategoryTheory.Pseudofunctor.DescentData'.pullHom'._auto_3 →
                                  ((F.map f₁.op.toLoc).toFunctor.obj (obj i₁) ⟶
                                    (F.map f₂.op.toLoc).toFunctor.obj (obj' i₂))
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Factorized rational functions are meromorphic in normal form on arbitrary subsets of `𝕜`.
 -/
Function.FactorizedRational.meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ) (U : Set 𝕜),
  MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) U
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Dep.nonempty : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D → D.Nonempty
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorComm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (m : M) (n : N) (p : P)
  (q : Q), (TensorProduct.tensorTensorTensorComm R M N P Q) (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) = m ⊗ₜ[R] p ⊗ₜ[R] (n ⊗ₜ[R] q)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.instUniformSpace : {α : Type u} → [inst : UniformSpace α] → UniformSpace (CauchyFilter α)
-- Mathlib.Algebra.Lie.Weights.Linear
/-- For an Abelian Lie algebra, the weights of any Lie module are linear.  -/
LieModule.instLinearWeightsOfIsLieAbelian : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : IsLieAbelian L] [IsDomain R] [Module.IsTorsionFree R M], LieModule.LinearWeights R L M
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_smul_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {V : (x : M') → TangentSpace I' x} {g : M' → 𝕜},
  VectorField.mpullback I I' f (g • V) x = g (f x) • VectorField.mpullback I I' f V x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insert_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {k : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl k = v
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} [inst_2 : Inhabited β] {f : β → β},
  (m.modify k f)[k']! = if (k == k') = true then (Option.map f m[k]?).get! else m[k']!
-- Mathlib.Topology.Compactness.Compact
/-- The preimage of a compact set in the image of an inducing map is compact.  -/
Topology.IsInducing.isCompact_preimage' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → ∀ {K : Set Y}, IsCompact K → K ⊆ Set.range f → IsCompact (f ⁻¹' K)
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.eventuallyConst_of_isArtinian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : ℕ →o (Submodule R M)ᵒᵈ), Filter.EventuallyConst (⇑f) Filter.atTop
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.entryAtIdx? : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Option (α × β)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If a functor `G` has the same collection of cocones as a functor `F`
which has a colimit, then `G` also has a colimit.  -/
CategoryTheory.Limits.HasColimit.ofCoconesIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {K : Type u₁} [inst_2 : CategoryTheory.Category.{v₂, u₁} K] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor K C) (h : F.cocones ≅ G.cocones) [CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.HasColimit G
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommSemigroupOfMulOpposite : {M : Type u_1} → [CommSemigroup Mᵐᵒᵖ] → CommSemigroup Mᵈᵐᵃ
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal_nil : ∀ {α : TypeVec.{u} 0} (ps : α.Arrow (TypeVec.repeat 0 Prop)), TypeVec.subtypeVal ps = TypeVec.nilFun
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).isEmpty = false