mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_sub : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p x y : 𝕜), ↑(x - y) = ↑x - ↑y
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- unit morphism  -/
CategoryTheory.Functor.CoreMonoidal.εIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              F.CoreMonoidal →
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α}, t.isEmpty = true → a ∉ t
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ),
  (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Set G` and `H : Subgroup G` are complements with `1 ∈ R`, and if
`G` is generated by `S : Set G`, then `H` is generated by the `Set`
  `(R * S).image (fun g ↦ g * (hR.toRightFun g)⁻¹)`.  -/
Subgroup.closure_mul_image_eq_top : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R),
  1 ∈ R → Subgroup.closure S = ⊤ → Subgroup.closure ((fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)) = ⊤
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is uniformly equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `β → α` satisfying the right
continuity conditions. See also `Set.UniformEquicontinuous.closure` for a more familiar statement.
 -/
UniformEquicontinuous.closure' : ∀ {Y : Type u_5} {α : Type u_6} {β : Type u_8} [tY : TopologicalSpace Y] [uα : UniformSpace α] [uβ : UniformSpace β]
  {A : Set Y} {u : Y → β → α},
  UniformEquicontinuous (u ∘ Subtype.val) → Continuous u → UniformEquicontinuous (u ∘ Subtype.val)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y) {Z : H}
  (φ :
    (CategoryTheory.CostructuredArrow.proj L Y).comp F ⟶
      (CategoryTheory.Functor.const (CategoryTheory.CostructuredArrow L Y)).obj Z)
  (g : CategoryTheory.CostructuredArrow L Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map g.hom)
        ((CategoryTheory.Limits.IsColimit.homEquiv h).symm φ)) =
    φ.app g
-- Init.Data.BitVec.Lemmas
BitVec.mul_zero : ∀ {w : ℕ} {x : BitVec w}, x * 0#w = 0#w
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_apply : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (Γ :
    (CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
      (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ)),
  CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax Γ =
    CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax Γ
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.hasPointwiseLeftKanExtension_of_preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasPointwiseLeftKanExtension F] [G.PreservesPointwiseLeftKanExtension F L],
  L.HasPointwiseLeftKanExtension (F.comp G)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_add_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : α → ε},
  MeasureTheory.Integrable f (μ + ν) ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable f ν
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_exp_comp_nhds_zero : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  Filter.Tendsto (fun x => Real.exp (f x)) l (nhds 0) ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.instContainsIdentities : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} [P.ContainsIdentities],
  (CategoryTheory.MorphismProperty.sourceLocalClosure K P).ContainsIdentities
-- Batteries.Data.BitVec.Lemmas
Fin.succ.eq_1 : ∀ {n : ℕ} (i : ℕ) (h : i < n), ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Given natural numbers `m` and `n` and corresponding natural literals `em` and `en`,
returns `(s, ⊢ Finset.Icc m n = s)`.

This cannot be easily merged with `evalFinsetIccInt` since they require different
handling of numerals for `ℕ` and `ℤ`.  -/
Mathlib.Tactic.Simp.evalFinsetIccNat : ℕ → ℕ → (em en : Q(ℕ)) → Lean.MetaM ((s : Q(Finset ℕ)) × Q(Finset.Icc «$em» «$en» = «$s»))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_tan_pi_div_two : Filter.Tendsto Real.tan (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) Filter.atTop
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instNoSuffixPatternModelChar : ∀ {c : Char}, String.Slice.Pattern.Model.NoSuffixPatternModel c
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_id : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D]
  [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  {x x' : D} (f : x ⟶ x') (y : D),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id y) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f y
-- Mathlib.Computability.PartrecCode
/-- The $S_n^m$ theorem: There is a computable function, namely `Nat.Partrec.Code.curry`, that takes a
program and a ℕ `n`, and returns a new program using `n` as the first argument.
 -/
Nat.Partrec.Code.smn : ∃ f, Computable₂ f ∧ ∀ (c : Nat.Partrec.Code) (n x : ℕ), (f c n).eval x = c.eval (Nat.pair n x)
-- Lean.Util.SCC
Lean.SCC.Data.mk.sizeOf_spec : ∀ (index? lowlink? : Option ℕ) (onStack : Bool),
  sizeOf { index? := index?, lowlink? := lowlink?, onStack := onStack } =
    1 + sizeOf index? + sizeOf lowlink? + sizeOf onStack
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens)
  (hUV : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  CategoryTheory.CategoryStruct.comp V.toSpecΓ
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V hUV)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V hUV) U.toSpecΓ
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `lt_of_tsub_lt_tsub_right` for a stronger statement in a linear order.  -/
lt_of_tsub_lt_tsub_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, c ≤ b → a - c < b - c → a < b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_add_cases : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R), x + y ≤ᵥ x ∨ x + y ≤ᵥ y
-- Mathlib.Analysis.Complex.Convex
Complex.Rectangle.eq_1 : ∀ (z w : ℂ), z.Rectangle w = Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im
-- Mathlib.Geometry.Manifold.Notation
/-- `HasMFDerivAt[s] f x f'` elaborates to `HasMFDerivWithinAt I J f s x f'`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termHasMFDerivAt[_]______» : Lean.ParserDescr
-- Lean.Elab.Term.TermElabM
/-- Saved context for postponed terms and tactics to be executed.  -/
Lean.Elab.Term.SavedContext : Type
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.isClosedMap_coe : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {H : AddSubgroup G},
  IsCompact ↑H → IsClosedMap QuotientAddGroup.mk
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- A base angle of an isosceles triangle with apex at the center of a circle is acute.  -/
EuclideanGeometry.Sphere.abs_oangle_center_left_toReal_lt_pi_div_two : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → |(EuclideanGeometry.oangle s.center p₂ p₁).toReal| < Real.pi / 2
-- Lean.Elab.Binders
/-- Given syntax of the forms
  a) (`:` term)?
  b) `:` term
return `term` if it is present, or a hole if not.  -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandBinderType : Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get? (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.get? m₂ k
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr : ∀ (i w : ℕ) (e e' : BitVec w), e' = e → e'.getLsbD i = e.getLsbD i
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt32 = OfNat.ofNat n
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.mk.inj : ∀ {line : Std.Format} {column : ℕ} {tags : List (ℕ × Std.Format)} {line_1 : Std.Format} {column_1 : ℕ}
  {tags_1 : List (ℕ × Std.Format)},
  { line := line, column := column, tags := tags } = { line := line_1, column := column_1, tags := tags_1 } →
    line = line_1 ∧ column = column_1 ∧ tags = tags_1
-- ImportGraph.Imports.RequiredModules
/-- Computes all the modules transitively required by the specified modules.
Should be equivalent to calling `transitivelyRequiredModules` on each module, but shares more of the work.
 -/
Lean.Environment.transitivelyRequiredModules' : Lean.Environment → List Lean.Name → optParam Bool false → Lean.CoreM (Lean.NameMap Lean.NameSet)
-- Mathlib.Data.Fintype.Order
Finite.map_iSup_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β},
  Antitone g → g (⨆ i, f i) = ⨅ i, g (f i)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.hasBreakContinueReturn : Lean.Elab.Term.Do.Code → Bool
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- Compressing a family doesn't change its size.  -/
UV.card_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  [inst_3 : DecidableEq α] (u v : α) (s : Finset α), (UV.compression u v s).card = s.card
-- Mathlib.Algebra.Ring.Equiv
/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft` as a `RingEquiv`.  -/
RingEquiv.piCongrLeft : {ι : Type u_7} →
  {ι' : Type u_8} →
    (S : ι' → Type u_9) →
      (e : ι ≃ ι') → [inst : (i : ι') → NonUnitalNonAssocSemiring (S i)] → ((i : ι) → S (e i)) ≃+* ((i : ι') → S i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instFieldOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Field (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → Field (DirectLimit G f)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.union : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt f f' t x → HasDerivWithinAt f f' (s ∪ t) x
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fun_sum : ∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : Fintype ι] {E : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] {X : ι → Ω → E},
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P → ProbabilityTheory.HasGaussianLaw (fun ω => ∑ i, X i ω) P
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [FiniteDimensional k ↥L₁], FiniteDimensional k ↥(L₁ ⊓ L₂)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- **Alias** of the reverse direction of `contDiffWithinAt_insert`. -/
ContDiffWithinAt.insert' : ∀ {𝕜 : 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 ℕ∞} {y : E}, ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n f (insert y s) x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getPenalty : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.PhaseName → Aesop.Frontend.RuleConfig → m ℤ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.clm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F →L[𝕜] G} {g : E → F},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => (f x) (g x)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff : ∀ {A : Type u_1} {B : Type u_2} [inst : Semiring A] [inst_1 : Field B] [IsAlgClosed B] (f : A →+* B) {p : Polynomial A},
  IsUnit p.leadingCoeff → (Polynomial.map f p).roots.card = p.natDegree
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeAddMonoid α),
  FreeAddMonoid.toList ((FreeAddMonoid.map f) xs) = List.map f (FreeAddMonoid.toList xs)
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.get?_terminates : ∀ {α : Type u} (s : Stream'.WSeq α) [h : s.Productive] (n : ℕ), (s.get? n).Terminates
-- Mathlib.Algebra.Torsor.Basic
/-- Cancellation subtracting the results of two subtractions.  -/
vsub_sub_vsub_cancel_left : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (p₁ p₂ p₃ : P),
  p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
-- Mathlib.Topology.Algebra.Module.Basic
/-- Constructs a bundled linear map from a function and a proof that this function belongs to the
closure of the set of linear maps.  -/
linearMapOfMemClosureRangeCoe : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    {R : Type u_4} →
      {S : Type u_5} →
        [inst : TopologicalSpace M₂] →
          [T2Space M₂] →
            [inst_2 : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M₁] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M₁] →
                      [inst_7 : Module S M₂] →
                        [ContinuousConstSMul S M₂] →
                          [ContinuousAdd M₂] →
                            {σ : R →+* S} → (f : M₁ → M₂) → f ∈ closure (Set.range DFunLike.coe) → M₁ →ₛₗ[σ] M₂
-- Mathlib.Data.Sign.Defs
SignType.zero_eq_zero : SignType.zero = 0
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.one_fromRows_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n] (A : Matrix m n R),
  (Matrix.fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.eraseKey k l)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y),
  AlgebraicGeometry.AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 => AlgebraicGeometry.IsAffine X) f ↔
    ∀ (U V : X.Opens),
      AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → AlgebraicGeometry.IsAffineOpen (U ⊓ V)
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Conditional summation over `ℕ` is given by limits of sums over `Finset.range n` as `n → ∞`.  -/
SummationFilter.conditional_filter_eq_map_range : (SummationFilter.conditional ℕ).filter = Filter.map Finset.range Filter.atTop
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → ℚ),
      Monotone seq →
        Filter.Tendsto seq Filter.atTop Filter.atTop →
          ∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun m => f (a, c) (seq m)) Filter.atTop (nhds 1)
