mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a power series within a set on a ball, then so does its derivative. Version
assuming that the function is analytic on `s`. For a version without this assumption but requiring
that `F` is complete, see `HasFPowerSeriesWithinOnBall.fderivWithin_of_mem`.  -/
HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinOnBall f p s x r →
    AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → x ∈ s → HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.two_le_card_support_of_ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f ≠ 1 → 2 ≤ f.support.card
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivAtFilter.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {L : Filter (E × E)} {f : E → E} {f' : E →L[𝕜] E},
  HasFDerivAtFilter f f' L → Filter.Tendsto (Prod.map f f) L L → ∀ (n : ℕ), HasFDerivAtFilter f^[n] (f' ^ n) L
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_mulVec : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [inst_5 : Fintype n] {A : X → Matrix m n R}
  {B : X → n → R}, Continuous A → Continuous B → Continuous fun x => (A x).mulVec (B x)
-- Mathlib.Data.Pi.Interval
Pi.card_Ici : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)] (a : (i : ι) → α i),
  (Finset.Ici a).card = ∏ i, (Finset.Ici (a i)).card
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc) (a : α) (t acc : List α),
  x = a :: t →
    x_1 = acc →
      (match x, x_1 with
        | [], acc => h_1 acc
        | a :: t, acc => h_2 a t acc) ≍
        h_2 a t acc
-- Mathlib.Probability.Decision.Risk.Basic
/-- **Data processing inequality** for the Bayes risk with respect to a prior: taking the map of
the data generating kernel by a function increases the risk.  -/
ProbabilityTheory.bayesRisk_le_bayesRisk_map : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u_3} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓧' : MeasurableSpace 𝓧'} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧)
  (π : MeasureTheory.Measure Θ) {f : 𝓧 → 𝓧'},
  Measurable f → ProbabilityTheory.bayesRisk ℓ P π ≤ ProbabilityTheory.bayesRisk ℓ (P.map f) π
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_add : ∀ {α : Type u} [inst : Mul α] (x y : Additive α), Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive.  -/
MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive : ∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetSemiring C →
    m.IsSigmaSubadditive →
      ∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
-- Mathlib.Algebra.Opposites
MulOpposite.instInv.eq_1 : ∀ {α : Type u_1} [inst : Inv α], MulOpposite.instInv = { inv := fun x => MulOpposite.op (MulOpposite.unop x)⁻¹ }
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_bind' : ∀ {m : Type w → Type w'} [inst : Monad m] {α β : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β},
  (x >>= f).operation = do
    let a ← x.operation
    (fun fa => ⟨↑fa, ⋯⟩) <$> (f ↑a).operation
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Cache.toCache : {u : Lean.Level} →
  {A : Q(Type u)} → {sA : Q(CommSemiring «$A»)} → Mathlib.Tactic.Algebra.Cache sA → Mathlib.Tactic.Ring.Common.Cache sA
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.epiModSerre_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] (X Y : C), P.epiModSerre 0 ↔ P Y
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.toMonoidHom : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' → R →* R'
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves limits of `K.op : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesColimit_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.leftOp F.unop],
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.ext : ∀ {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β},
  H₁.vertexSet = H₂.vertexSet → H₁.edgeSet = H₂.edgeSet → H₁.Compatible H₂ → H₁ = H₂
-- Std.Data.DTreeMap.Raw.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.DTreeMap.Raw.union : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_image_Icc : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [inst_4 : IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a),
  ⇑(affineHomeomorph a b ⋯) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- In the case of a representable morphism `f' : F.obj Y ⟶ G`, whose codomain lies
