mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeEquivalenceOpConeOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.coconeEquivalenceOpConeOp F =
    {
      functor :=
        { obj := fun c => Opposite.op c.op, map := fun {X Y} f => Quiver.Hom.op { hom := f.hom.op, w := ⋯ },
          map_id := ⋯, map_comp := ⋯ },
      inverse :=
        { obj := fun c => (Opposite.unop c).unop, map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ },
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)),
      counitIso :=
        CategoryTheory.Iso.refl
          ({ obj := fun c => (Opposite.unop c).unop, map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun c => Opposite.op c.op, map := fun {X Y} f => Quiver.Hom.op { hom := f.hom.op, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }),
      functor_unitIso_comp := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Init.Data.UInt.Bitwise
UInt32.zero_shiftRight : ∀ {a : UInt32}, 0 >>> a = 0
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_blockDiagonal : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] [inst_2 : Zero R] [inst_3 : DecidableEq p] {A : X → p → Matrix m n R},
  Continuous A → Continuous fun x => Matrix.blockDiagonal (A x)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_apply : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)) (i j : n),
  LinearMap.BilinForm.toMatrix' B i j = (B (Pi.single i 1)) (Pi.single j 1)
-- Mathlib.Algebra.Group.Defs
ZSMul.ofSMul.eq_1 : ∀ {M : Type u_2} [inst : SMul ℤ M], ZSMul.ofSMul = { zsmul := fun n x => SMul.smul n x }
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.ElimEmptyInductive.M : Type → Type
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {k : α}, t.insertMany [k] = t.insert k
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_of_Iio : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α},
  (∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)) → Measurable f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_neg_right : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P Q : W'.Point), P.sym2x (-Q) = P.sym2x Q
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasLimitsOfShape : ∀ (J : Type v) [inst : CategoryTheory.Category.{v_1, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J TopCat
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_toSubsemiring : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A),
  (Subalgebra.map f S).toSubsemiring = Subsemiring.map (↑f) S.toSubsemiring
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] (m : ℕ),
  (Matrix.diagonal fun x => ↑m) = ↑m
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.iff_exists_smul_integral : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {z : A} [IsReduced R],
  IsAlgebraic R z ↔ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
-- Init.Data.List.Lemmas
List.flatten_concat : ∀ {α : Type u_1} {L : List (List α)} {l : List α}, (L ++ [l]).flatten = L.flatten ++ l
-- Mathlib.CategoryTheory.Action.Continuous
DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] → CategoryTheory.HasForget₂ (DiscreteContAction V G) TopCat
-- Mathlib.Analysis.Normed.Module.Shrink
Shrink.instNormedAddCommGroup : {α : Type u_3} → [inst : Small.{v, u_3} α] → [NormedAddCommGroup α] → NormedAddCommGroup (Shrink.{v, u_3} α)
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 → ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1], FreeMonoid.countP p = FreeMonoid.countP p_1
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The cylinder object obtained by switching the two inclusions.  -/
HomotopicalAlgebra.Cylinder.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.Cylinder A → HomotopicalAlgebra.Cylinder A
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {hc : t.max! ∈ t}, t.get t.max! hc = t.max!
-- Mathlib.Algebra.CharP.Defs
CharP.char_is_prime_or_zero : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [hc : CharP R p],
  Nat.Prime p ∨ p = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.instEpiModuleCatGShortComplexH0 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupHomology.shortComplexH0 A).g
-- Init.Data.ByteArray.Bootstrap
List.toByteArray.match_1.congr_eq_1 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (x : List UInt8) (x_1 : ByteArray) (h_1 : (r : ByteArray) → motive [] r)
  (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r) (r : ByteArray),
  x = [] →
    x_1 = r →
      (match x, x_1 with
        | [], r => h_1 r
        | b :: bs, r => h_2 b bs r) ≍
        h_1 r
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_uInt16ToNat : ∀ (n : UInt16), USize.ofNatClamp n.toNat = n.toUSize
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.instIteratorIteratorIdOfUpwardEnumerable : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Iterator (Std.Rxi.Iterator α) Id α
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.Scheme.JointlySurjective K] [Nonempty ↥X] (𝒰 : AlgebraicGeometry.Scheme.Cover K X), Nonempty 𝒰.I₀
-- Mathlib.Algebra.Module.CharacterModule
/-- Any character `c` in `(A ⊗ B)⋆` induces a linear map `A → B⋆` by `a ↦ b ↦ c (a ⊗ b)`.
 -/
