mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrict.congr_simp : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits], Polynomial.Gal.restrict p E = Polynomial.Gal.restrict p E
-- Batteries.Data.List.Lemmas
List.countBefore_cons : ∀ {α : Type u_1} {xs : List α} {x : α} {i : ℕ} [inst : BEq α] {a : α},
  List.countBefore x (a :: xs) i =
    if i = 0 then 0 else if (a == x) = true then List.countBefore x xs (i - 1) + 1 else List.countBefore x xs (i - 1)
-- Lean.Data.Lsp.Internal
/-- The request ID in the context of which this worker -> watchdog request was emitted.
Used for cancelling this request in the watchdog.
 -/
Lean.Lsp.LeanQueryModuleParams.sourceRequestID : Lean.Lsp.LeanQueryModuleParams → Lean.JsonRpc.RequestID
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] (f : E →L[𝕜] E) (hf : f.det ≠ 0)
  (x : E), (f.toContinuousLinearEquivOfDetNeZero hf) x = f x
-- Mathlib.Algebra.Group.Action.Defs
AddDistribAddAction.toAddAction : {M : Type u_9} →
  {N : Type u_10} → {inst : AddMonoid M} → {inst_1 : AddMonoid N} → [self : AddDistribAddAction M N] → AddAction M N
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_anti : ∀ {k : Type u_1} {V1 : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : LinearOrder k] [inst_4 : Preorder V1] [AddLeftMono V1] [SMulPosMono k V1] {p₀ p₁ : V1},
  p₁ ≤ p₀ → Antitone ⇑(AffineMap.lineMap p₀ p₁)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise inversion of finset `s⁻¹` is defined as `{x⁻¹ | x ∈ s}` in scope `Pointwise`.  -/
Finset.inv : {α : Type u_2} → [DecidableEq α] → [Inv α] → Inv (Finset α)
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.goalDiagToMessageData.go : Lean.Meta.Grind.Goal → Lean.Grind.Config → Bool → Lean.Meta.Grind.M✝ Unit
-- Mathlib.Algebra.Order.Group.Abs
div_le_of_mabs_div_le_left : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G}, |a / b|ₘ ≤ c → b / c ≤ a
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (X_1 : CategoryTheory.Over U),
  (U.overEquivalence.unitIso.inv.app X_1).left = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
sInf_sup_eq : ∀ {α : Type u} [inst : Order.Coframe α] {s : Set α} {b : α}, sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.funMap_cast : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  {n : ℕ} (f : L.Functions n) (x : Fin n → (a : α) → M a),
  (FirstOrder.Language.Structure.funMap f fun i => Quotient.mk' (x i)) =
    Quotient.mk' fun a => FirstOrder.Language.Structure.funMap f fun i => x i a
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.hasRightDerivedFunctor_iff_of_iso : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_2} H] {F F' : CategoryTheory.Functor C H} (e : F ≅ F')
  (W : CategoryTheory.MorphismProperty C), F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
