mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Util
Lean.Elab.checkSyntaxNodeKindAtNamespaces : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → Lean.Name → m Lean.Name
-- Batteries.Tactic.Init
/-- `fapply e` is like `apply e` but it adds goals in the order they appear,
rather than putting the dependent goals first.
 -/
Batteries.Tactic.tacticFapply_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Under.instHasInitial : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] {X : T},
  CategoryTheory.Limits.HasInitial (CategoryTheory.Under X)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get? (t₁ \ t₂) k = Std.DTreeMap.Const.get? t₁ k
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Map a function over the support of a standard simplex.
For each n : N, the weight is the sum of weights of all m : M with g m = n.
 -/
Convexity.StdSimplex.map : {R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [IsStrictOrderedRing R] →
        {M : Type v} → {N : Type w} → (M → N) → Convexity.StdSimplex R M → Convexity.StdSimplex R N
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivAt.mul` -/
HasDerivAt.fun_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasDerivAt c c' x → HasDerivAt d d' x → HasDerivAt (fun i => c i * d i) (c' * d x + c x * d') x
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.IsPrimary.comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {I : Ideal S},
  I.IsPrimary → ∀ (φ : R →+* S), (Ideal.comap φ I).IsPrimary
-- Mathlib.Order.Atoms
Prop.instIsSimpleOrderProp : IsSimpleOrder Prop
-- Mathlib.Topology.Algebra.LinearTopology
/-- Assume that `M` is a module over two rings `R` and `R'`, and that its topology
is linear with respect to each of these rings. Then, it has a basis of neighborhoods of zero
made of sub-`(R, R')`-bimodules.

The proof is inspired by lemma 9 in [I. Kaplansky, *Topological Rings*](kaplansky_topological_1947).
TODO: Formalize the lemma in its full strength.

Note: due to the lack of a satisfying theory of sub-bimodules, we use `AddSubgroup`s with
extra conditions.  -/
IsLinearTopology.hasBasis_subbimodule : ∀ (R : Type u_1) (R' : Type u_2) {M : Type u_3} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module R' M] [SMulCommClass R R' M] [inst_6 : TopologicalSpace M]
  [IsLinearTopology R M] [IsLinearTopology R' M],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0 ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun I =>
    ↑I
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.id_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  (S : CategoryTheory.Span Wₗ Wᵣ c c'),
  (CategoryTheory.CategoryStruct.id S).hom = CategoryTheory.CategoryStruct.id S.apex
-- Mathlib.Analysis.Convex.Strict.Extreme
StrictConvex.extremePoints_eq_sdiff_interior : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [Nontrivial A] {S : Set A},
  StrictConvex ℝ S → Set.extremePoints ℝ S = S \ interior S
-- Mathlib.NumberTheory.Real.Irrational
irrational_neg_iff : ∀ {x : ℝ}, Irrational (-x) ↔ Irrational x
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ'_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  (W.preΨ' n).natDegree ≤ (n ^ 2 - if Even n then 4 else 1) / 2
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsSeparator.def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsSeparator G →
    ∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
      (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g
-- Mathlib.GroupTheory.OrderOfElement
injective_zpow_iff_not_isOfFinOrder : ∀ {G : Type u_1} [inst : Group G] {x : G}, (Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The (almost) optimal value of `n` in `Behrend.bound_aux`.  -/
Behrend.nValue : ℕ → ℕ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.union_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Order.Hom.Basic
OrderEmbedding.map_inf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : α ↪o β) (x y : α),
  f (x ⊓ y) ≤ f x ⊓ f y
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_add_cos : ∀ (x y : ℝ), Real.cos x + Real.cos y = 2 * Real.cos ((x + y) / 2) * Real.cos ((x - y) / 2)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_singleton : ∀ {X : Type u_2} [inst : EMetricSpace X] (x : X), dimH {x} = 0
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_eq_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : TopologicalSpace.Compacts α}, ↑s = ∅ ↔ s = ⊥
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.trans_isLittleO : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =Θ[l] g → g =o[l] k → f =o[l] k
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_prod_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {L : Type u_5} [inst_4 : RCLike L]
  (f : α → L) (g : β → L), ∫ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) * ∫ (y : β), g y ∂ν
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isClosedEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], Topology.IsClosedEmbedding fun x => {x}
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
instHasOuterApproxClosedOfPseudoMetrizableSpace : ∀ (X : Type u_1) [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X], HasOuterApproxClosed X
-- Std.Time.Zoned.ZoneRules
/-- Time based on a wall clock, which can include daylight saving adjustments.
 -/
Std.Time.TimeZone.StdWall.wall : Std.Time.TimeZone.StdWall
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.zero_sub_add_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → 0 - a + a = 0
-- Mathlib.Order.WithBot
WithBot.coe_inj : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Topology.UniformSpace.Defs
/-- See also `comp3_mem_uniformity`.  -/
comp_le_uniformity3 : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => s.comp (s.comp s)) ≤ uniformity α
-- Mathlib.Data.Finset.Sups
Finset.image_sdiff_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  Finset.image (Function.uncurry fun x1 x2 => x1 \ x2) (s ×ˢ t) = s.diffs t
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯)
      CategoryTheory.Abelian.SpectralObject.cyclesMap_i._auto_1 →
    CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) (X.iCycles f' g' n) =
      CategoryTheory.CategoryStruct.comp (X.iCycles f g n) ((X.H n).map β)
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J_det_mul_J_det : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  (Matrix.J l R).det * (Matrix.J l R).det = 1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
GradedRing.congr_simp : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : Semiring A] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] (𝒜 𝒜_1 : ι → σ),
  𝒜 = 𝒜_1 → GradedRing 𝒜 = GradedRing 𝒜_1