CharacterModule.curry : {R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → CharacterModule (TensorProduct R A B) →ₗ[R] A →ₗ[R] CharacterModule B
-- Mathlib.Data.Bool.Count
List.IsChain.count_not_eq_count : ∀ {l : List Bool},
  List.IsChain (fun x1 x2 => x1 ≠ x2) l → Even l.length → ∀ (b : Bool), List.count (!b) l = List.count b l
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.copy_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (s : Set A) (hs : s = ↑S),
  (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Order.Hom.Order
OrderHom.lattice : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Lattice β] → Lattice (α →o β)
-- Mathlib.MeasureTheory.Measure.Haar.Disintegration
/-- The image of an additive Haar measure under a surjective linear map is proportional to a given
additive Haar measure. The proportionality factor will be infinite if the linear map has a
nontrivial kernel.  -/
LinearMap.exists_map_addHaar_eq_smul_addHaar' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [BorelSpace F] [inst_9 : NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F)
  (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
  [inst_12 : LocallyCompactSpace E],
  Function.Surjective ⇑L →
    ∃ c, 0 < c ∧ c < ⊤ ∧ MeasureTheory.Measure.map (⇑L) μ = (c * MeasureTheory.Measure.addHaar Set.univ) • ν
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_biSup_limsup : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {p : Set ι → Prop}
  {f : Filter ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        ∀ {t : Set ι}, p t → ProbabilityTheory.Kernel.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.saturate.I₀} (k : E.saturate.I₁ i j),
  E.fromSaturateOfHasPullbacks.s₁ k = PUnit.unit
-- Mathlib.RingTheory.FormalGroup.Basic
/-- Given a formal group `F`, `F.IsComm` is a proposition that $F(X,Y) = F(Y,X)$.  -/
FormalGroup.IsComm : {R : Type u_1} → [inst : CommRing R] → FormalGroup R → Prop
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.eq_of_isSt_real : ∀ {r s : ℝ}, (↑r).IsSt s → r = s
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_eq_one_iff : ∀ {a b : Ordinal.{u_4}}, a / b = 1 ↔ b ≤ a ∧ a < b * 2
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsQuasiPreprimitive.toIsPretransitive : ∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} [self : MulAction.IsQuasiPreprimitive G X],
  MulAction.IsPretransitive G X
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom = CategoryTheory.CategoryStruct.id F.X
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_6 : ∀ (coeff k : ℤ) (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.intMul k a) =
    bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul k) a
-- Mathlib.Data.Num.ZNum
ZNum.cast_sub : ∀ {α : Type u_1} [inst : AddCommGroupWithOne α] (m n : ZNum), ↑(m - n) = ↑m - ↑n
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.source_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} (self : Bundle.Trivialization F proj),
  self.source = proj ⁻¹' self.baseSet
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceBinPred : Lean.Name → ℕ → (ℤ → ℤ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Algebra.Algebra.TransferInstance
Equiv.algebraMap_def : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommSemiring R] (e : α ≃ β) [inst_1 : Semiring β]
  [inst_2 : Algebra R β] (r : R), (algebraMap R α) r = e.symm ((algebraMap R β) r)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.mk.inj : ∀ {α : Type} {root root_1 : Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)},
  { root := root } = { root := root_1 } → root = root_1
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.zero_mul_eq : ∀ {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a b : α}, a = 0 → R b 0 → a * b = 0
-- Mathlib.Topology.Order.LeftRight
Filter.Eventually.exists_gt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a : α} [(nhdsWithin a (Set.Ioi a)).NeBot]
  {p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ b, a < b ∧ p b
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bind_apply : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (b : β), (p.bind f) b = ∑' (a : α), p a * (f a) b
-- Mathlib.Order.WithBot
Equiv.withBotSubtypeNe_symm_apply_coe : ∀ {α : Type u_1} (x : α), ↑(Equiv.withBotSubtypeNe.symm x) = ↑x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_le_coe : ∀ {α : Type u_1} [inst : LE α] {a b : α}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp_i : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ)
      (groupHomology.shortComplexH2 B).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (groupHomology.chainsMap₂ f φ)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_inj : ∀ {b x y : Ordinal.{u_1}}, Ordinal.CNF.coeff b x = Ordinal.CNF.coeff b y ↔ x = y
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.map_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : PredOrder α] [NoMinOrder α]
  [inst_4 : PredOrder β] (f : α ≤i β) (a : α), f (Order.pred a) = Order.pred (f a)