in the image of `F`, we get that two morphism `a b : Z ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf'.snd g : hf.pullback  ⟶ X` are equal.
* Their compositions (in `C`) with `hf'.fst' g : hf.pullback  ⟶ Y` are equal.  -/
CategoryTheory.Functor.relativelyRepresentable.hom_ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} [inst_2 : F.Full] [F.Faithful] {c : C} {a_1 b_1 : c ⟶ hf'.pullback g},
  CategoryTheory.CategoryStruct.comp a_1 (hf'.fst' g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.fst' g) →
    CategoryTheory.CategoryStruct.comp a_1 (hf'.snd g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.snd g) → a_1 = b_1
-- Mathlib.Data.Multiset.Sum
Multiset.Nodup.disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β}, s.Nodup → t.Nodup → (s.disjSum t).Nodup
-- Mathlib.Algebra.Ring.CharZero
CharZero.eq_neg_self_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R}, a = -a ↔ a = 0
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_unitIso_inv_app_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), ((MonObj.mopEquiv C).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Init.SimpLemmas
and_self_left : ∀ {a b : Prop}, a ∧ a ∧ b ↔ a ∧ b
-- Mathlib.Algebra.Star.StarAlgHom
/-- If a monoid `R` acts on another monoid `S`, then a non-unital star algebra homomorphism
over `S` can be viewed as a non-unital star algebra homomorphism over `R`.  -/
NonUnitalStarAlgHom.restrictScalars : (R : Type u_1) →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : Monoid S] →
            [inst_2 : Star A] →
              [inst_3 : Star B] →
                [inst_4 : NonUnitalNonAssocSemiring A] →
                  [inst_5 : NonUnitalNonAssocSemiring B] →
                    [inst_6 : MulAction R S] →
                      [inst_7 : DistribMulAction S A] →
                        [inst_8 : DistribMulAction S B] →
                          [inst_9 : DistribMulAction R A] →
                            [inst_10 : DistribMulAction R B] →
                              [IsScalarTower R S A] → [IsScalarTower R S B] → (A →⋆ₙₐ[S] B) → A →⋆ₙₐ[R] B
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueEquiv_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Unique m] [inst_1 : Unique n] (M : Matrix m n A),
  Matrix.uniqueEquiv M = M default default
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances.0.«term_⁺¹» : Lean.TrailingParserDescr
-- Lean.Elab.Tactic.Monotonicity
Lean.Meta.Monotonicity.solveMono : (optParam ({α : Type} → Lean.Expr → Array Lean.Name → Lean.MetaM α) fun {α} => Lean.Meta.Monotonicity.defaultFailK) →
  Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R],
  (CategoryTheory.forget₂ (TopModuleCat R) TopCat).ReflectsIsomorphisms
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.ae_cond_mem : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  MeasurableSet s → ∀ᵐ (x : Ω) ∂μ[|s], x ∈ s
-- Mathlib.Algebra.Group.Basic
/-- Variant of `mul_eq_one_iff_inv_eq` with swapped equality.  -/
mul_eq_one_iff_inv_eq' : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b = 1 ↔ b⁻¹ = a
-- Init.Data.List.Count
List.countP_pos_iff : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, 0 < List.countP p l ↔ ∃ a ∈ l, p a = true
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- In a category with an initial object and pushouts,
a coproduct of objects `X` and `Y` is isomorphic to a pushout.  -/
coprodIsoPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] →
      [inst_2 : CategoryTheory.Limits.HasPushouts C] →
        (X Y : C) →
          [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
            X ⨿ Y ≅
              CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
_private.Mathlib.GroupTheory.FreeGroup.NielsenSchreier.0.IsFreeGroupoid.SpanningTree.homOfPath.match_1.splitter : {G : Type u_1} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] →
          (motive :
              (x : G) →
                Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x →
                  Sort u_2) →
            (x : G) →
              (x_1 :
                  Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T))
                    x) →
                (Unit →
                    motive (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T))
                      Quiver.Path.nil) →
                  ((x b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T) →
                      (p :
                          Quiver.Path
                            (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T))
                            b) →
                        (f : b ⟶ x) → motive x (p.cons f)) →
                    motive x x_1
-- Mathlib.GroupTheory.Exponent
add_notMem_of_exponent_two : ∀ {G : Type u} [inst : AddGroup G], AddMonoid.exponent G = 2 → ∀ {x y : G}, x ≠ 0 → y ≠ 0 → x ≠ y → x + y ∉ {x, y, 0}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.instHasPushoutCompInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z Z' : C} {f : Z ⟶ X} {g : Z' ⟶ Y} (i : Z' ⟶ Z)
  [inst_1 : CategoryTheory.IsIso i] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) g],
  CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv i) g)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instUnionOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Union (Std.ExtHashSet α)
-- Aesop.Index.Basic
Aesop.IndexingMode.or.injEq : ∀ (imodes imodes_1 : Array Aesop.IndexingMode),
  (Aesop.IndexingMode.or imodes = Aesop.IndexingMode.or imodes_1) = (imodes = imodes_1)
-- Mathlib.Algebra.Prime.Defs
/-- An element `p` of a commutative monoid with zero (e.g., a ring) is called *prime*,
if it's not zero, not a unit, and `p ∣ a * b → p ∣ a ∨ p ∣ b` for all `a`, `b`.  -/
Prime : {M : Type u_1} → [CommMonoidWithZero M] → M → Prop
-- Mathlib.Data.Part
Part.assert_neg : ∀ {α : Type u_1} {p : Prop} {f : p → Part α}, ¬p → Part.assert p f = Part.none
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_zero_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s : Set α},
  MeasurableSet s → (p.toMeasure s = 0 ↔ Disjoint p.support s)
