mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w) (lhs : BitVec w) (rhs : BitVec target.n)
  (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig target).aig,
              ref :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig target).vec.get idx hidx }⟧ =
          (lhs.sshiftRight' (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectedSystem.coe_natLERec : ∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))) (m n : ℕ) (h : m ≤ n),
  ⇑(FirstOrder.Language.DirectedSystem.natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.mk_outCLM : ∀ (K : Type u_1) {E : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E]
  (x : SeparationQuotient E), SeparationQuotient.mk ((SeparationQuotient.outCLM K E) x) = x
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftSTEST_batteries : ∀ {σ ε : Type}, LawfulMonadLift (ST σ) (EST ε σ)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a b : B} {a' : C}
  (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))
-- Mathlib.SetTheory.ZFC.Class
Class.coe_sdiff : ∀ (x y : ZFSet.{u}), ↑(x \ y) = ↑x \ ↑y
-- Init.Data.Array.Lemmas
Array.foldrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → β} {b : β}
  {xs : Array α} {start stop : ℕ},
  Array.foldrM (fun x1 x2 => pure (f x1 x2)) b xs start stop = pure (Array.foldr f b xs start stop)
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- If a function `f : R → ℝ` is monotone, then the function mapping `x` to the right limit of `f`
at `x` is a Stieltjes function, i.e., it is monotone and right-continuous.  -/
Monotone.stieltjesFunction : {R : Type u_1} →
  [inst : LinearOrder R] →
    [inst_1 : TopologicalSpace R] → [OrderTopology R] → {f : R → ℝ} → Monotone f → StieltjesFunction R
-- Lean.Widget.UserWidget
Lean.Widget.instInhabitedWidgetSource : Inhabited Lean.Widget.WidgetSource
-- Mathlib.Data.PSigma.Order
/-- Dictionary / lexicographic `PartialOrder` for dependent pairs.  -/
PSigma.Lex.partialOrder : {ι : Type u_1} →
  {α : ι → Type u_2} → [PartialOrder ι] → [(i : ι) → PartialOrder (α i)] → PartialOrder (Σₗ' (i : ι), α i)
-- Lean.Elab.Term.TermElabM
/-- Execute `x`, but keep state modifications only if `x` did not postpone.
This method is useful to implement elaboration functions that cannot decide whether
they need to postpone or not without updating the state.  -/
Lean.Elab.Term.commitIfDidNotPostpone : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Logic.Denumerable
Nat.Subtype.coe_comp_ofNat_range : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s],
  Set.range (Subtype.val ∘ Nat.Subtype.ofNat s) = s
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Clause.reify.mk : ∀ {v : Sat.Valuation} {c : Sat.Clause} {p : Prop}, (¬v.satisfies c → p) → Sat.Clause.reify v c p
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.size.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).size = l.size + r.size + 1
-- Init.Data.SInt.Lemmas
Int64.ofInt_mul : ∀ (a b : ℤ), Int64.ofInt (a * b) = Int64.ofInt a * Int64.ofInt b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ) (lhs : aig.RefVec w)
  (rhs : aig.RefVec n) (pow n_1 : ℕ) (lhs_1 : aig.RefVec w) (rhs_1 : aig.RefVec n_1) (pow_1 : ℕ),
  ({ n := n, lhs := lhs, rhs := rhs, pow := pow } = { n := n_1, lhs := lhs_1, rhs := rhs_1, pow := pow_1 }) =
    (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1 ∧ pow = pow_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If the left extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, an extension
`b : L'.LeftExtension F₁` is universal if and only if
`(LeftExtension.precomp₂ L' α).obj b` is universal.  -/
CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂Equiv : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor D D'} →
                    {F₀ : CategoryTheory.Functor C H} →
                      {F₁ : CategoryTheory.Functor D H} →
                        (α : F₀ ⟶ L.comp F₁) →
                          CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F₁ α) →
                            (b : L'.LeftExtension F₁) →
                              CategoryTheory.StructuredArrow.IsUniversal b ≃
                                CategoryTheory.StructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj b)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ext_iff : ∀ {X : Type u_5} {inst : TopologicalSpace X} {x y : DiscreteQuotient X}, x = y ↔ ⇑x.toSetoid = ⇑y.toSetoid
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.coe_topologicalClosure_bot : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  ↑⊥.topologicalClosure = closure {0}
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a fallback : α},
  ∅.getD a fallback = fallback
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms],
  ((CategoryTheory.Functor.whiskeringRight C D E).obj F).ReflectsIsomorphisms
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_balance' : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.balance' x r).dual = r.dual.balance' x l.dual
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).op =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.op X)).symm
-- Mathlib.Order.Notation
/-- Typeclass for the `⊤` (`\top`) notation  -/
Top : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Products.Unitor
/-- The left unitor functor `1 × C ⥤ C`  -/
CategoryTheory.prod.leftUnitor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} × C) C
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Turn a `Subalgebra` into a `NonUnitalSubalgebra` by forgetting that it contains `1`.  -/
Subalgebra.toNonUnitalSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → NonUnitalSubalgebra R A
-- Mathlib.Topology.Spectral.Basic
/-- A topological space is spectral if it is T0, compact, sober, quasi-separated, and its compact open
subsets form an open basis.
 -/
SpectralSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C) (X : ↑(F.obj c)),
  ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).fiber = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.sup_support_coeff_multisetProd_le`. -/
AddMonoidAlgebra.sup_support_multiset_prod_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (m : Multiset (AddMonoidAlgebra R A)),
        m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f => f.coeff.support.sup degb) m).sum
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.cfc_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} {y : ℝ} {f : ℝ → ℝ},
  (∀ x ∈ spectrum ℝ a, 0 < f x) →
    autoParam (ContinuousOn f (spectrum ℝ a)) CFC.cfc_rpow._auto_1 →
      autoParam (IsSelfAdjoint a) CFC.cfc_rpow._auto_3 → cfc f a ^ y = cfc (fun r => f r ^ y) a
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the image is a cokernel  -/
CategoryTheory.Abelian.AbelianStruct.imageIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (self : CategoryTheory.Abelian.AbelianStruct f) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.imageπ ⋯)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsInitial_snd : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj X₃)]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj Y₃)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PullbackObjObj.ofIsInitial G f₁ f₃ h).snd =
    CategoryTheory.CategoryStruct.id ((G.obj (Opposite.op Y₁)).obj Y₃)
-- Mathlib.Topology.Homotopy.Basic
/-- Given a family of homotopies `F i` between `f₀ i : C(X, Y i)` and `f₁ i : C(X, Y i)`, returns a
homotopy between `ContinuousMap.pi f₀` and `ContinuousMap.pi f₁`.  -/
ContinuousMap.Homotopy.pi : {X : Type u} →
  {ι : Type u_2} →
    [inst : TopologicalSpace X] →
      {Y : ι → Type u_3} →
        [inst_1 : (i : ι) → TopologicalSpace (Y i)] →
          {f₀ f₁ : (i : ι) → C(X, Y i)} →
            ((i : ι) → (f₀ i).Homotopy (f₁ i)) → (ContinuousMap.pi f₀).Homotopy (ContinuousMap.pi f₁)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x : HahnSeries Γ R},
  (-x).orderTop = x.orderTop
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.subset_coe_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Monoid M]
  [inst_3 : IsScalarTower R M M] [inst_4 : SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ}, ↑p ^ n ⊆ ↑(p ^ n)
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.toDiffTag : Bool → Lean.Widget.ExprDiffTag✝ → Lean.Widget.DiffTag
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.algEquiv_apply : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] (S : Type u_5) [inst_4 : CommSemiring S] [inst_5 : Module S E] [inst_6 : SMulCommClass 𝕜₁ S E]
  [inst_7 : SMul S 𝕜₁] [inst_8 : IsScalarTower S 𝕜₁ E] [inst_9 : ContinuousConstSMul S E]
  [inst_10 : IsTopologicalAddGroup E] (self : E →WOT[𝕜₁] E), (ContinuousLinearMapWOT.algEquiv S) self = self.toCLM
-- Mathlib.Probability.Moments.SubGaussian
/-- If `X` is sub-Gaussian with parameter `cX` with respect to the restriction of `μ` to
a sub-sigma-algebra `m` and `Y` is conditionally sub-Gaussian with parameter `cY` with respect to
`m` and `μ` then `X + Y` is sub-Gaussian with parameter `cX + cY` with respect to `μ`.

`HasSubgaussianMGF X cX (μ.trim hm)` can be obtained from `HasSubgaussianMGF X cX μ` if `X` is
`m`-measurable. See `HasSubgaussianMGF.trim`.  -/
ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [inst : StandardBorelSpace Ω]
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {Y : Ω → ℝ} {cX cY : NNReal} (hm : m ≤ mΩ),
  ProbabilityTheory.HasSubgaussianMGF X cX (μ.trim hm) →
    ProbabilityTheory.HasCondSubgaussianMGF m hm Y cY μ → ProbabilityTheory.HasSubgaussianMGF (X + Y) (cX + cY) μ
-- Mathlib.RingTheory.Derivation.ToSquareZero
derivationToSquareZeroEquivLift_apply_coe_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] (hI : I ^ 2 = ⊥)
  [inst_6 : IsScalarTower R A B] (d : Derivation R A ↥I) (x : A),
  ↑((derivationToSquareZeroEquivLift I hI) d) x = ↑(d x) + (algebraMap A B) x
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.pow_sub_pow_eq_sub_mul_geomSum : ∀ {α : Type u_1} [inst : CommRing α] (a b : α) (n : ℕ), a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum✝ a b n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) (a : B),
  (α.naturality (CategoryTheory.CategoryStruct.id a)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (α.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (α.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (α.app a)).inv
          (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapId a).inv)))
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_eq_abs : ∀ (r : ℝ), ‖r‖ = |r|
-- Mathlib.Data.Countable.Defs
Function.Surjective.uncountable : ∀ {α : Sort u} {β : Sort v} [Uncountable β] {f : α → β}, Function.Surjective f → Uncountable α
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.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.PreservesFiniteEffectiveEpiFamilies] [inst_3 : F.ReflectsFiniteEffectiveEpiFamilies] [inst_4 : F.Full]
  [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough] [inst_7 : CategoryTheory.Precoherent D],
  CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D) F
-- Mathlib.Order.BooleanAlgebra.Set
Set.empty_sdiff : ∀ {α : Type u_1} (s : Set α), ∅ \ s = ∅
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instLattice : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → Lattice (FiniteGaloisIntermediateField k K)
-- Mathlib.FieldTheory.SeparableClosure
isClosed_restrictScalars_separableClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra K E] [inst_6 : IsScalarTower F K E],
  (separableClosureOperator F E).IsClosed (IntermediateField.restrictScalars F (separableClosure K E))
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product `α × β × γ` that are equal on products of sets are equal.
See `ext_prod₃'` for the same statement for `(α × β) × γ`.  -/
MeasureTheory.Measure.ext_prod₃ : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ ν : MeasureTheory.Measure (α × β × γ)} [MeasureTheory.IsFiniteMeasure μ],
  (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) →
    μ = ν
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- If `P` is a presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural presentation of `T ⊗[R] S` over `T`.  -/
Algebra.Presentation.baseChange : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (T : Type u_1) →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    Algebra.Presentation R S ι σ → Algebra.Presentation T (TensorProduct R T S) ι σ
-- Mathlib.Combinatorics.Graph.Basic
/-- A graph with exactly two vertices and no loops.  -/
Graph.banana : {α : Type u_1} → {β : Type u_2} → α → α → Set β → Graph α β
-- Std.Http.Protocol.H1.Writer
/-- When `true`, body bytes are intentionally omitted from the wire for this message
(e.g. HEAD responses), while headers/framing metadata may still describe the
hypothetical representation.
 -/