-- Init.Data.SInt.Lemmas
Int64.toInt8_add : ∀ (a b : Int64), (a + b).toInt8 = a.toInt8 + b.toInt8
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_eq_addMonoidOf_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M}, AddLocalization.mk = (AddLocalization.addMonoidOf S).mk'
-- Mathlib.Data.Option.NAry
Option.map₂_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ}
  {ε : Type u_8} {ε' : Type u_9} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
    Option.map₂ f (Option.map₂ g a b) c = Option.map₂ f' a (Option.map₂ g' b c)
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_one : ∀ {α : Type u_2} [inst : One α] {p : α → Prop}, (∃ᶠ (x : α) in 1, p x) ↔ p 1
-- Batteries.Data.List.Perm
/-- `Subperm.idxInj` is an injective map from `Fin xs.length` to `Fin ys.length`
which exists when we have `xs <+~ ys`: conceptually it represents an embedding of
one list into the other. For example:
```
(by decide : [1, 0, 1] <+~ [5, 0, 1, 3, 1]).idxInj 1 = 1
```
 -/
List.Subperm.idxInj : {α : Type u_1} → [inst : BEq α] → [ReflBEq α] → {xs ys : List α} → xs.Subperm ys → Fin xs.length → Fin ys.length
-- Init.Data.Option.Lemmas
Option.any_eq_true_iff_get : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.any p x = true ↔ ∃ (h : x.isSome = true), p (x.get h) = true
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.conjTranspose_mul_self_eq_zero : ∀ {m : Type u_1} {R : Type u_4} [inst : Fintype m] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {n : Type u_5} {A : Matrix m n R},
  A.conjTranspose * A = 0 ↔ A = 0
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If the derivative of `f` is positive at a root `x₀` of `f`, then locally the sign of `f x`
matches `x - x₀`.  -/
eventually_nhdsWithin_sign_eq_of_deriv_pos : ∀ {f : ℝ → ℝ} {x₀ : ℝ}, deriv f x₀ > 0 → f x₀ = 0 → ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x - x₀)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_iff_nonpos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α] {a b : α},
  a + b ≤ b ↔ a ≤ 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated differential within a set `s` at a point `x` is not modified if one intersects
`s` with a neighborhood of `x` within `s`.  -/
iteratedFDerivWithin_inter' : ∀ {𝕜 : 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 u : Set E}
  {f : E → F} {x : E} {n : ℕ},
  u ∈ nhdsWithin x s → iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_hom : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (l : List M) {F : Type u_8}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N] (f : F), (List.map (⇑f) l).prod = f l.prod
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_one_right_iff : ∀ (n : ℕ), n.Coprime 1 ↔ True
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVlt : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vlt ValuativeRel.vlt ValuativeRel.vlt
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.smul_mem : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {x : E} {r : R} (C : PointedCone R E), 0 ≤ r → x ∈ C → r • x ∈ C
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerLeft.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ),
  CategoryTheory.Join.mapIsoWhiskerLeft H α =
    CategoryTheory.Join.mkNatIso
      (CategoryTheory.Join.mapPairLeft H Fᵣ ≪≫
        CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Iso.refl H) (CategoryTheory.Join.inclLeft E E') ≪≫
          (CategoryTheory.Join.mapPairLeft H Gᵣ).symm)
      (CategoryTheory.Join.mapPairRight H Fᵣ ≪≫
        CategoryTheory.Functor.isoWhiskerRight α (CategoryTheory.Join.inclRight E E') ≪≫
          (CategoryTheory.Join.mapPairRight H Gᵣ).symm)
      ⋯
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_subsingleton : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton R],
  Module.rank R M = 1
-- Init.Data.SInt.Lemmas
Int8.eq_sub_iff_add_eq : ∀ {a b c : Int8}, a = c - b ↔ a + b = c
-- Mathlib.FieldTheory.IsSepClosed
/-- Every separable polynomial splits in the field extension `f : k →+* K` if `k` is
separably closed.

