mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.MinMaxOn
minOn_eq_right_of_lt : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.Total fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderLT β] {f : α → β} {x y : α}, f y < f x → minOn f x y = y
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `erase` which can be used in the absence of balance
information but still assumes the preconditions of `erase`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.erase! : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fx : γ) → motive (some fx)) → motive __do_lift
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZPowersEqTop_apply : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) (a : Multiplicative ℤ),
  (intEquivOfZPowersEqTop g hg) a = g ^ Multiplicative.toAdd a
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.StdSimplex.restrict_ne_zero_aux : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  {w : Convexity.StdSimplex K X} {p : X → Prop} [inst_3 : DecidablePred p],
  (∃ a, p a ∧ w.weights a ≠ 0) → ((Finsupp.filter p w.weights).sum fun _x k => k) ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.comp : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} {b : m → α} [inst : LT α] [inst_1 : Zero R]
  {M : Matrix m m (Matrix n n R)}, M.BlockTriangular b → ((Matrix.comp m m n n R) M).BlockTriangular fun i => b i.1
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNeg.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Neg G], Filter.Germ.instNeg = { neg := Filter.Germ.map Neg.neg }
-- Mathlib.Data.Fintype.Sets
/-- Many `Fintype` instances for sets are defined using an extensionally equal `Finset`.
Rewriting `s.toFinset` with `Set.toFinset_ofFinset` replaces the term with such a `Finset`.  -/
Set.toFinset_ofFinset : ∀ {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p), p.toFinset = s
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_neg : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddGroup α]
  (M : (i : o) → Matrix (m' i) (n' i) α), Matrix.blockDiagonal' (-M) = -Matrix.blockDiagonal' M
-- Init.Data.List.Impl
List.take_eq_takeTR : @List.take = @List.takeTR
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.instLETransOfLawfulUpwardEnumerableLE : {α : Type u} →
  [inst : LE α] →
    [inst_1 : Std.PRange.UpwardEnumerable α] →
      [Std.PRange.LawfulUpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerableLE α] →
          Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- An intermediate field of `E / F` is contained in the relative perfect closure of `F` in `E`
if and only if it is purely inseparable over `F`.  -/
le_perfectClosure_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
  L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey? =
    some (t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k')
-- Init.Data.Rat.Lemmas
Rat.add_lt_add_right : ∀ {a b c : ℚ}, a + c < b + c ↔ a < b
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating : ∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set α → Prop) {s : Set α}
  [HasCountableSeparatingOn α p s], s ∈ l → s.Nonempty → (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ a ∈ s, {a} ∈ l
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_zero : ∀ {R : Type u_1} [inst : Semiring R], LaurentPolynomial.T 0 = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_prod_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G} {K : Subgroup N}
  {J : Subgroup (G × N)}, J ≤ H.prod K ↔ Subgroup.map (MonoidHom.fst G N) J ≤ H ∧ Subgroup.map (MonoidHom.snd G N) J ≤ K
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryAddEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M)
  (n : N) (r : R),
  MonoidAlgebra.curryAddEquiv.symm (MonoidAlgebra.single m (MonoidAlgebra.single n r)) = MonoidAlgebra.single (m, n) r
