mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.equivalence_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Idempotents.DoldKan.equivalence.functor = CategoryTheory.Idempotents.DoldKan.N
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_sub_le_iff_left : ∀ {R : Type u} {n : ℕ} [inst : Ring R] {p q : Polynomial R}, q.natDegree ≤ n → ((p - q).natDegree ≤ n ↔ p.natDegree ≤ n)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_pOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology], S.f = 0 → CategoryTheory.IsIso S.pOpcycles
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `‖Complex.exp z‖ → ∞` as `Complex.re z → ∞`.  -/
Complex.tendsto_exp_comap_re_atTop : Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atTop) (Bornology.cobounded ℂ)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A morphism `f` satisfies `[Cofibration f]` if it belongs to `cofibrations C`.  -/
HomotopicalAlgebra.Cofibration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (X ⟶ Y) → [HomotopicalAlgebra.CategoryWithCofibrations C] → Prop
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.le_antisymm : ∀ {α : Type u} [self : Std.LinearOrderPackage α] (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_toFun : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : Fin (List.length basis)} {r : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis (↑n) r).toFun = basis[n] ^ r
-- Mathlib.Data.UInt
UInt64.toBitVec_intCast : ∀ (z : ℤ), (↑z).toBitVec = ↑z
-- Batteries.Data.Vector.Lemmas
Vector.scanl.eq_1 : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} (f : β → α → β) (init : β) (as : Vector α n),
  Vector.scanl f init as = (Vector.scanlM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u`.  -/
mem_nhdsGE_iff_exists_Ico_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α}
  {s : Set α}, s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
-- Mathlib.Analysis.Convex.Topology
/-- If `s` is a convex set, then `a • interior s + b • s ⊆ interior s` for all `0 < a`, `0 ≤ b`,
`a + b = 1`. See also `Convex.combo_interior_closure_subset_interior` for a stronger version.  -/
Convex.combo_interior_self_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • interior s + b • s ⊆ interior s
-- Mathlib.Topology.DiscreteSubset
mem_codiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X},
  S ∈ Filter.codiscrete X ↔ ∀ (x : X), Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal Sᶜ)
-- Mathlib.Data.ZMod.Units
ZMod.coe_unitOfIsCoprime : ∀ {m : ℕ} (n : ℤ) (h : IsCoprime n ↑m), ↑(ZMod.unitOfIsCoprime n h) = ↑n
-- Lean.Compiler.IR.Basic
/-- `let x : ty := e; b`  -/
Lean.IR.FnBody.vdecl : Lean.IR.VarId → Lean.IR.IRType → Lean.IR.Expr → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is maximized when `f` and
`g` monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_mul_le_sum_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f (σ i) * g i ≤ ∑ i ∈ s, f i * g i
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.mkImplType : Lean.Elab.ComputedFields.M Lean.Name
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∩ t₂).getKeyD k fallback = if k ∈ t₂ then t₁.getKeyD k fallback else fallback
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.header.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.toOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)),
  f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯ }
-- Lean.Meta.Tactic.Grind.Split
/-- Selects a case-split from the list of candidates, performs the split and applies
continuation to all subgoals.
If a subgoal is solved without using new hypotheses, closes the original goal using this proof. That is,
it performs non-chronological backtracking.

If `stopsAtFirstFailure = true`, it stops the search as soon as the given continuation cannot solve a subgoal.

If `compress = true`, then it uses `<;>` to generate the resulting tactic sequence if all subgoal sequences are
identical. For example, suppose that the following sequence is generated with `compress = false`
```
cases #50fc
next => lia
next => lia
```
Then with `compress = true` it generates `cases #50fc <;> lia`
 -/
Lean.Meta.Grind.Action.splitNext : optParam Bool true → optParam Bool true → Lean.Meta.Grind.Action
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffOn.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n g s → ContDiffOn ℝ n (fun x => inner 𝕜 (f x) (g x)) s
-- Mathlib.Analysis.LocallyConvex.Separation
/-- Given a set `s` which is a convex neighbourhood of `0` and a point `x₀` outside of it, there is
a continuous linear functional `f` separating `x₀` and `s`, in the sense that it sends `x₀` to 1 and
all of `s` to values strictly below `1`.  -/
separate_convex_open_set : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] {s : Set E},
  0 ∈ s → Convex ℝ s → IsOpen s → ∀ {x₀ : E}, x₀ ∉ s → ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