-- Mathlib.Tactic.CongrExclamation
/-- The configuration for the `congr!` tactic.  -/
Congr!.Config : Type
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)},
  CPolynomialOn 𝕜 (fun p => p.2.compContinuousLinearMap p.1) t
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.conjTranspose_mul : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → A.conjTranspose * A = ↑(Fintype.card n) • 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanFileProgressParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanFileProgressParams
-- Mathlib.Order.Category.BddDistLat
BddDistLat.dualEquiv_inverse : BddDistLat.dualEquiv.inverse = BddDistLat.dual
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_mono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.addEnergy t₁ ≤ s₂.addEnergy t₂
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mul_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Mul Y] (f g : LocallyConstant X Y) (x : X),
  (f * g) x = f x * g x
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsConnected.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [toIsPreconnected : CategoryTheory.IsPreconnected J]
  [is_nonempty : Nonempty J], CategoryTheory.IsConnected J
-- Mathlib.Topology.Algebra.Group.Basic
/-- Addition from the left in a topological additive group as a homeomorphism.  -/
Homeomorph.addLeft : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [SeparatelyContinuousAdd G] → G → G ≃ₜ G
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_sdiff : ∀ {α : Type u} {s t : Set α}, (s \ t).Finite → t.Finite → s.Finite
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_disjSups_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t : Finset α}, (s.disjSups t).Nonempty → t.Nonempty
-- Lean.ExtraModUses
Lean.ExtraModUse.mk.inj : ∀ {module : Lean.Name} {isExported isMeta : Bool} {module_1 : Lean.Name} {isExported_1 isMeta_1 : Bool},
  { module := module, isExported := isExported, isMeta := isMeta } =
      { module := module_1, isExported := isExported_1, isMeta := isMeta_1 } →
    module = module_1 ∧ isExported = isExported_1 ∧ isMeta = isMeta_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.mk.inj : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {hom : u.right ⟶ v.left}
  {comm :
    autoParam
      (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
        CategoryTheory.CategoryStruct.comp hom v.hom)
      CategoryTheory.Arrow.RightHomotopy.comm._autoParam}
  {hom_1 : u.right ⟶ v.left}
  {comm_1 :
    autoParam
      (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
        CategoryTheory.CategoryStruct.comp hom_1 v.hom)
      CategoryTheory.Arrow.RightHomotopy.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instInhabited : {α : Type u} → Inhabited (FreeAddGroup α)
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_single_single : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] [inst_2 : (a : α) → (b : β a) → Zero (γ a b)] (a : α) (b : β a) (x : γ a b),
  Sigma.uncurry (Pi.single a (Pi.single b x)) = Pi.single ⟨a, b⟩ x
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.inf_of_left : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (s ⊓ t).Finite
-- Mathlib.Order.Sublattice
Sublattice.coe_pi : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] (s : Set κ) (L : (i : κ) → Sublattice (π i)),
  ↑(Sublattice.pi s L) = s.pi fun i => ↑(L i)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_map_toList : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M), (List.map f s.toList).sum = s.sum f
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec_4 : (Lean.Grind.IntInterval.ii == Lean.Grind.IntInterval.ii) = true
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_sub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s - t).inf f = t.inf fun y => s.inf fun x => f (x - y)
-- Mathlib.Data.Nat.Factorization.Root
/-- The RHS is a noncomputable version of `Nat.ceilRoot` with better order-theoretic
properties.  -/
Nat.ceilRoot_def : ∀ {a n : ℕ}, n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2
-- Mathlib.Data.Finset.Lattice.Union
Finset.inf_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → α} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
  [inst_2 : DecidableEq β] (s : Finset γ) (t : γ → Finset β), (s.biUnion t).inf f = s.inf fun x => (t x).inf f
