mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `C < f'`, then
`f` grows faster than `C * x` on `D`, i.e., `C * (y - x) < f y - f x` whenever `x, y ∈ D`,
`x < y`.  -/
Convex.mul_sub_lt_image_sub_of_lt_deriv : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, C < deriv f x) → ∀ x ∈ D, ∀ y ∈ D, x < y → C * (y - x) < f y - f x
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X) {Z : H}
  (h : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L X).comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom)
        (CategoryTheory.CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).hom h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f) h
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rci α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Logic.Basic
imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- The left uniformity on a topological group (as opposed to the right uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformGroup` structure. Two important special cases where they _do_ coincide are for
commutative groups (see `isUniformGroup_of_commGroup`) and for compact groups (see
`IsUniformGroup.of_compactSpace`).  -/
IsTopologicalGroup.leftUniformSpace : (G : Type u_1) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → UniformSpace G
-- Mathlib.Probability.Independence.Conditional
/-- A family of sets is conditionally independent if the family of measurable space structures they
generate is conditionally independent. For a set `s`, the generated measurable space has measurable
sets `∅, s, sᶜ, univ`.
See `ProbabilityTheory.iCondIndepSet_iff`.  -/
ProbabilityTheory.iCondIndepSet : {Ω : Type u_1} →
  {ι : Type u_2} →
    (m' : MeasurableSpace Ω) →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          m' ≤ mΩ →
            (ι → Set Ω) →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iCondIndepSet._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.Analysis.Real.Sqrt
Real.one_lt_sqrt_two : 1 < √2
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.andProjections.go : Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Algebra.Order.Kleene
/-- Construct an idempotent semiring from an idempotent addition.  -/
IdemSemiring.ofSemiring : {α : Type u_1} → [inst : Semiring α] → (∀ (a : α), a + a = a) → IdemSemiring α
-- Mathlib.Tactic.Says
/-- If this option is `true`, verify for `X says Y` that `X says` outputs `Y`.  -/
Mathlib.Tactic.Says.says.verify : Lean.Option Bool
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_assoc_rev : ∀ {R : Type u_1} [sR : CommSemiring R] (a b c : R), a + (b + c) = a + b + c
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)} {unit : CategoryTheory.Functor.id C ⟶ F.comp G}
  {counit : G.comp F ⟶ CategoryTheory.Functor.id D}
  {homEquiv_unit :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam}
  {homEquiv_counit :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam}
  {homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)} {unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G}
  {counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D}
  {homEquiv_unit_1 :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv_1 X Y) f = CategoryTheory.CategoryStruct.comp (unit_1.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam}
  {homEquiv_counit_1 :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv_1 X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit_1.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam},
  { homEquiv := homEquiv, unit := unit, counit := counit, homEquiv_unit := homEquiv_unit,
        homEquiv_counit := homEquiv_counit } =
      { homEquiv := homEquiv_1, unit := unit_1, counit := counit_1, homEquiv_unit := homEquiv_unit_1,
        homEquiv_counit := homEquiv_counit_1 } →
    homEquiv = homEquiv_1 ∧ unit = unit_1 ∧ counit = counit_1
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left,
namely `a₁ ≤ a₂ → a₁ • b ≤ a₂ • b` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
SMulPosMono : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero β] → Prop
-- Init.Core
Std.instCommutativeAnd : Std.Commutative And
-- Lean.Elab.Term.TermElabM
/-- See `containsPostponedTerm`  -/
Lean.Elab.Term.ContainsPendingMVar.visit : Lean.Expr → Lean.Elab.Term.ContainsPendingMVar.M Unit
-- Mathlib.RingTheory.Norm.Basic
IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots : ∀ {K : Type u_4} {L : Type u_5} {F : Type u_6} [inst : Field K] [inst_1 : Field L] [inst_2 : Field F]
  [inst_3 : Algebra K L] [inst_4 : Algebra K F] (x : L),
  (Polynomial.map (algebraMap K F) (minpoly K x)).Splits →
    (algebraMap K F) ((Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.type₁_index : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d),
  (hx.type₁ hd).index = SSet.prodStdSimplex.pairingCore.min x hd
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.subgroup`.

---

Subgroups of torsion groups are torsion groups.  -/
IsTorsion.subgroup : ∀ {G : Type u_1} [inst : Group G], IsMulTorsion G → ∀ (H : Subgroup G), IsMulTorsion ↥H
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The multiplicative kernel of a `MonoidHom` is the `Submonoid` of elements `x : G` such that
`f x = 1`.  -/
MonoidHom.mker : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : MonoidHomClass F M N] → F → Submonoid M
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.instIsCancelAddOfIsLeftCancelAdd : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [IsLeftCancelAdd R], IsCancelAdd (MvPolynomial σ R)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f →
    MeasureTheory.Integrable g μ →
      ∀ (v : E),
        Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0))
          (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.equivMatrix.congr_simp : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n], TwoSidedIdeal.equivMatrix = TwoSidedIdeal.equivMatrix
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of the forward direction of `linearIndependent_iff_injective_fintypeLinearCombination`. -/
LinearIndependent.fintypeLinearCombination_injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι],
  LinearIndependent R v → Function.Injective ⇑(Fintype.linearCombination R v)