-- Mathlib.Combinatorics.Graph.Delete
Graph.vertexSet_restrict : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β), (G.restrict E₀).vertexSet = G.vertexSet
-- Lean.Elab.ElabRules
Lean.Elab.Command.elabElabRulesAux : Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
  Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") →
    Lean.TSyntax `Lean.Parser.Term.attrKind →
      Lean.SyntaxNodeKind →
        Option Lean.Ident →
          Option Lean.Ident →
            Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.Elab.Command.CommandElabM Lean.Syntax
-- Lean.Parser.Term
Lean.Parser.Term.funBinder : Lean.Parser.Parser
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_monotoneOn : MonotoneOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Extension.cotangentComplex_injective_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (P : Algebra.Extension R A)
  [Algebra.FormallySmooth R P.Ring], Function.Injective ⇑P.cotangentComplex ↔ Subsingleton (Algebra.H1Cotangent R A)
-- Mathlib.Data.Nat.Cast.Defs
_private.Mathlib.Data.Nat.Cast.Defs.0.Nat.unaryCast.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prevn_zero : ∀ {s : String.Slice} {p : s.Pos}, p.prevn 0 = p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (t.alter k f).getKeyD k fallback = if (f t[k]?).isSome = true then k else fallback
-- Init.Data.Dyadic.Basic
Dyadic.ofOdd.injEq : ∀ (n k : ℤ) (hn : n % 2 = 1) (n_1 k_1 : ℤ) (hn_1 : n_1 % 2 = 1),
  (Dyadic.ofOdd n k hn = Dyadic.ofOdd n_1 k_1 hn_1) = (n = n_1 ∧ k = k_1)
-- Mathlib.Data.Set.Restrict
Set.injective_codRestrict : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
  Function.Injective (Set.codRestrict f s h) ↔ Function.Injective f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.union_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Init.Data.Int.Lemmas
Int.add_sub_add_left : ∀ (k n m : ℤ), k + n - (k + m) = n - m
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_left_nth : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (i : ℤ),
  (Turing.Tape.move Turing.Dir.left T).nth i = T.nth (i - 1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_iff_isZero_cokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.Epi f ↔ CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.goals : Lean.Widget.InteractiveGoals → Array Lean.Widget.InteractiveGoal
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.ker_eq_bot_of_mono : ∀ {A B : AddGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f], (AddGrpCat.Hom.hom f).ker = ⊥
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.conjMap_comp_inv_apply : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(SubMulAction.ofStabilizer G a)),
  (SubMulAction.ofStabilizer.conjMap ⋯) ((SubMulAction.ofStabilizer.conjMap hg) x) = x
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_atTop_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {f : α → β},
  Filter.map f Filter.atTop = ⨅ a, Filter.principal (f '' {a' | a ≤ a'})
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.instFunLike : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → (S : AddGroupExtension N E G) → FunLike S.Section G E
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- A term in a valued CSP instance over the template `Γ`.  -/
ValuedCSP.Term : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → ValuedCSP D C → Type u_3 → Type (max (max u_1 u_2) u_3)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
finite sets `s` and `t` and a natural number `b` such that `#t * n ≤ #s`, there exists
`y ∈ t` such that its preimage in `s` has at least `n` elements. See also
`Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to` for a stronger statement.  -/
Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  (∀ a ∈ s, f a ∈ t) → t.Nonempty → t.card * n ≤ s.card → ∃ y ∈ t, n ≤ {x ∈ s | f x = y}.card
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.order_toSubring : ∀ {σ : Type u_1} {R : Type u_3} [inst : Ring R] (p : MvPowerSeries σ R) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T), (p.toSubring T hp).order = p.order
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
_private.Mathlib.FieldTheory.AbsoluteGaloisGroup.0.Field.termG_K : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Constructor for weighted cones.  -/
CategoryTheory.Limits.WeightedCone.mk : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {W : CategoryTheory.Functor J (Type w)} →
          {F : CategoryTheory.Functor J C} →
            (pt : C) →
              (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)) →
                (∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
                    CategoryTheory.CategoryStruct.comp (π x) (F.map f) =
                      π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)) →
                  CategoryTheory.Limits.WeightedCone W F
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfRightInverse_symm_apply : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) (a : B),
  (Ideal.quotientKerAlgEquivOfRightInverse hf).symm a = (Ideal.Quotient.mk (RingHom.ker ↑f)) (g a)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_neg`. -/
Antivary.of_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Antivary (-f) (-g) → Antivary f g
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppLid_self : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R],
  finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ
-- Mathlib.Data.Fin.Tuple.Finset
Finset.map_snocEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.castSucc) → Prop)
  [inst : DecidablePred P],
  Finset.map (Fin.snocEquiv α).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (Fin.init r)}) =
    S (Fin.last n) ×ˢ {r ∈ Fintype.piFinset (Fin.init S) | P r}
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given finite sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` times the product of
`f i` over `i ∈ s ∩ t` equals the product of `f i` over `i ∈ s` times the product of `f i`
over `i ∈ t`.  -/
finprod_mem_union_inter : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  s.Finite →
    t.Finite →
      (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
        (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.MonObj X],
  autoParam (CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul)
      CategoryTheory.IsCommMonObj.mul_comm._autoParam →
    CategoryTheory.IsCommMonObj X
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.toBoundedOrder : {α : Type u_2} → [inst : HeytingAlgebra α] → BoundedOrder α
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The homological Euler characteristic as a sum over all indices using `finsum`.
This is the Euler characteristic computed from the homology groups rather than
the original complex. Defaults to 0 if the support of the ranks is infinite.  -/
HomologicalComplex.homologyEulerChar : {R : Type u_1} →
  [inst : Ring R] →
    {ι : Type u_2} →
      {c : ComplexShape ι} →
        [c.EulerCharSigns] → (C : HomologicalComplex (ModuleCat R) c) → [∀ (i : ι), C.HasHomology i] → ℤ
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const_add : ∀ {α : Type u_1} {mα : MeasurableSpace α} (β : Type u_4) [inst : MeasurableSpace β] (μ ν : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.const β (μ + ν) = ProbabilityTheory.Kernel.const β μ + ProbabilityTheory.Kernel.const β ν
-- Batteries.Data.List.Scan
List.length_partialProds : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] {l : List α}, l.partialProds.length = l.length + 1
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The image of a face of a cone under an injective linear map is a face of the
image of the cone.  -/
PointedCone.IsFaceOf.map : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] (f : M →ₗ[R] N),
  Function.Injective ⇑f → F.IsFaceOf C → (PointedCone.map f F).IsFaceOf (PointedCone.map f C)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (CategoryTheory.ConcreteCategory.hom (X.evaluation U ↑x ⋯)) f = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Limits.Cocone.underPost_ι_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone D)
  (j : J) (k : CategoryTheory.Under j), (c.underPost j).ι.app k = CategoryTheory.Under.homMk (c.ι.app k.right) ⋯
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Division of rational functions.  -/
RatFunc.div : {K : Type u_1} → [inst : CommRing K] → [IsDomain K] → RatFunc K → RatFunc K → RatFunc K
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_pos_of_exponent_pos : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α],
  0 < AddMonoid.exponent M → ∀ (m : M) (a : α), 0 < AddAction.period m a
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instContinuousFourierInv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  ContinuousFourierInv ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.AlgebraicTopology.SingularSet
/-- The canonical map `Δ[n] ⟶ Simp(Δₜ[n])` (where `Δₜ[n]` is the topological `n`-simplex).  -/
SSet.stdSimplexToTop : SSet.stdSimplex ⟶ SimplexCategory.toTop.{u}.comp TopCat.toSSet
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_map_tmul_tmul_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} {κ : ι → Type u_2} {Λ : ι → Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : Coalgebra R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] {F : Type u_5} [inst_6 : FunLike F A B] [LinearMapClass F R A B] (f g h : F) (a : A)
  {repr : Coalgebra.Repr R a ι} {a₁ : (i : ι) → Coalgebra.Repr R (repr.left i) (κ i)}
  {a₂ : (i : ι) → Coalgebra.Repr R (repr.right i) (Λ i)},
  ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_zero_iff_norm_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α},
  Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun x => ‖f x‖) a (nhds 0)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Topology.Algebra.Group.Units
