mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.mk.inj : ∀ {m : Type u_1} {inst : Fintype m} {inst_1 : LinearOrder m} {n : Type u_2} {inst_2 : LinearOrder n} {R : Type u_3}
  {inst_3 : CommRing R} {A : Matrix m n R} {L : Matrix m m R} {σ : Equiv.Perm m} {pivot : m → WithTop n}
  {isPivotedBy : (L * A.submatrix (⇑σ) id).IsPivotedBy pivot} {L_lowerTriangular : L.IsLowerTriangular}
  {L_diag_ne_zero : ∀ (i : m), L.diag i ≠ 0} {L_1 : Matrix m m R} {σ_1 : Equiv.Perm m} {pivot_1 : m → WithTop n}
  {isPivotedBy_1 : (L_1 * A.submatrix (⇑σ_1) id).IsPivotedBy pivot_1} {L_lowerTriangular_1 : L_1.IsLowerTriangular}
  {L_diag_ne_zero_1 : ∀ (i : m), L_1.diag i ≠ 0},
  { L := L, σ := σ, pivot := pivot, isPivotedBy := isPivotedBy, L_lowerTriangular := L_lowerTriangular,
        L_diag_ne_zero := L_diag_ne_zero } =
      { L := L_1, σ := σ_1, pivot := pivot_1, isPivotedBy := isPivotedBy_1, L_lowerTriangular := L_lowerTriangular_1,
        L_diag_ne_zero := L_diag_ne_zero_1 } →
    L = L_1 ∧ σ = σ_1 ∧ pivot = pivot_1
-- Batteries.Data.Nat.Gcd
/-- **Alias** of `Nat.Coprime.mul_left`. -/
Nat.Coprime.mul : ∀ {m k n : ℕ}, m.Coprime k → n.Coprime k → (m * n).Coprime k
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.uset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i : ℕ} {y : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5} {fvarId_1 : Lean.FVarId}
  {i_1 : ℕ} {y_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5},
  Lean.Compiler.LCNF.CodeDecl.uset fvarId i y h = Lean.Compiler.LCNF.CodeDecl.uset fvarId_1 i_1 y_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `Prod.snd` as a bundled `AddActionHom`.  -/