Std.Http.Protocol.H1.Writer.omitBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Batteries.Data.List.Lemmas
List.idxOfNth_countBefore_of_lt_length_of_beq : ∀ {α : Type u_1} {i : ℕ} {x : α} [inst : BEq α] {xs : List α} {h : i < xs.length},
  (xs[i] == x) = true → List.idxOfNth x xs (List.countBefore x xs i) = i
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm.congr_simp : ∀ {α : Type u_4} {p : α → Prop} (f f_1 : Equiv.Perm α) (e_f : f = f_1) (h : ∀ (x : α), p (f x) ↔ p x),
  f.subtypePerm h = f_1.subtypePerm ⋯
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.evalRpcProcedure : Lean.Environment → Lean.Options → Lean.Name → Except String Lean.Server.RpcProcedure
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_eq_one_iff : ∀ {α : Type u_2} {x : α} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle], f.cycleOf x = 1 ↔ f x = x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by the sup norm of the iterated derivatives.
In the scope `Distributions.Seminorm`, we denote them by `N[𝕜; F]_{K, n, i}`
(or `N[𝕜]_{K, n, i}`), or simply by `N[𝕜; F]_{K, i}` (or `N[𝕜; F]_{K, i}`) when `n = ∞`.  -/
Distributions.«termN[_;_]_{_,_}» : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_ext_iff : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] {g h : FreeAbelianGroup α →+ β},
  g = h ↔ ∀ (x : α), g (FreeAbelianGroup.of x) = h (FreeAbelianGroup.of x)
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.hexDigit_isHexDigit : ∀ {x : UInt8}, x < 16 → Std.Http.Internal.Char.isHexDigitByte (Std.Http.URI.hexDigit x) = true
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- Quasi-inverses compose in the opposite order.  -/
LinearMap.IsQuasiInverse.comp : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂},
  u'.IsQuasiInverse u → v'.IsQuasiInverse v → (u' ∘ₗ v').IsQuasiInverse (v ∘ₗ u)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- Let `x : (K →+* ℂ) → ℂ` such that `x_φ = conj x_(conj φ)` for all `φ : K →+* ℂ`, then the