See also `IsSepClosed.splits_codomain` for the case where `k` is separably closed.
 -/
IsSepClosed.splits_domain : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [IsSepClosed k] {f : k →+* K} (p : Polynomial k),
  p.Separable → (Polynomial.map f p).Splits
-- Mathlib.Algebra.Notation.Defs
/-- `a +ᵥ b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+ᵥ` in identifiers is `vadd`. -/
HVAdd.hVAdd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HVAdd α β γ] → α → β → γ
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + t/n) ^ n` as `n → ∞` is `exp t` for `t : ℝ`.  -/
Real.tendsto_one_add_div_pow_exp : ∀ (t : ℝ), Filter.Tendsto (fun n => (1 + t / ↑n) ^ n) Filter.atTop (nhds (Real.exp t))
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
/-- Summand in the sum to be bounded (`ℕ` version).  -/
HurwitzKernelBounds.f_nat : ℕ → ℝ → ℝ → ℕ → ℝ
-- Mathlib.Topology.Germ
Filter.Germ.value_smul : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {α : Type u_4} {β : Type u_5} [inst_1 : SMul α β]
  (φ : (nhds x).Germ α) (ψ : (nhds x).Germ β), (φ • ψ).value = φ.value • ψ.value
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.instIsTriangularizableSubtypeMemLieSubalgebra : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [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]
  (L' : LieSubalgebra R L) [LieModule.IsTriangularizable R L M], LieModule.IsTriangularizable R (↥L') M
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The finset of those partitions in which each part is used at most once.  -/
Nat.Partition.distincts : (n : ℕ) → Finset n.Partition
-- Mathlib.Algebra.Group.Units.Defs
Units.mk.injEq : ∀ {α : Type u} [inst : Monoid α] (val inv : α) (val_inv : val * inv = 1) (inv_val : inv * val = 1) (val_1 inv_1 : α)
  (val_inv_1 : val_1 * inv_1 = 1) (inv_val_1 : inv_1 * val_1 = 1),
  ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
      { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 }) =
    (val = val_1 ∧ inv = inv_1)
-- Mathlib.CategoryTheory.Category.Preorder
Monotone.functor.congr_simp : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] {f f_1 : X → Y} (e_f : f = f_1) (h : Monotone f),
  h.functor = ⋯.functor
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_eq_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] (v : n → α)
  (M : Matrix m n α), M.mulVec v = ∑ i, MulOpposite.op (v i) • M.transpose i
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_mul_inv_iff_mul_eq₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → (a = b * c⁻¹ ↔ a * c = b)
-- Init.Data.UInt.Lemmas
UInt64.le_iff_lt_or_eq : ∀ {a b : UInt64}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_pos : ∀ (n p : ℕ), 0 < p ^ n.factorization p
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_dvd_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime z y → x ∣ y → IsRelPrime z x
-- Init.Data.Option.Lemmas
Option.le_filter : ∀ {α : Type u_1} [inst : LE α],
  (∀ (x : α), x ≤ x) → ∀ {o : Option α} {p : α → Bool}, o ≤ Option.filter p o ↔ Option.all p o = true
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.instFaithfulObjPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Faithful], (CategoryTheory.Over.post F).Faithful
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_le_conductor_mem_conductorSet : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (hd : d ∈ χ.conductorSet),
  χ.conductor ≤ (Classical.choose ⋯).conductor
-- Batteries.Recycling.RBTree.Basic
/-- The red-black balance invariant. `Balanced t c n` says that the color of the root node is `c`,
and the black-height (the number of black nodes on any path from the root) of the tree is `n`.
Additionally, every red node must have black children.
 -/
RBTree.RBNode.Balanced : {α : Type u_1} → RBTree.RBNode α → RBTree.RBColor → ℕ → Prop
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {𝒢 : Subgroup (GL (Fin 2) K)}
  [𝒢.HasDetPlusMinusOne] {g : GL (Fin 2) K},
  g ∈ 𝒢 →
    ↑g 1 0 = 0 →
      (g.IsParabolic ↔
        (∃ x, x ≠ 0 ∧ g = Matrix.GeneralLinearGroup.upperRightHom x) ∨
          ∃ x, x ≠ 0 ∧ g = -Matrix.GeneralLinearGroup.upperRightHom x)