mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.duple.congr_simp : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (x x_1 : M),
  x = x_1 →
    ∀ (y y_1 : M),
      y = y_1 →
        ∀ {s s_1 : R} (e_s : s = s_1) {t t_1 : R} (e_t : t = t_1) (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1),
          Convexity.StdSimplex.duple x y hs ht h = Convexity.StdSimplex.duple x_1 y_1 ⋯ ⋯ ⋯
-- Lean.Expr
/-- Count the number of lambdas at the head of the given expression.
 -/
Lean.Expr.getNumHeadLambdas : Lean.Expr → ℕ
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.collectUsed : Array Lean.Elab.DefViewElabHeader →
  Array Lean.Expr → List Lean.Elab.Term.LetRecToLift → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 -/
CategoryTheory.Limits.Bicone.pt : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {F : J → C} → CategoryTheory.Limits.Bicone F → C
-- Mathlib.Order.Category.PartOrd
/-- Turn a morphism in `PartOrd` back into a `OrderHom`.  -/
PartOrd.Hom.hom : {X Y : PartOrd} → X.Hom Y → ↑X →o ↑Y
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit : {n : ℕ} →
  Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
        Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.single_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toColex fun₀ | a => 1) ≤ toColex fun₀ | b => 1) ↔ a ≤ b
-- Mathlib.Order.Set
WithTop.range_eq : ∀ {α : Type u_1} {β : Type u_2} (f : WithTop α → β), Set.range f = insert (f ⊤) (Set.range (f ∘ WithBot.some))
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.ofNat_mul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : ℕ), OfNat.ofNat (a * b) = OfNat.ofNat a * OfNat.ofNat b
-- Mathlib.Data.Multiset.Filter
Multiset.countP_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst_1 : DecidablePred q] (s : Multiset α),
  Multiset.countP p (Multiset.filter q s) = Multiset.countP (fun a => p a ∧ q a) s
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.hasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C],
  CategoryTheory.Limits.HasColimitsOfShape
    (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z)) C
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instInfSet : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → InfSet (CategoryTheory.Precoverage C)
-- Mathlib.Data.Set.Functor
Set.image2.eq_1 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s : Set α) (t : Set β),
  Set.image2 f s t = {c | ∃ a ∈ s, ∃ b ∈ t, f a b = c}
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.pair.sizeOf_spec : ∀ (a a_1 : Nat.Partrec.Code), sizeOf (a.pair a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.SInt.Bitwise
Int8.xor_assoc : ∀ (a b c : Int8), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a < b → IsConnected (Set.Ioo a b)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.lintegral_prod_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} (f : α × β → ENNReal),
  ∫⁻ (z : α × β), f z ∂μ.prod ν ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_neg_atTop_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {x y : G},
  (MapClusterPt (-x) Filter.atTop fun x => x • y) ↔ MapClusterPt x Filter.atTop fun x => x • y
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take_nil : ∀ {α : Type u} {n : ℕ}, Stream'.Seq.take n Stream'.Seq.nil = []
-- Init.Data.Iterators.Basic
/-- The output value could plausibly be emitted in the next step.  -/
Std.Iter.IsPlausibleIndirectOutput.direct : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {out : β},
  it.IsPlausibleOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsRightAdjoint], F.PreservesMonomorphisms
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E}
  {x : E},
  HasFDerivAt f f' x →
    HasFDerivAt g g' x →
      0 < f x → HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
-- Init.Data.BitVec.Lemmas
BitVec.getElem_of_getElem? : ∀ {w n : ℕ} {a : Bool} {l : BitVec w}, l[n]? = some a → ∃ (h : n < w), l[n] = a
-- Mathlib.Algebra.Exact.Basic
Function.Exact.addMonoidHom_ker_eq : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g → g.ker = f.range
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_empty : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], NonUnitalSubsemiring.closure ∅ = ⊥
-- Mathlib.Order.CompletePartialOrder
DirectedOn.le_sSup : ∀ {α : Type u_2} [inst : CompletePartialOrder α] {d : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) d → a ∈ d → a ≤ sSup d
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkIntModuleInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.zero_bind : ∀ {α β : Type u} (f : α → FreeAddGroup β), 0 >>= f = 0
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isUnit_unit' : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {ζ : G} {n : ℕ} (hn : n ≠ 0) (hζ : IsPrimitiveRoot ζ n),
  IsPrimitiveRoot ⋯.unit' n
-- Mathlib.Order.Basic
le_iff_le_iff_lt_iff_lt : ∀ {α : Type u_2} {β : Type u_5} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β},
  (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)