-- Mathlib.Data.Finset.Image
Finset.range_add_one' : ∀ (n : ℕ), Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun i => i + 1, inj' := ⋯ } (Finset.range n))
-- Mathlib.AlgebraicGeometry.Gluing
/-- Promoted to higher priority to short circuit simplifier.  -/
AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J) {Z : AlgebraicGeometry.Scheme} (h : D.glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp (D.t i j)
      (CategoryTheory.CategoryStruct.comp (D.f j i) (CategoryTheory.CategoryStruct.comp (D.ι j) h)) =
    CategoryTheory.CategoryStruct.comp (D.f i j) (CategoryTheory.CategoryStruct.comp (D.ι i) h)
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
group is finitely generated.  -/
Subgroup.fg_of_index_ne_zero : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [hG : Group.FG G] [H.FiniteIndex], Group.FG ↥H
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : List α},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).buckets).Perm
      (Std.Internal.List.insertListIfNewUnit (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β} (h : t.WF),
  (↑(t.insertMany l ⋯)).toListModel.Perm (Std.Internal.List.insertList t.toListModel l)
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_1 : ∀ (x : ℤ), Int.fdiv 0 x = 0
-- Mathlib.Topology.Semicontinuity.Defs
hasOpenLowerSectionsOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β},
  HasOpenLowerSectionsOn f Set.univ ↔ HasOpenLowerSections f
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.le_of_suffix : ∀ {p q : DyckWord}, ↑p <:+ ↑q → p ≤ q
-- Mathlib.Topology.Constructions.SumProd
isEmbedding_graph : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Topology.IsEmbedding fun x => (x, f x)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_desc_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc f g) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWorkspaceClientCapabilities : Lean.FromJson Lean.Lsp.WorkspaceClientCapabilities
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_self : ∀ {R : Type u} [inst : EuclideanDomain R] {a : R}, a ≠ 0 → a / a = 1
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- For a connected object `X` of `C`, the quotient `X / Aut X` is terminal if and only if
the quotient `F.obj X / Aut X` has exactly one element.  -/
CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X : C) →
            [inst_3 : CategoryTheory.PreGaloisCategory.IsConnected X] →
              CategoryTheory.Limits.IsTerminal
                  (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))) ≃
                Unique (MulAction.orbitRel.Quotient (CategoryTheory.Aut X) (F.obj X).obj)
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish (q + 1) φ → AlgebraicTopology.DoldKan.HigherFacesVanish q φ
-- Mathlib.Algebra.Order.ZeroLEOne
/-- Typeclass for expressing that the `0` of a type is less or equal to its `1`.  -/
ZeroLEOneClass : (α : Type u_2) → [Zero α] → [One α] → [LE α] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- Promote an equality to an isomorphism of `Over.map` functors.  -/
CategoryTheory.MorphismProperty.Over.mapCongr : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          [inst_2 : P.IsStableUnderComposition] →
            [Q.RespectsIso] →
              {X Y : T} →
                {f g : X ⟶ Y} →
                  (hfg : f = g) →
                    (hf : P f) →
                      CategoryTheory.MorphismProperty.Over.map Q hf ≅ CategoryTheory.MorphismProperty.Over.map Q ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Mathlib.Analysis.Complex.OpenMapping
/-- Corollary to the open mapping theorem: A holomorphic function whose imaginary part is constant is
itself constant.
 -/
AnalyticOnNhd.eq_const_of_im_eq_const : ∀ {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ},
  AnalyticOnNhd ℂ f U → (∀ x ∈ U, (f x).im = c₀) → IsOpen U → IsConnected U → ∃ c, ∀ x ∈ U, f x = c
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFiniteObj : ∀ {X : FintypeCat}, Finite X.obj
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_antiperiodic : Function.Antiperiodic Complex.exp (↑Real.pi * Complex.I)
-- Init.Tactics
/-- Stops the stateful proof mode of `Std.Do.SPred`.
This will simply forget all the names given to stateful hypotheses and pretty-print
a bit differently.
 -/
Lean.Parser.Tactic.mstopMacro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Two maps into a wide equalizer are equal if they are equal when composed with the wide
equalizer map.  -/
CategoryTheory.Limits.wideEqualizer.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C}
  {k l : W ⟶ CategoryTheory.Limits.wideEqualizer f},
  CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.wideEqualizer.ι f) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f) →
    k = l