/-- The isomorphism of topological groups between the units of a product and
the product of the units.  -/
ContinuousMulEquiv.piUnits : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [inst_1 : (i : ι) → TopologicalSpace (M i)] → ((i : ι) → M i)ˣ ≃ₜ* ((i : ι) → (M i)ˣ)
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or `none` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.Const.get? : {α : Type u} → {δ : Type w} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => δ) → α → Option δ
-- Mathlib.Algebra.Group.Submonoid.Pointwise
coe_set_nsmul : ∀ {M : Type u_3} {S : Type u_6} [inst : AddMonoid M] [inst_1 : SetLike S M] [AddSubmonoidClass S M] {n : ℕ},
  n ≠ 0 → ∀ (H : S), n • ↑H = ↑H
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_monotone_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ},
  P.unop ≤ Q.unop ↔ P ≤ Q
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : K),
  (∀ (v : IsDedekindDomain.HeightOneSpectrum R), (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1) →
    x ∈ (algebraMap R K).range
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk_replaceFun : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f g : ℝ → ℝ),
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f).replaceFun g =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s g
-- Init.Data.Vector.Lemmas
Vector.flatten_replicate_singleton : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Vector.replicate n #v[a]).flatten = Vector.cast ⋯ (Vector.replicate n a)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (j : σ) (f : MvPolynomial σ R),
  MvPolynomial.degreeOf j (f * MvPolynomial.X j) = MvPolynomial.degreeOf j f + 1 ↔ f ≠ 0
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.eval_eq_smeval : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (p : Polynomial R), Polynomial.eval r p = p.smeval r
-- Mathlib.Topology.Order.Compact
instCompactIccSpaceOrderDual : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [CompactIccSpace α], CompactIccSpace αᵒᵈ
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf.congr_simp : ∀ {α : Type u_2} (f f_1 : Equiv.Perm α),
  f = f_1 →
    ∀ {inst : DecidableRel f.SameCycle} [inst_1 : DecidableRel f_1.SameCycle] (x x_1 : α),
      x = x_1 → f.cycleOf x = f_1.cycleOf x_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂UnopOfOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsTriangulatedClosed₂], P.unop.IsTriangulatedClosed₂
-- Mathlib.Algebra.Group.Fin.Basic
Fin.lt_one_iff : ∀ {n : ℕ} (x : Fin (n + 2)), x < 1 ↔ x = 0