-- Mathlib.Tactic.Linarith.Frontend
/-- Split `≠` in hypotheses, by branching in cases `<` and `>`.  -/
Mathlib.Tactic.Linarith.LinarithConfig.splitNe : Mathlib.Tactic.Linarith.LinarithConfig → Bool
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `G` is closed under inverses  -/
Subgroup.inv_mem' : ∀ {G : Type u_3} [inst : Group G] (self : Subgroup G) {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
-- Mathlib.Topology.Order
instTopologicalSpaceNat : TopologicalSpace ℕ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas.0.RootPairing.termα : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inl_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.snd h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a b : B} {a' : C} {f g : a ⟶ b}
  (β : f ⟶ g) (h : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.Bicategory.whiskerRight (η.naturality g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.unitOfList l) k = ()
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_eq_empty : ∀ {n : ℕ}, n.properDivisors = ∅ ↔ n ≤ 1
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLEOrdinal : LE Std.Time.Nanosecond.Ordinal
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_containsKey_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    ((List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).isEmpty = true ↔
      ∀ (k : α), Std.Internal.List.containsKey k l₁ = true → Std.Internal.List.containsKey k l₂ = false)
-- Mathlib.Algebra.Group.Action.Defs
/-- Note that the `SMulCommClass α β β` typeclass argument is usually satisfied by `Algebra α β`.  -/
mul_smul_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul β] [inst_1 : SMul α β] [SMulCommClass α β β] (s : α) (x y : β),
  x * s • y = s • (x * y)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- If `t.coef = 0`, then `t.toFun` is zero.  -/
Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun : ∀ {t : Tactic.ComputeAsymptotics.Monomial} (basis : Tactic.ComputeAsymptotics.Basis), t.coef = 0 → t.toFun basis = 0
-- Batteries.Data.Array.Match
Array.PrefixTable.toArray : {α : Type u_1} → Array.PrefixTable α → Array (α × ℕ)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Auxiliary lemma for `IsAdjoinRoot.lift`  -/
IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T},
  Polynomial.eval₂ i x f = 0 →
    ∀ (z : S) (w : Polynomial R), h.map w = z → Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α}, (m₁.union m₂ ⋯ ⋯).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_singleton : ∀ {α : Type u_1} [inst : EDist α] {x : α}, {x}.einfsep = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The pushout of two epimorphisms exists.  -/
CategoryTheory.NormalEpiCategory.pushout_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C] {X Y Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [CategoryTheory.Epi a]
  [CategoryTheory.Epi b], CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span a b)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_eq_lift : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Injective f →
    Cardinal.lift.{max u w, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)
-- Init.Data.SInt.Bitwise
Int32.shiftLeft_or : ∀ {a b c : Int32}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.Data.Set.Finite.Monad
Finite.Set.finite_pure : ∀ {α : Type u} (a : α), (pure a).Finite
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [inst_2 : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup]
  [inst_3 : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup], ∃ π, v.IsUniformizer ↑π
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- Induced inner product on a submodule.  -/
Submodule.innerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (W : Submodule 𝕜 E) → InnerProductSpace 𝕜 ↥W
-- Mathlib.Data.List.Cycle
Cycle.chain_iff_pairwise : ∀ {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [IsTrans α r], Cycle.Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_sub : ∀ {R : Type u_1} {a b : R} [inst : Sub R] (z w : QuadraticAlgebra R a b), (z - w).re = z.re - w.re
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Any monoid homomorphism `M →* A` can be lifted to an algebra homomorphism
`R[M] →ₐ[R] A`.  -/
AddMonoidAlgebra.lift : (R : Type u_1) →
  (A : Type u_4) →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : Semiring A] → [inst_3 : Algebra R A] → (Multiplicative M →* A) ≃ (AddMonoidAlgebra R M →ₐ[R] A)
-- Mathlib.Tactic.Conv
/-- * `discharge => tac` is a conv tactic which rewrites target `p` to `True` if `tac` is a tactic
  which proves the goal `⊢ p`.
* `discharge` without argument returns `⊢ p` as a subgoal.
 -/
Mathlib.Tactic.Conv.dischargeConv : Lean.ParserDescr
-- Mathlib.Data.List.Perm.Basic
List.Perm.insertIdx : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → ∀ (n : ℕ) (a : α), (l₁.insertIdx n a).Perm (l₂.insertIdx n a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.minKey?.bind t.getKey? = t.minKey?
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) (F.map h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) h_1) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
            h_1)))
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow : ∀ (S : Type u_1) [inst : CommRing S] (d e : ℕ),
  (1 - PowerSeries.X) ^ (d + e) * ↑(PowerSeries.invOneSubPow S e) = (1 - PowerSeries.X) ^ d