-- Mathlib.CategoryTheory.Products.Associator
/-- The equivalence swapping the second and third categories in `(A × C) × (D × E)`. This follows
the definition of `MonoidalCategory.tensorμ`.  -/
CategoryTheory.prod.prodμ : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (A : Type u₄) → [inst_3 : CategoryTheory.Category.{v₄, u₄} A] → (A × C) × D × E ≌ (A × D) × C × E
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- The functor from a category to the canonical quotient of its path category.  -/
CategoryTheory.toQuotientPaths : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor C (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : CategoryTheory.Cat) (x : CategoryTheory.Join C ↑D),
  CategoryTheory.CategoryStruct.id x = x.id
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_getKey_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} (h' : k ∈ t),
  cmp (t.getKey k h') k = Ordering.eq
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.hasCentralRadical_iff : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.HasCentralRadical R L ↔ LieAlgebra.radical R L = LieAlgebra.center R L
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.hom_ext_iff : ∀ {X Y : UniformSpaceCat} {f g : X ⟶ Y},
  f = g ↔ ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Init.Data.Array.Monadic
Array.flatMapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : { x // p x } → m (Array β)} {g : α → m (Array β)},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.flatMapM f xs = Array.flatMapM g xs.unattach
-- Lean.Data.Json.Basic
Lean.Json.Structured.arr.sizeOf_spec : ∀ (elems : Array Lean.Json), sizeOf (Lean.Json.Structured.arr elems) = 1 + sizeOf elems
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.abs_repr : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Cofix F α),
  Quot.mk MvQPF.Mcongr x.repr = x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.builder_name.quot : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_sub : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.opcyclesMapIso iso i).inv = HomologicalComplex.opcyclesMap iso.inv i
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.isScalarTower : ∀ (R₁ : Type u_1) (R₂ : Type u_2) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : CommSemiring R₂] [inst_2 : Ring A]
  [inst_3 : Algebra R₁ A] [inst_4 : Algebra R₂ A] [inst_5 : SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A),
  IsScalarTower R₁ R₂ (A ⧸ I)
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_uInt64ToBitVec : ∀ (n : UInt64), { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_eq_if : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_9 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    if hu : r.lower < r.upper then
      have hle := ⋯;
      do
      let __do_lift ← f r.lower ⋯ init
      match __do_lift with
        | ForInStep.yield c => forIn' (r.lower<...r.upper) c fun a ha acc => f a ⋯ acc
        | ForInStep.done c => pure c
    else pure init
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.ι_gluedIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
  [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J) {Z : C'} (h : (D.mapGlueData F).glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).hom h) =
    CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) h
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.algSpec_map_left : ∀ {R : CommRingCat} {X Y : (CommAlgCat ↑R)ᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Over.Hom.left ((AlgebraicGeometry.algSpec R).map f) =
    AlgebraicGeometry.Spec.map (CategoryTheory.Under.Hom.right ((commAlgCatEquivUnder R).functor.map f.unop))
-- Init.Prelude
/-- Constructs a new empty byte array with initial capacity `c`.
 -/
ByteArray.emptyWithCapacity : ℕ → ByteArray
-- Mathlib.Data.Nat.Bits
Nat.bodd.eq_1 : ∀ (n : ℕ), n.bodd = n.testBit 0
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A version of `Cone.ext` for `Fan`s.  -/
CategoryTheory.Limits.Fan.ext : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        {c₁ c₂ : CategoryTheory.Limits.Fan f} →
          (e : c₁.pt ≅ c₂.pt) →
            autoParam (∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b))
                CategoryTheory.Limits.Fan.ext._auto_1 →
              (c₁ ≅ c₂)
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.instFunLike : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → FunLike (B₁ →bᵢ B₂) M₁ M₂
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.liftNCAlgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : Semiring B] [inst_5 : Algebra R B] (f f_1 : A →ₐ[R] B)
  (e_f : f = f_1) (g g_1 : Multiplicative M →* B) (e_g : g = g_1)
  (h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)),
  AddMonoidAlgebra.liftNCAlgHom f g h_comm = AddMonoidAlgebra.liftNCAlgHom f_1 g_1 ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr}
  {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_1' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x : CategoryTheory.IsIso (α.app X)},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X))
      (CategoryTheory.CategoryStruct.comp (F.map f) (α.app Y)) =
    G.map f
-- Mathlib.Algebra.Lie.Semisimple.Lemmas
LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful : ∀ (k : Type u_1) (L : Type u_2) (M : Type u_3) [inst : Field k] [CharZero k] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra k L] [Module.Finite k L] [inst_5 : AddCommGroup M] [inst_6 : Module k M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule k L M] [Module.Finite k M] [LieModule.IsIrreducible k L M]
  [LieModule.IsFaithful k L M] [LieModule.IsTriangularizable k L M],
  (∀ (x : L), (LinearMap.trace k M) ((LieModule.toEnd k L M) x) = 0) → LieAlgebra.HasTrivialRadical k L
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.map_fst_toList_eq_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → List.map Prod.fst (Std.DHashMap.Raw.Const.toList m) = m.keys
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.maxKey he ∈ t
-- Init.Data.List.MinMaxOn
List.minOn?.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (l l_1 : List α), l = l_1 → List.minOn? f l = List.minOn? f_1 l_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Bool} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter f m).contains k = true → m.contains k = true
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.cons : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α × Bool},
  FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (x :: L₁) (x :: L₂)
-- Mathlib.Tactic.Simproc.VecPerm
/-- Helper function to produce a term of type `Fin m` given by `n` (and a proof that `n < m` via
`decide`.)
Note: this could be inlined below, but this seems to produce a strange Qq bug.  -/
_private.Mathlib.Tactic.Simproc.VecPerm.0.Mathlib.Tactic.FinVec.mkFin : Q(ℕ) → (m : Q(ℕ)) → Lean.MetaM Q(Fin «$m»)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_compl_le_add_of_le_add : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet s → MeasurableSet t → ∀ {ε : ENNReal}, μ s ≤ μ t + ε → μ tᶜ ≤ μ sᶜ + ε
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry : Type
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.swap_mul : ∀ {α : Type u_4} [inst : DecidableEq α] {f : Equiv.Perm α},
  f.IsCycle → ∀ {x : α}, f x ≠ x → f (f x) ≠ x → (Equiv.swap x (f x) * f).IsCycle