-- Mathlib.Algebra.Lie.Classical
/-- An equivalence between two possible definitions of the classical Lie algebra of type D.  -/
LieAlgebra.Orthogonal.typeDEquivSo' : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] →
      [inst_1 : CommRing R] →
        [inst_2 : Fintype l] →
          [Invertible 2] → ↥(LieAlgebra.Orthogonal.typeD l R) ≃ₗ⁅R⁆ ↥(LieAlgebra.Orthogonal.so' l l R)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The codomain of the 2-morphism associated with a node as a list
(the first component is the node itself).  -/
Mathlib.Tactic.Widget.StringDiagram.Node.tarList : Mathlib.Tactic.Widget.StringDiagram.Node →
  List (Mathlib.Tactic.Widget.StringDiagram.Node × Mathlib.Tactic.BicategoryLike.Atom₁)
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedCommRing.toNonUnitalCommRing : {α : Type u_5} → [self : NonUnitalNormedCommRing α] → NonUnitalCommRing α
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_isOpenEmbedding : ∀ (D : TopCat.GlueData) (i : D.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i))
-- Init.Data.List.Lemmas
List.map_filterMap_some_eq_filter_map_isSome : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α},
  List.map some (List.filterMap f l) = List.filter (fun b => b.isSome) (List.map f l)
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.restrictScalars_eq : ∀ (𝕜 : Type u_1) (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  {E : Type u_6} [inst_3 : SeminormedAddCommGroup E] [h : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E]
  [IsScalarTower 𝕜 𝕜' E], NormedSpace.restrictScalars 𝕜 𝕜' E = h
-- Mathlib.Order.Heyting.Hom
/-- `HeytingHomClass F α β` states that `F` is a type of Heyting homomorphisms.

You should extend this class when you extend `HeytingHom`.  -/
HeytingHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [HeytingAlgebra α] → [HeytingAlgebra β] → [FunLike F α β] → Prop
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^8 - 1` for natural numbers greater than or equal to `2^8`.
 -/
UInt8.ofNatTruncate : ℕ → UInt8
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.exists_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] {a b : R}, (algebraMap R S) a = (algebraMap R S) b → ∃ n, x ^ n * a = x ^ n * b
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence induces a continuous linear map.  -/
ContinuousLinearEquiv.toContinuousLinearMap : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → (M₁ ≃SL[σ₁₂] M₂) → M₁ →SL[σ₁₂] M₂
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find
`i : ι`, belonging to `t` if `t` is nonempty, such that `‖(s.map f).sum‖ ≤ ‖f i‖`.  -/
IsUltrametricDist.exists_norm_multiset_sum_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι]
  {f : ι → M}, ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).sum‖ ≤ ‖f i‖
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_le_cancel_eq : ∀ (ctx : Nat.Internal.Linear.Context) (m₁ m₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_le ctx (m₁.cancel m₂) = Nat.Internal.Linear.Poly.denote_le ctx (m₁, m₂)
-- Mathlib.Algebra.Homology.Opposite
/-- Sends a complex `X` with objects in `V` to the corresponding complex with objects in `Vᵒᵖ`.  -/
HomologicalComplex.op : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → HomologicalComplex V c → HomologicalComplex Vᵒᵖ c.symm
-- Lean.Meta.Sym.SymM
/-- Maps expressions to their maximal free variable (by declaration index).

- `maxFVar[e] = some fvarId` means `fvarId` is the free variable with the largest declaration
  index occurring in `e`.
- `maxFVar[e] = none` means `e` contains no free variables (but may contain metavariables).

Recall that if `e` contains a metavariable `?m`, then we assume `e` may contain any free variable
in the local context associated with `?m`.

This mapping enables O(1) local context compatibility checks during metavariable assignment.
Instead of traversing local contexts with `isSubPrefixOf`, we check if the maximal free variable
in the assigned value is in scope of the metavariable's local context.

**Note**: We considered using a mapping `PHashMap ExprPtr FVarId`. However, there is a corner
case that is not supported by this representation. `e` contains a metavariable (with an empty local context),
and no free variables.
 -/
Lean.Meta.Sym.State.maxFVar : Lean.Meta.Sym.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId)
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vsub_cancel_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y z : P), nndist (x -ᵥ z) (y -ᵥ z) = nndist x y
-- Mathlib.Topology.ContinuousOn
Continuous.continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, Continuous f → ContinuousWithinAt f s x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.negate : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β → Std.Sat.CNF.Clause α
-- Mathlib.Algebra.Lie.TensorProduct
/-- A useful alternative characterisation of Lie ideal operations on Lie submodules.

Given a Lie ideal `I ⊆ L` and a Lie submodule `N ⊆ M`, by tensoring the inclusion maps and then
applying the action of `L` on `M`, we obtain morphism of Lie modules `f : I ⊗ N → L ⊗ M → M`.

This lemma states that `⁅I, N⁆ = range f`.  -/
LieSubmodule.lieIdeal_oper_eq_tensor_map_range : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} [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]
  (I : LieIdeal R L) (N : LieSubmodule R L M),
  ⁅I, N⁆ = ((LieModule.toModuleHom R L M).comp (TensorProduct.LieModule.mapIncl I N)).range
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_eq_ker_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Surjective ⇑f → ∀ {H : Subgroup N}, Subgroup.comap f H = f.ker ↔ H = ⊥
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension : ∀ (K : Type w) {L : Type z} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsIntegral K L] {n : ℕ}
  [NeZero n] {ζ : L}, IsPrimitiveRoot ζ n → IsCyclotomicExtension {n} K ↥K⟮ζ⟯
-- Mathlib.Order.Interval.Finset.Defs
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.  -/
IsEmpty.toLocallyFiniteOrder : {α : Type u_1} → [inst : Preorder α] → [IsEmpty α] → LocallyFiniteOrder α
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instCommMonoidWithZeroSubtypeMemSubmonoidMrangeMonoidWithZeroHomOfClass : {R : Type u_3} →
  {Γ₀ : Type u_5} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
        (v : Valuation R Γ₀) → CommMonoidWithZero ↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v))
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' : ∀ {f : ℝ → ℝ},
  MeasurableEmbedding f →
    ∀ {s : Set ℝ},
      MeasurableSet s →
        ∀ {f' : ℝ → ℝ},
          (∀ (x : ℝ), HasDerivAt f (f' x) x) →
            ∀ {g : ℝ → ℝ},
              0 ≤ᵐ[MeasureTheory.volume] g →
                MeasureTheory.Integrable g MeasureTheory.volume →
                  (MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s =
                    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
-- Std.Time.DateTime.PlainDateTime
/-- Determines the era of the given `PlainDateTime` based on its year.
 -/
Std.Time.PlainDateTime.era : Std.Time.PlainDateTime → Std.Time.Year.Era
-- Init.Data.BitVec.Lemmas
BitVec.toNat_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, (x.rotateLeft r).toNat = x.toNat <<< (r % w) % 2 ^ w ||| x.toNat >>> (w - r % w)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
InformationTheory.integrable_llr_compProd_iff : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) →
    (MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ) ↔
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ ∧
        MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (μ.compProd η)) (μ.compProd κ))
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `J` is nonzero.  -/
FractionalIdeal.ideal_factor_ne_zero : ∀ {R : Type u_6} [inst : CommRing R] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R}, I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J → J ≠ 0
-- Mathlib.Data.List.Sort
List.orderedInsert_of_not_le : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {a b : α} (l : List α),
  ¬r a b → List.orderedInsert r a (b :: l) = b :: List.orderedInsert r a l
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.val_neg_addUnit' : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a), ↑(-h.addUnit') = -a
-- Mathlib.Order.Bounds.Image
IsGLB.of_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) → ∀ {s : Set α} {x : α}, IsGLB (f '' s) (f x) → IsGLB s x
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.toBasisAt.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_9 : (x : M) → AddCommGroup (V x)]
  [inst_10 : (x : M) → Module 𝕜 (V x)] [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V]
  {ι : Type u_7} {s s_1 : ι → (x : M) → V x} (e_s : s = s_1) {u u_1 : Set M} (e_u : u = u_1) {x : M}
  {n n_1 : WithTop ℕ∞} (e_n : n = n_1) (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u), hs.toBasisAt hx = ⋯.toBasisAt ⋯
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.lid_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W) (a : A) (w : W),
  (Representation.TensorProduct.lid A σ) (a ⊗ₜ[A] w) = a • w