-- Mathlib.Order.Height
Set.exists_eq_chainHeight_of_finite : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.Finite → ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.asIso' f = { hom := CategoryTheory.inv f, inv := f, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Topology.EMetricSpace.Basic
/-- Expressing uniform convergence on a set using `edist`.  -/
EMetric.tendstoUniformlyOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι}
  {s : Set β}, TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.numerator_isAddUnit : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (s : ↥S),
  IsAddUnit (AddOreLocalization.numeratorHom ↑s)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w w' : V},
  G.IsCycles → ∀ (p : G.Walk v w), w ≠ w' → w' ∈ p.support → p.IsPath → G.Adj v w' → p.snd = w'
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_right_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m : M}, Function.Injective (MonoidAlgebra.single m)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) =
    CategoryTheory.CategoryStruct.comp (f₁ * f₂ * f₁⁻¹ * f₂⁻¹) h
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `AddMonoid.Coprod M N →+ M`.  -/
AddMonoid.Coprod.fst : {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddMonoid.Coprod M N →+ M
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  f =O[𝕜; l] g → (-f) =O[𝕜; l] g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.prod_mono : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] {s₁ s₂ : AffineSubspace k P} {t₁ t₂ : AffineSubspace k Q},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- `ModuleCat.Hom.hom` as an isomorphism of rings.  -/
ModuleCat.endRingEquiv : {R : Type u} → [inst : Ring R] → (M : ModuleCat R) → CategoryTheory.End M ≃+* (↑M →ₗ[R] ↑M)
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.mem_range_ofSubtype_iff : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p] {g : Equiv.Perm α},
  g ∈ Equiv.Perm.ofSubtype.range ↔ ↑g.support ⊆ Set.ofPred p
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.snd` as a continuous linear map.  -/
WithLp.sndL : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [inst : TopologicalSpace α] →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Semiring 𝕜] →
              [inst_3 : AddCommGroup α] →
                [inst_4 : AddCommGroup β] → [inst_5 : Module 𝕜 α] → [inst_6 : Module 𝕜 β] → WithLp p (α × β) →L[𝕜] β
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffWithinAt.snd : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'} {s : Set N} {x : N},
  ContMDiffWithinAt J (I.prod I') n f s x → ContMDiffWithinAt J I' n (fun x => (f x).2) s x
-- Mathlib.Data.PNat.Defs
PNat.not_lt_one : ∀ (n : ℕ+), ¬n < 1
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} (self : CategoryTheory.SmallObject.FunctorObjIndex f πX),
  CategoryTheory.CategoryStruct.comp self.t πX = CategoryTheory.CategoryStruct.comp (f self.i) self.b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E E_1 : CategoryTheory.PreZeroHypercover S)
  (e_E : E = E_1) [inst_1 : E.HasPullbacks], E.toPreOneHypercover = E_1.toPreOneHypercover
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprLevelMVarId_mathlib : Lean.ToExpr Lean.LevelMVarId
-- Mathlib.Topology.UniformSpace.Defs
nhds_basis_uniformity' : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s → ∀ {x : α}, (nhds x).HasBasis p fun i => UniformSpace.ball x (s i)
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `Max` across an `Equiv`.  -/
Equiv.max : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Max β] → Max α
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.root_left_of_root_gcd : ∀ {R : Type u} {k : Type y} [inst : Field R] [inst_1 : CommSemiring k] [inst_2 : DecidableEq R] {ϕ : R →+* k}
  {f g : Polynomial R} {α : k}, Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 → Polynomial.eval₂ ϕ α f = 0
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.flip_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M)
  (h : optParam (Module.IsReflexive R N) ⋯), e.flip.flip = e
-- Lean.Data.Lsp.CodeActions
/-- Requested kind of actions to return.

Actions not of this kind are filtered out by the client before being
shown. So servers can omit computing them.
 -/
Lean.Lsp.CodeActionContext.only? : Lean.Lsp.CodeActionContext → Option (Array Lean.Lsp.CodeActionKind)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.unassignedMVarsEqualUpToIdsCore : Lean.MVarId → Lean.MVarId → Aesop.EqualUpToIdsM Bool
-- Mathlib.MeasureTheory.Integral.Pi
/-- On a finite product space in `n` variables, for a natural number `n`, a product of integrable
functions depending on each coordinate is integrable.  -/
MeasureTheory.Integrable.fin_nat_prod : ∀ {𝕜 : Type u_1} [inst : NormedCommRing 𝕜] {n : ℕ} {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)}
  {μ : (i : Fin n) → MeasureTheory.Measure (E i)} [∀ (i : Fin n), MeasureTheory.SigmaFinite (μ i)]
  {f : (i : Fin n) → E i → 𝕜},
  (∀ (i : Fin n), MeasureTheory.Integrable (f i) (μ i)) →
    MeasureTheory.Integrable (fun x => ∏ i, f i (x i)) (MeasureTheory.Measure.pi μ)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_preimage_down : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_of_base_le_one : ∀ {p : ℕ}, p ≤ 1 → ∀ (n : ℕ), p.maxPowDvdDiv n = (0, n)
-- Batteries.Data.List.Basic
List.any.eq_2 : ∀ {α : Type u} (x : α → Bool) (h : α) (t : List α), (h :: t).any x = (x h || t.any x)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_mul_lcm : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R),
  EuclideanDomain.gcd x y * EuclideanDomain.lcm x y = x * y
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_sqrt : ∀ {x : ℝ}, 0 ≤ x → Real.log √x = Real.log x / 2
-- Init.Data.Array.Lex.Lemmas
Array.le_refl : ∀ {α : Type u_1} [inst : LT α] [i₀ : Std.Irrefl fun x1 x2 => x1 < x2] (xs : Array α), xs ≤ xs
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.neg : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {φ : MvPolynomial σ R}, φ.IsSymmetric → (-φ).IsSymmetric
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `pointwiseCocone` is indeed a colimit cocone.  -/
CategoryTheory.Limits.pointwiseIsColimit : {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)) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pointwiseCocone F)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotation.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  WittVector.frobeniusRotation p ha₁ ha₂ = WittVector.mk p (WittVector.frobeniusRotationCoeff p ha₁ ha₂)