-- Mathlib.Algebra.GCDMonoid.Basic
Irreducible.isUnit_gcd_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {x y : α},
  Irreducible x → (IsUnit (gcd x y) ↔ ¬x ∣ y)
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.smul_modByMonic : ∀ {R : Type u} [inst : CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R), c • p %ₘ q = c • (p %ₘ q)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] (f : P.Hom P'), f.toAlgHom = MvPolynomial.aeval f.val
-- Mathlib.Probability.Moments.ComplexMGF
/-- If two random variables have the same moment-generating function then they have
the same `integrableExpSet`.  -/
ProbabilityTheory.integrableExpSet_eq_of_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ],
  ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' →
    ProbabilityTheory.integrableExpSet X μ = ProbabilityTheory.integrableExpSet Y μ'
-- Init.Prelude
/-- Retrieves the current value of the monad's mutable state.
 -/
MonadStateOf.get : {σ : semiOutParam (Type u)} → {m : Type u → Type v} → [self : MonadStateOf σ m] → m σ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The congruence relation used to localize a `CommMonoid` at a submonoid can be expressed
equivalently as an infimum (see `Localization.r`) or explicitly
(see `Localization.r'`).  -/
Localization.r_eq_r' : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M), Localization.r S = Localization.r' S
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.isLocallyInjective_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) [inst_4 : J.HasSheafCompose (CategoryTheory.forget D)]
  [CategoryTheory.Sheaf.IsLocallyInjective φ],
  CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.sheafCompose J (CategoryTheory.forget D)).map φ)
-- Mathlib.Data.Stream.Defs
/-- Tail of a stream: `Stream'.tail (h :: t) = t`.  -/
Stream'.tail : {α : Type u} → Stream' α → Stream' α
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.integral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ},
  ProbabilityTheory.IsCondKernelCDF f κ ν →
    ∀ (a : α) (x : ℝ), ∫ (b : β), ↑(f (a, b)) x ∂ν a = (κ a).real (Set.univ ×ˢ Set.Iic x)
-- Mathlib.FieldTheory.SeparableClosure
Field.insepDegree_self : ∀ (F : Type u) [inst : Field F], Field.insepDegree F F = 1
-- Init.Data.Array.Erase
Array.erase_append_left : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {xs : Array α} (ys : Array α),
  a ∈ xs → (xs ++ ys).erase a = xs.erase a ++ ys
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_ground_inter : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk (M.E ∩ X) = M.eRk X
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.mk : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          Std.IterM m β → Std.Iterators.Types.ULiftIterator α m n β lift