AddActionHom.snd : (M : Type u_1) → (α : Type u_2) → (β : Type u_3) → [inst : VAdd M α] → [inst_1 : VAdd M β] → α × β →ₑ[id] β
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The second exterior derivative of a sufficiently smooth differential form is zero.  -/
extDerivWithin_extDerivWithin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 r ω s x →
    minSmoothness 𝕜 2 ≤ r →
      UniqueDiffOn 𝕜 s → x ∈ closure (interior s) → x ∈ s → extDerivWithin (extDerivWithin ω s) s x = 0
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- `(fun x ↦ c) =O[l] f` if and only if `f` is bounded away from zero.  -/
Asymptotics.isBigO_const_left_iff_pos_le_norm : ∀ {α : Type u_1} {E' : Type u_6} {E'' : Type u_9} [inst : SeminormedAddCommGroup E'] [inst_1 : NormedAddCommGroup E'']
  {f' : α → E'} {l : Filter α} {c : E''}, c ≠ 0 → ((fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_iSup_of_monotone : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {m1 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeSup ι] [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  (∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) →
    (∀ (i : ι), m i ≤ _mΩ) → m1 ≤ _mΩ → Monotone m → ProbabilityTheory.Indep (⨆ i, m i) m1 μ
-- Mathlib.Algebra.Group.Action.Basic
/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`.  -/
arrowAction : {G : Type u_7} → {A : Type u_8} → {B : Type u_9} → [inst : DivisionMonoid G] → [MulAction G A] → MulAction G (A → B)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.mul : Nat.Primrec (Nat.unpaired fun x1 x2 => x1 * x2)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- A permutation restricted to the support of a cycle factor is that cycle factor  -/
Equiv.Perm.subtypePerm_on_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset),
  g.subtypePerm ⋯ = c.subtypePermOfSupport
-- Lean.Server.AsyncList
/-- Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well.
The returned boolean indicates whether the complete `AsyncList` was returned, or whether only a
proper prefix was returned.
 -/
Lean.AsyncList.getFinishedPrefix : {ε α : Type} → Lean.AsyncList ε α → BaseIO (List α × Option ε × Bool)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsFunctor_obj_X_carrier : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  ↑(((groupCohomology.cochainsFunctor k G).obj A).X n) = ((Fin n → G) → ↑A)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {W : ι → CategoryTheory.MorphismProperty C}
  [∀ (i : ι), (W i).RespectsIso], (⨅ i, W i).RespectsIso
-- Init.Control.Lawful.Instances
StateT.run_seqLeft : ∀ {m : Type u → Type u_1} {α β σ : Type u} [inst : Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ),
  (x <* y).run s = do
    let p ← x.run s
    let p' ← y.run p.2
    pure (p.1, p'.2)
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.smul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α} {a : α},
  IsUpperSet s → IsUpperSet (a • s)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.id_apply : ∀ (V : Type u_1) [inst : SeminormedAddCommGroup V] (a : V), (NormedAddGroupHom.id V) a = a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K) {Z : C}
  (h : (CategoryTheory.Limits.colimit F).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.evaluation K C).obj k)) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).inv h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F j).app k) h
-- Mathlib.Algebra.Group.ULift
ULift.zero.eq_1 : ∀ {α : Type u} [inst : Zero α], ULift.zero = { zero := { down := 0 } }
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_mul_right : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, (f * g).NeBot → g.NeBot
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.isNontrivial_restrict : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne], v.restrict.IsNontrivial
-- Mathlib.Algebra.Tropical.BigOperators
Multiset.trop_sum : ∀ {R : Type u_1} [inst : AddCommMonoid R] (s : Multiset R), Tropical.trop s.sum = (Multiset.map Tropical.trop s).prod
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- Given a functor `ι : A ⥤ C` from a preadditive category to a triangulated category,
a morphism `X₁ ⟶ X₂` in `A` is admissible if, when we complete `ι.obj f₁` in
a distinguished triangle `ι.obj X₁ ⟶ ι.obj X₂ ⟶ X₃ ⟶ (ι.obj X₁)⟦1⟧`,
there exists objects `K` and `Q`, and a distinguished triangle
`(ι.obj K)⟦1⟧ ⟶ X₃ ⟶ (ι.obj Q) ⟶ ...`.  -/
CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  CategoryTheory.Functor A C → CategoryTheory.MorphismProperty A
-- Mathlib.Data.NNReal.Defs
/-- Coercion `ℝ≥0 → ℝ` as a `RingHom`.

TODO: what if we define `Coe ℝ≥0 ℝ` using this function?  -/
NNReal.toRealHom : NNReal →+* ℝ
-- Mathlib.Order.Filter.Germ.Basic
/-- The germ corresponding to a global function.  -/
Filter.Germ.ofFun : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → (α → β) → l.Germ β
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.roth_lower_bound : ∀ {N : ℕ}, ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ ↑(rothNumberNat N)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LaxLeftLinear C] (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d) =
    F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_map_eq_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).degree = p.degree
-- Mathlib.Order.Concept
/-- The upper polar of `s : Set α` along a relation `r : α → β → Prop` is the set of all elements
which `r` relates to all elements of `s`.  -/
upperPolar : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → Set α → Set β
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongr_trans : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₃ : Type u_11} {R₁' : Type u_12} {R₂' : Type u_13} {R₃' : Type u_14}
  {M₁ : Type u_17} {M₂ : Type u_18} {M₃ : Type u_19} {M₁' : Type u_20} {M₂' : Type u_21} {M₃' : Type u_22}
  [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : CommSemiring R₁']
  [inst_4 : CommSemiring R₂'] [inst_5 : CommSemiring R₃'] [inst_6 : AddCommMonoid M₁] [inst_7 : AddCommMonoid M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : AddCommMonoid M₁'] [inst_10 : AddCommMonoid M₂'] [inst_11 : AddCommMonoid M₃']
  [inst_12 : Module R₁ M₁] [inst_13 : Module R₂ M₂] [inst_14 : Module R₃ M₃] [inst_15 : Module R₁' M₁']
  [inst_16 : Module R₂' M₂'] [inst_17 : Module R₃' M₃'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₂₃ : R₂ →+* R₃}
  {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₂'₃' : R₂' →+* R₃'} {σ₃'₂' : R₃' →+* R₂'} {σ₁'₃' : R₁' →+* R₃'} {σ₃'₁' : R₃' →+* R₁'} {σ₁₁' : R₁ →+* R₁'}
  {σ₂₂' : R₂ →+* R₂'} {σ₃₃' : R₃ →+* R₃'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} {σ₃₂' : R₃ →+* R₂'}
  {σ₂₃' : R₂ →+* R₃'} {σ₃₁' : R₃ →+* R₁'} {σ₁₃' : R₁ →+* R₃'}, ⋯
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.iteratedFDeriv_aux : ∀ {ι : Type u_3} {M₁ : ι → Type u_1} {α : Type u_2} [inst : DecidableEq α] (s : Set ι)
  [inst_1 : DecidableEq { x // x ∈ s }] (e : α ≃ ↑s) (m : α → (i : ι) → M₁ i) (a : α) (z : (i : ι) → M₁ i),
  (fun i => Function.update m a z (e.symm i) ↑i) = fun i =>
    Function.update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalNonAssocRing : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalNonAssocRing R] → [IsTopologicalRing R] → NonUnitalNonAssocRing (SeparationQuotient R)
-- Std.Data.DHashMap.Basic
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.DHashMap.toList : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → List ((a : α) × β a)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instDistrib : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Distrib (FreeAlgebra R X)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A morphism is called a degeneracy if it is a `σ i` for some `i : Fin (n + 1)`.  -/
SimplexCategoryGenRel.degeneracies : CategoryTheory.MorphismProperty SimplexCategoryGenRel
-- Mathlib.MeasureTheory.Group.Integral
/-- If some left-translate of a function negates it, then the integral of the function with respect
to a left-invariant measure is 0.  -/
MeasureTheory.integral_eq_zero_of_mul_left_eq_neg : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulLeftInvariant],
  (∀ (x : G), f (g * x) = -f x) → ∫ (x : G), f x ∂μ = 0
-- Init.GetElem
_private.Init.GetElem.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Lean.Server.References
Lean.Server.References.MatchedDefinition.mk.injEq : ∀ {α : Type} (mod : Lean.Name) (modUri : Lean.Lsp.DocumentUri) (ident : α) (range : Lean.Lsp.Range) (mod_1 : Lean.Name)
  (modUri_1 : Lean.Lsp.DocumentUri) (ident_1 : α) (range_1 : Lean.Lsp.Range),
  ({ mod := mod, modUri := modUri, ident := ident, range := range } =
      { mod := mod_1, modUri := modUri_1, ident := ident_1, range := range_1 }) =
    (mod = mod_1 ∧ modUri = modUri_1 ∧ ident = ident_1 ∧ range = range_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp},
  Array.map Sigma.fst t.toArray = t.keysArray
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.differentiableOn_weierstrassP : ∀ (L : PeriodPair), DifferentiableOn ℂ L.weierstrassP (↑L.lattice)ᶜ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.toSpecΓ '' X.zeroLocus s = PrimeSpectrum.zeroLocus s
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_coeff_cert : ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitEpi.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) f = CategoryTheory.CategoryStruct.id Y
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.triangleLTGE a ⟶ t.triangleLTGE b`
when `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (a b : ℤ) → a ≤ b → (t.triangleLTGE a ⟶ t.triangleLTGE b)
-- Lean.Expr
/-- Polymorphic operation for generating unique/fresh metavariable identifiers.
It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
Lean.mkFreshMVarId : {m : Type → Type} → [Monad m] → [Lean.MonadNameGenerator m] → m Lean.MVarId
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.initial_fst_of_isCofiltered_costructuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B]
  [∀ (b : B), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow L (R.obj b))],
  (CategoryTheory.Comma.fst L R).Initial
-- Mathlib.Algebra.Group.Basic
mul_right_surjective : ∀ {G : Type u_3} [inst : Group G] (a : G), Function.Surjective fun x => x * a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteGrp.Hom.mk : {A B : ProfiniteGrp.{u}} → (↑A.toProfinite.toTop →ₜ* ↑B.toProfinite.toTop) → A.Hom B
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {t : Set E},
  s =ᶠ[nhds x] t → (ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n f t x)
-- Std.Http.Data.Method
/-- Retrieve properties of a resource (WebDAV).
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.1
 -/
Std.Http.Method.propfind : Std.Http.Method
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn_obj : ∀ (n : ℕ) (i : Fin (n + 1)) (x : SimplexCategoryᵒᵖ),
  (SSet.horn n i).obj x = {s | Set.range ⇑(SSet.stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
-- Init.Data.UInt.Lemmas
UInt16.sub_le : ∀ {a b : UInt16}, b ≤ a → a - b ≤ a
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [IsDomain R] [inst_5 : NormalizedGCDMonoid R] {p : Polynomial K},
  p ≠ 0 → IsUnit (IsLocalization.integerNormalization (nonZeroDivisors R) p).primPart → IsUnit p
-- Mathlib.Order.Filter.Basic
Filter.not_disjoint_self_iff : ∀ {α : Type u} {f : Filter α}, ¬Disjoint f f ↔ f.NeBot
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.comulAlgHom_comp_mapRingHom : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] (f : R →+* S),
  (Bialgebra.comulAlgHom S (AddMonoidAlgebra S M)).comp (AddMonoidAlgebra.mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (AddMonoidAlgebra.mapRingHom M f) (AddMonoidAlgebra.mapRingHom M f) ⋯ ⋯).comp
      (Bialgebra.comulAlgHom R (AddMonoidAlgebra R M)).toRingHom
-- Init.Data.Array.Lemmas
List.unzip_toArray : ∀ {α : Type u_1} {β : Type u_2} {as : List (α × β)}, as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Icc a b` where `a` and `b` are numerals.

**Warnings**:
* With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
* Make sure to exclude `Finset.insert_eq_of_mem` from your simp call when using this simproc. This
  avoids a quadratic time performance hit.  -/
Finset.Icc_ofNat_ofNat : Lean.Meta.Simp.Simproc
-- Init.Data.Rat.Lemmas
Rat.divInt_zero : ∀ (n : ℤ), Rat.divInt n 0 = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.mk.injEq : ∀ {numVarsSucc : ℕ} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
  (nodupkey :
    autoParam (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause ∨ (l, false) ∉ clause)
      Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam)
  (nodup : autoParam (List.Nodup clause) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam)
  (clause_1 : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
  (nodupkey_1 :
    autoParam
      (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause_1 ∨ (l, false) ∉ clause_1)
      Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam)
  (nodup_1 : autoParam (List.Nodup clause_1) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam),
  ({ clause := clause, nodupkey := nodupkey, nodup := nodup } =
      { clause := clause_1, nodupkey := nodupkey_1, nodup := nodup_1 }) =
    (clause = clause_1)
-- Init.Data.Iterators.Basic
Std.IterM.step_mk : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : α),
  { internalState := it }.step = Std.Iterator.step { internalState := it }
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.WeaklyEtale
-- Mathlib.Algebra.Group.Action.Prod
Prod.vaddCommClassBoth : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add N] [inst_1 : Add P] [inst_2 : VAdd M N] [inst_3 : VAdd M P]
  [VAddCommClass M N N] [VAddCommClass M P P], VAddCommClass M (N × P) (N × P)
-- Mathlib.Data.Setoid.Basic
Setoid.inf_iff_and : ∀ {α : Type u_1} {r s : Setoid α} {x y : α}, (r ⊓ s) x y ↔ r x y ∧ s x y
-- Mathlib.Data.Fintype.Defs
Fintype.decidablePiFintype : {α : Type u_5} → {β : α → Type u_4} → [(a : α) → DecidableEq (β a)] → [Fintype α] → DecidableEq ((a : α) → β a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKeyD_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_deleteEdges_le : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set (Sym2 V)), (G'.deleteEdges s).spanningCoe ≤ G'.spanningCoe
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- **Alias** of `Summable.hasFiniteSupport_of_discreteTopology`. -/
Summable.finite_support_of_discreteTopology : ∀ {α : Type u_5} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α),
  Summable f → Function.HasFiniteSupport f
-- Init.Data.String.Basic
String.get? : String → String.Pos.Raw → Option Char
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → ∀ {Y : C} (f : X ⟶ Y), CategoryTheory.Mono f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.insert : ∀ {𝕜 : 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 : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → HasMFDerivAt[insert x s] f x f'
-- Mathlib.Data.BitVec
BitVec.toFin_pow : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), (x ^ n).toFin = x.toFin ^ n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.maxKey?.isSome = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_8 : ∀ (a b : Lean.Grind.CommRing.Expr),
  (a.sub b).toPoly = a.toPoly.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly)
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_a_cert : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R ≃+* P) (hIJ : I = Ideal.comap f J) (a : Localization.AtPrime J),
  (Localization.localRingEquiv I J f hIJ).symm a = (Localization.localRingHom J I ↑f.symm ⋯) a