-- Lean.SubExpr
Lean.SubExpr.Pos.fromString? : String → Except String Lean.SubExpr.Pos
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_mem_Icc : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n m : ι}, n ≤ m → ∀ (ω : Ω), MeasureTheory.hittingBtwn u s n m ω ∈ Set.Icc n m
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piRing.eq_1 : ∀ (R : Type u) (M : Type v) (ι : Type x) [inst : Semiring R] (S : Type u_4) [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : SMulCommClass R S M],
  LinearEquiv.piRing R M ι S =
    (LinearMap.lsum R (fun x => R) S).symm ≪≫ₗ LinearEquiv.piCongrRight fun x => LinearMap.ringLmapEquivSelf R S M
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.inv.congr_simp : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G],
  Homeomorph.inv G = Homeomorph.inv G
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.isRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos → String.Slice.Pattern.Model.IsRevMatch pat pos
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the groups.  -/
Subgroup.pi_le_iff : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [inst_1 : DecidableEq η] [Finite η]
  {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)},
  Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The prime case of the **Erdős–Ginzburg–Ziv theorem** for `ℤ`.

Any sequence of `2 * p - 1` elements of `ℤ` contains a subsequence of `p` elements whose sum is
divisible by `p`.  -/
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.Int.erdos_ginzburg_ziv_prime : ∀ {ι : Type u_1} {p : ℕ} [Fact (Nat.Prime p)] {s : Finset ι} (a : ι → ℤ),
  s.card = 2 * p - 1 → ∃ t ⊆ s, t.card = p ∧ ↑p ∣ ∑ i ∈ t, a i