-- Mathlib.Data.Finset.Basic
Finset.erase_subset_iff_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ t → (s.erase a ⊆ t ↔ s ⊆ t)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.of_existsUnique_irreducible_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) →
    (∀ (f g : Multiset α),
        (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) →
      UniqueFactorizationMonoid α
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F], Differentiable 𝕜 1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_sub : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → μ.Integrable g → ∫ᵛ (x : X), (f - g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
-- Mathlib.Data.Fintype.Card
Finite.surjective_of_injective : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Injective f → Function.Surjective f
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  {t : Set α}, IsLocalExtrOn f t a → s ⊆ t → IsLocalExtrOn f s a
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T0Space X] [h : TopologicalSpace.PseudoMetrizableSpace X],
  TopologicalSpace.MetrizableSpace X
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntry_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯) k).isLE = true
-- Mathlib.Order.Heyting.Basic
sup_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ⊔ a \ b = a
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instSMulOfModule : {𝕜 : Type u_3} →
  {𝕝 : Type u_1} →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst : CommSemiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module 𝕜 F] →
                  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → [inst_5 : CommSemiring 𝕝] → [Module 𝕝 E] → SMul 𝕝 (WeakBilin B)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_ite_eq' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => b = x] (a : α) (L : optParam (SummationFilter β) (SummationFilter.unconditional β))
  [L.LeAtTop], HasProd (fun b' => if b = b' then a else 1) a L
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.compStarAlgHom_apply : ∀ (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [inst : TopologicalSpace X] [inst_1 : CommSemiring 𝕜]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : IsTopologicalSemiring A] [inst_5 : Star A]
  [inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A] [inst_8 : TopologicalSpace B] [inst_9 : Semiring B]
  [inst_10 : IsTopologicalSemiring B] [inst_11 : Star B] [inst_12 : ContinuousStar B] [inst_13 : Algebra 𝕜 B]
  (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) (f : C(X, A)),
  (ContinuousMap.compStarAlgHom X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ }.comp f
-- Aesop.RuleSet
Aesop.GlobalRuleSet.erase : Aesop.GlobalRuleSet → Aesop.RuleFilter → Aesop.GlobalRuleSet × Bool
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)],
  Nonempty (CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.Γ.mapCocone c.op))
-- Mathlib.Analysis.MellinTransform
MellinConvergent.comp_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} {a : ℝ},
  a ≠ 0 → (MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a))
-- Lean.Declaration
Lean.instInhabitedDeclaration.default : Lean.Declaration
-- Mathlib.Topology.Order.LeftRightLim
leftLim_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds (Function.leftLim f a)) →
    ∀ [h' : (nhdsWithin a (Set.Iio a)).NeBot], Function.leftLim (Function.rightLim f) a = Function.leftLim f a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {x y : S.Relation}, x.fst = y.fst → x.snd = y.snd → x.r ≍ y.r → x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_id : ∀ {X : SSet} (A : X.Subcomplex), A.image (CategoryTheory.CategoryStruct.id X) = A
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.ext : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : Metric.PiNatEmbed X Y f},
  x.ofPiNat = y.ofPiNat → x = y
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_comm : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R), I * J = J * I
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod.eq_1 : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i → γ), f.prod g = ∏ i ∈ f.support, g i (f i)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_extendScalars : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E), ↑(IntermediateField.extendScalars h) = ↑E
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0},
  MeasurableSet s →
    μ s ≠ ⊤ →
      ∀ {f : ↥(MeasureTheory.Lp ℝ 2 μ)},
        ↑↑f =ᵐ[μ.restrict s] 0 → ↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succ?_encode : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  {x : α}, Std.PRange.succ? (HasModel.encode✝ x) = Option.map HasModel.encode✝ (Std.PRange.succ? x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited β] {a : α}, Std.DTreeMap.Const.get! t a = t.get! a
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_mul_I : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.w₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀),
  CategoryTheory.CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.mk.inj : ∀ {mvarId : Lean.MVarId} {newHs : Array Lean.FVarId} {subst : Lean.Meta.FVarSubst} {mvarId_1 : Lean.MVarId}
  {newHs_1 : Array Lean.FVarId} {subst_1 : Lean.Meta.FVarSubst},
  { mvarId := mvarId, newHs := newHs, subst := subst } = { mvarId := mvarId_1, newHs := newHs_1, subst := subst_1 } →
    mvarId = mvarId_1 ∧ newHs = newHs_1 ∧ subst = subst_1
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
  CategoryTheory.sheafifyLift J η hQ =
    (((CategoryTheory.sheafificationAdjunction J D).homEquiv P { obj := Q, property := hQ }).symm η).hom