-- Mathlib.Data.Set.Basic
Set.union_inter_cancel_left : ∀ {α : Type u} {s t : Set α}, (s ∪ t) ∩ s = s
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The adjoint operator as a partially defined linear operator, denoted as `T†`.  -/
LinearPMap.adjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → (E →ₗ.[𝕜] F) → [CompleteSpace E] → F →ₗ.[𝕜] E
-- Batteries.Tactic.Alias
_private.Batteries.Tactic.Alias.0.Batteries.Tactic.Alias.addSide : Bool → Lean.Name → Lean.Elab.Modifiers → Lean.ConstantInfo → Lean.Elab.TermElabM Unit
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (x_1 : RBTree.RBNode α) →
        ((t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t) →
          ((parent : RBTree.RBNode.Path α) →
              (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a) →
            ((a : RBTree.RBNode α) →
                (y : α) →
                  (parent : RBTree.RBNode.Path α) →
                    (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b) →
              ((parent : RBTree.RBNode.Path α) →
                  (y : α) →
                    (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a) →
                ((a : RBTree.RBNode α) →
                    (y : α) →
                      (parent : RBTree.RBNode.Path α) →
                        (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b) →
                  motive x x_1
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a b : α), (s.erase a).erase b = (s.erase b).erase a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_pow_mul_le_seminorm : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (k : ℕ) (x₀ : E),
  ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.coe_add_self_eq : ∀ {M : Type u_3} [inst : AddMonoid M] (s : AddSubmonoid M), ↑s + ↑s = ↑s
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {b : ι → ℝ} {f : ℝ → E} (I a : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) →
    Filter.Tendsto b l Filter.atTop →
      (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I) → MeasureTheory.IntegrableOn f (Set.Ioi a) μ
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ico_ae_eq_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ico a b =ᵐ[μ] Set.Icc a b
-- Init.Data.BitVec.Lemmas
BitVec.toInt_append_zero : ∀ {n m : ℕ} {x : BitVec n}, (x ++ 0#m).toInt = 2 ^ m * x.toInt
-- Mathlib.Data.Real.Basic
Real.commRing : CommRing ℝ
-- Std.Time.Date.Unit.Day
Std.Time.Day.instInhabitedOrdinal : Inhabited Std.Time.Day.Ordinal
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
RingHom.compLeftContinuousBounded_apply_apply : ∀ {β : Type v} {γ : Type w} (α : Type u_2) [inst : TopologicalSpace α] [inst_1 : SeminormedRing β]
  [inst_2 : SeminormedRing γ] (g : β →+* γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β)
  (x : α), ((RingHom.compLeftContinuousBounded α g hg) f) x = g (f x)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instIsOrderedAddMonoid : ∀ {ι : Type u_1} (α : ι → Type u_3) [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), IsOrderedAddMonoid (α i)], IsOrderedAddMonoid (Π₀ (i : ι), α i)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The opcycles in degree `i` of a homological complex.  -/
HomologicalComplex.opcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → (K : HomologicalComplex C c) → (i : ι) → [K.HasHomology i] → C
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The computable `ChosenPullbacksAlong.pullback g` is naturally isomorphic to the noncomputable
`Over.pullback g`.  -/
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Z X : C} →
      (g : Z ⟶ X) →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
          CategoryTheory.ChosenPullbacksAlong.pullback g ≅ CategoryTheory.Over.pullback g
-- Mathlib.Order.Ideal
Order.Ideal.coe_ssubset_coe : ∀ {P : Type u_1} [inst : LE P] {s t : Order.Ideal P}, ↑s ⊂ ↑t ↔ s < t
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_inter_ground : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk (X ∩ M.E) = M.eRk X
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ordered_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a b = Ordering.lt) t.toList
-- Mathlib.FieldTheory.KrullTopology
/-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ Gal(L/K)` is
closed.  -/
IntermediateField.fixingSubgroup_isClosed : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [FiniteDimensional K ↥E], IsClosed ↑E.fixingSubgroup
-- Batteries.Data.RunningStats
/-- Compute running statistics of a data stream using Welford's algorithm.  -/
Batteries.RunningStats : Type
-- Mathlib.Data.EReal.Inv
EReal.abs_coe_lt_top : ∀ (x : ℝ), (↑x).abs < ⊤
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.mul_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x y : CategoryTheory.CatCenter C) (X : C),
  (x * y).app X = CategoryTheory.CategoryStruct.comp (y.app X) (x.app X)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.coe_mk : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E} (hv : Orthonormal 𝕜 v)
  (hsp : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure), ⇑(HilbertBasis.mk hv hsp) = v
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zero_pow_le_one : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] [ZeroLEOneClass M₀] (n : ℕ), 0 ^ n ≤ 1