-- Lean.Meta.Tactic.Grind.Types
/-- Returns expressions in the given expression equivalence class.  -/
Lean.Meta.Grind.getEqc : Lean.Expr → optParam Bool false → Lean.Meta.Grind.GoalM (List Lean.Expr)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂)
  (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
  self.map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp (self.map f g') (self.map f' g)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects limits, then `F : Cᵒᵖ ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The unit for the equivalence `CommMon (C ⥤ D) ≌ C ⥤ CommMon D`.
 -/
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [inst_3 : CategoryTheory.BraidedCategory D] →
            CategoryTheory.Functor.id (CategoryTheory.CommMon (CategoryTheory.Functor C D)) ≅
              CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.comp
                CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
-- Std.Http.Data.Version
Std.Http.instReprVersion : Repr Std.Http.Version
-- Mathlib.GroupTheory.CosetCover
/-- B. H. Neumann Lemma :
If a finite family of cosets of subgroups covers the group, then at least one
of these subgroups has index not exceeding the number of cosets.  -/
Subgroup.exists_index_le_card_of_leftCoset_cover : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ → ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
-- Plausible.Testable
/-- Shrink a counter-example `x` by using `Shrinkable.shrink x`, picking the first
candidate that falsifies a property and recursively shrinking that one.
The process is guaranteed to terminate because `shrink x` produces
a proof that all the values it produces are smaller (according to `SizeOf`)
than `x`.  -/
Plausible.Testable.minimizeAux : {α : Sort u_1} →
  [inst : Plausible.SampleableExt α] →
    {β : α → Prop} →
      [(x : α) → Plausible.Testable (β x)] →
        Plausible.Configuration →
          String →
            Plausible.SampleableExt.proxy α →
              ℕ →
                OptionT Plausible.Gen
                  ((x : Plausible.SampleableExt.proxy α) × Plausible.TestResult (β (Plausible.SampleableExt.interp x)))
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.condExp_sub_nonneg : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E]
  {f : ι → Ω → E}, MeasureTheory.Submartingale f ℱ μ → ∀ {i j : ι}, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]
-- Mathlib.Data.Ordmap.Ordset
/-- O(log n). Does the set contain the element `x`? That is,
is there an element that is equivalent to `x` in the order?  -/
Ordset.mem : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → α → Ordset α → Bool
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_contains : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.ExtTreeSet α cmp},
  (∀ (k : α), t₁.contains k = t₂.contains k) → t₁ = t₂
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.CommSq.cube_lemma_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M000 M001 M010 M011 M100 M101 M110 M111 : C}
  (f00x : M000 ⟶ M001) (f01x : M010 ⟶ M011) (f10x : M100 ⟶ M101) (f11x : M110 ⟶ M111) (f0x0 : M000 ⟶ M010)
  (f0x1 : M001 ⟶ M011) (f1x0 : M100 ⟶ M110) (f1x1 : M101 ⟶ M111) (fx00 : M000 ⟶ M100) (fx01 : M001 ⟶ M101)
  (fx10 : M010 ⟶ M110) (fx11 : M011 ⟶ M111),
  CategoryTheory.CommSq f0x0 f00x f01x f0x1 →
    CategoryTheory.CommSq f1x0 f10x f11x f1x1 →
      CategoryTheory.CommSq fx00 f00x f10x fx01 →
        CategoryTheory.CommSq fx10 f01x f11x fx11 →
          CategoryTheory.CommSq f0x0 fx00 fx10 f1x0 →
            ∀ [CategoryTheory.Epi f00x], CategoryTheory.CommSq f0x1 fx01 fx11 f1x1
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.lift_injective : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [inst_2 : CommRing P] (g : (i : ι) → G i →+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) [Nonempty ι] [IsDirectedOrder ι],
  (∀ (i : ι), Function.Injective ⇑(g i)) → Function.Injective ⇑(Ring.DirectLimit.lift G f P g Hg)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If distinct points `p₁` and `p₂` lie in `s` but `p₃` does not, the three points are affinely
independent.  -/
affineIndependent_of_ne_of_mem_of_mem_of_notMem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
  p₁ ≠ p₂ → p₁ ∈ s → p₂ ∈ s → p₃ ∉ s → AffineIndependent k ![p₁, p₂, p₃]
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_map_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) (X_1 : CategoryTheory.Functor J₂ C)
  {X_2 Y : J₁} (f : X_2 ⟶ Y) (X_3 : J₂),
  ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).obj X_1).map f).app X_3 =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.map f) (X_1.obj X_3)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_eq_exp : ∀ {x y : ℝ}, Circle.exp x = Circle.exp y ↔ ∃ m, x = y + ↑m * (2 * Real.pi)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- The `ObjectProperty C` corresponding to the notion of projective objects in `C`.  -/
CategoryTheory.isProjective : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.ideal_isPrincipal : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup]
  (I : Ideal ↥v.valuationSubring), Submodule.IsPrincipal I
-- Mathlib.Order.BoundedOrder.Basic
Prod.instOrderTop : (α : Type u) → (β : Type v) → [inst : LE α] → [inst_1 : LE β] → [OrderTop α] → [OrderTop β] → OrderTop (α × β)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₁' : a ⟶ b} {r₁' : b ⟶ a}
  (adj₁' : CategoryTheory.Bicategory.Adjunction l₁' r₁') {l₂ : b ⟶ c} {r₂ : c ⟶ b}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (φ : l₁' ⟶ l₁),
  (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂))
      (CategoryTheory.Bicategory.whiskerRight φ l₂) =
    CategoryTheory.Bicategory.whiskerLeft r₂ ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₁') φ)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_3.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.node RBTree.RBColor.red a y b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_2 a y b
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_eq_refl_iff : ∀ {α : Sort u_1} [inst : DecidableEq α] {x y : α}, Equiv.swap x y = Equiv.refl α ↔ x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofHasPushout_ι : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)],
  (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁ f₂).ι =
    CategoryTheory.Limits.pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_right_eq_Ico_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert b (Finset.Ico a b) = Finset.Ico a (Order.succ b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.inv_mul_le_one`. -/
Units.le_of_inv_mul_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, ↑u⁻¹ * a ≤ 1 → a ≤ ↑u
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.grpObjMkPullbackSnd_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [inst_2 : CategoryTheory.GrpObj (CategoryTheory.Over.mk f)],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback g))
      ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.one)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_sup_toInt_eq_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j k : Fin n),
  max (Mathlib.Tactic.Order.ToInt.toInt val i) (Mathlib.Tactic.Order.ToInt.toInt val j) =
      Mathlib.Tactic.Order.ToInt.toInt val k ↔
    max (val i) (val j) = val k
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.nil : {m : Type u → Type u} → {α : Type u} → MLList.MLListImpl✝ m α
-- Mathlib.Condensed.Functors
instFullCondensedTypeCondensedSetUlift : Condensed.ulift.Full
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.splits_charpoly : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  A.IsHermitian → A.charpoly.Splits
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_injective : ∀ {R : Type u}, Function.Injective Tropical.untrop
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instPosMulStrictMono : PosMulStrictMono Ordinal.{u_4}