-- Init.PropLemmas
/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches.  -/
ite_not : ∀ {α : Sort u_1} (p : Prop) [inst : Decidable p] (x y : α), (if ¬p then x else y) = if p then y else x
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.saveFunInd : Lean.Expr → Lean.Name → Array Lean.Expr → Lean.Meta.Try.Collector.M Unit
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.one_sub_nonneg : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] (x : ↑(Set.Icc 0 1)), 0 ≤ 1 - ↑x
-- Batteries.Data.List.Lemmas
List.mem_idxsOf_getElem : ∀ {α : Type u_1} {i : ℕ} {xs : List α} [inst : BEq α] [EquivBEq α] (h : i < xs.length), i ∈ List.idxsOf xs[i] xs
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.inr_apply : ∀ {α : Type u_1} {β : Type u_2} (val : β), Function.Embedding.inr val = Sum.inr val
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.forIn.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.forIn = 1
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.restrict_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α), (κ.restrict hs) a = (κ a).restrict s
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup'_product_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset β} {t : Finset γ}
  (h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).sup' h f = s.sup' ⋯ fun i => t.sup' ⋯ fun i' => f (i, i')
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.fstX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j),
  HomologicalComplex.homotopyCofiber.fstX φ i j hij =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij).hom
      CategoryTheory.Limits.biprod.fst
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_left_on_Ioo : ∀ {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  a < b →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
        (∀ x ∈ Set.Ioo a b, g' x ≠ 0) →
          Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds 0) →
            Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds 0) →
              Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin b (Set.Iio b)) l →
                Filter.Tendsto (fun x => f x / g x) (nhdsWithin b (Set.Iio b)) l
-- Init.Data.Rat.Lemmas
Rat.divInt_eq_divInt_iff : ∀ {d₁ d₂ n₁ n₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → (Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Function.Surjective ⇑Monoid.Coprod.fst
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.fst_notMem_right : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → w₁ ∉ t
-- Init.Data.SInt.Lemmas
Int16.sub_lt : ∀ {a b : Int16}, 0 < b → b ≤ a → a - b < a
-- Mathlib.Algebra.Group.ULift
ULift.smul.eq_1 : ∀ {α : Type u} {β : Type v} [inst : SMul β α], ULift.smul = { smul := fun n x => { down := n • x.down } }
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : D),
  iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X))
      (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))
-- Mathlib.Algebra.Torsor.Basic
Set.smul_set_sdiv_smul_set : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (v : G) (s t : Set P),
  v • s /ₛ v • t = s /ₛ t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ}
  [inst_2 : Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ) (Q : Polynomial ℤ),
  (RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp)
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (Polynomial.map (Int.castRingHom (ZMod p)) Q)) =
    (Ideal.Quotient.mk (Ideal.span {↑p})) ((Polynomial.aeval θ) Q)
-- Init.Data.List.TakeDrop
List.replace_takeWhile : ∀ {α : Type u_1} {a b : α} [inst : BEq α] [LawfulBEq α] {l : List α} {p : α → Bool},
  p a = p b → (List.takeWhile p l).replace a b = List.takeWhile p (l.replace a b)
-- Std.Data.ExtDTreeMap.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.ExtDTreeMap.contains : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Bool
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeSurjective : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.Surjective
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.hom_ext : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- Given an open subgroup `U` and an element `r` of a nonarchimedean ring, there is an open
subgroup `V` such that `r • V` is contained in `U`.  -/
NonarchimedeanRing.left_mul_subset : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) (r : R),
  ∃ V, r • ↑V ⊆ ↑U
-- Mathlib.Data.Fintype.EquivFin
_private.Mathlib.Data.Fintype.EquivFin.0.Infinite.natEmbeddingAux.eq_def : ∀ (α : Type u_4) [inst : Infinite α] (x : ℕ),
  Infinite.natEmbeddingAux✝ α x =
    let n := x;
    Classical.choose ⋯
-- Std.Internal.Do.WP.Frame
/-- Reinterpret a `WPMonad m` so its weakest precondition is the `PreservesSup.frameClosure` of the
base wp over a family of `Sup`-preserving resource operators `op r` that act by `comp` with unit `e`.
The resource frame rule then holds by construction (`WP.Frames.of_frameClosure`).  -/
Std.Internal.Do.WPMonad.of_frameClosure : {m : Type → Type} →
  [inst : Monad m] →
    {P : Type u} →
      {E : Type z} →
        [inst_1 : Std.Internal.Do.Assertion P] →
          [inst_2 : Std.Internal.Do.Assertion E] →
            {R : Type} →
              (op : R → P → P) →
                [∀ (r : R), Lean.Order.PreservesSup (op r)] →
                  {comp : R → R → R} →
                    {e : R} →
                      (∀ (r r' : R) (a : P), op (comp r r') a = op r (op r' a)) →
                        (∀ (a : P), op e a = a) → Std.Internal.Do.WPMonad m P E → Std.Internal.Do.WPMonad m P E
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.IsReduced.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N},
  (∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j) → P.IsReduced
-- Mathlib.CategoryTheory.Shift.Basic
/-- auxiliary definition for `FullyFaithful.hasShift`  -/
CategoryTheory.Functor.FullyFaithful.hasShift.add : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F : CategoryTheory.Functor C D} →
                F.FullyFaithful →
                  (s : A → CategoryTheory.Functor C C) →
                    ((i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) →
                      (a b : A) → s (a + b) ≅ (s a).comp (s b)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_eq_bot : ∀ {M : Type u_2} [inst : MulOneClass M] {S : Submonoid M}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.Algebra.Group.Hom.Instances
instIsCancelMulOneHom : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : MulOneClass N] [IsCancelMul N], IsCancelMul (OneHom M N)
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_union_eq_adjoin_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (s t : Set A),
  Algebra.adjoin R (s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)