representation of `commMap K x` on `stdBasis` is given (up to reindexing) by the product of
`matrixToStdBasis` by `x`.  -/
NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (K →+* ℂ) → ℂ),
  (∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)) →
    ∀ (c : NumberField.mixedEmbedding.index K),
      ↑(((NumberField.mixedEmbedding.stdBasis K).repr ((NumberField.mixedEmbedding.commMap K) x)) c) =
        (NumberField.mixedEmbedding.matrixToStdBasis K).mulVec (x ∘ ⇑(NumberField.mixedEmbedding.indexEquiv K)) c
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_sub_right : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x - b) '' t = (fun x => x + b) ⁻¹' t
-- Mathlib.Order.Directed
directedOn_iff_isDirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, DirectedOn (fun x1 x2 => x1 ≤ x2) s ↔ IsDirectedOrder ↑s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.instCategoryStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) → CategoryTheory.CategoryStruct.{v, max u v} (CategoryTheory.Endofunctor.Algebra F)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the forward direction of `contMDiffAt_iff_contDiffAt`. -/
ContMDiffAt.contDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {x : E},
  ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x → ContDiffAt 𝕜 n f x
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.mem_finsuppAntidiag : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ}, f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s
-- Lean.Meta.Basic
Lean.Meta.FunInfo.mk.injEq : ∀ (paramInfo : Array Lean.Meta.ParamInfo) (resultDeps : Array ℕ) (paramInfo_1 : Array Lean.Meta.ParamInfo)
  (resultDeps_1 : Array ℕ),
  ({ paramInfo := paramInfo, resultDeps := resultDeps } = { paramInfo := paramInfo_1, resultDeps := resultDeps_1 }) =
    (paramInfo = paramInfo_1 ∧ resultDeps = resultDeps_1)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_normalizer : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ),
  (AddSubgroup.normalizer ↑H).unop = AddSubgroup.normalizer ↑H.unop