mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.subset_lieSpan : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M}, s ⊆ ↑(LieSubmodule.lieSpan R L s)
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- **Alias** of `ContDiffAt.eventually_apply_implicitFunction`.

---

`implicitFunction` is indeed the (local) implicit function defined by `f`.  -/
IsContDiffImplicitAt.apply_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (x : E₁) in nhds u.1, f (x, cdf.implicitFunction pn if₂ x) = f u
-- Init.Data.Int.Lemmas
Int.subNatNat_elim : ∀ (m n : ℕ) (motive : ℕ → ℕ → ℤ → Prop),
  (∀ (i n : ℕ), motive (n + i) n ↑i) →
    (∀ (i m : ℕ), motive m (m + i + 1) (Int.negSucc i)) → motive m n (Int.subNatNat m n)
-- Mathlib.Algebra.Ring.Parity
Odd.neg : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd a → Odd (-a)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.fromIdeal_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Surjective ⇑(KaehlerDifferential.fromIdeal R S)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_inj : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₂ : Type u_6} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R₁ M₂] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₂] {f f' : M₂},
  ContinuousLinearMap.toSpanSingleton R₁ f = ContinuousLinearMap.toSpanSingleton R₁ f' ↔ f = f'
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
equals the product of their L-series in their common half-plane of absolute convergence.  -/
ArithmeticFunction.LSeries_mul : ∀ {f g : ArithmeticFunction ℂ} {s : ℂ},
  (LSeries.abscissaOfAbsConv fun n => f n) < ↑s.re →
    (LSeries.abscissaOfAbsConv fun n => g n) < ↑s.re →
      LSeries (fun n => (f * g) n) s = LSeries (fun n => f n) s * LSeries (fun n => g n) s
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- If `f` is a `C^n` local diffeomorphism at `x`, for `n ≠ 0`, the differential `df_x`
is a linear equivalence.  -/
IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              IsLocalDiffeomorphAt I J n f x →
                                                n ≠ 0 → TangentSpace I x ≃L[𝕜] TangentSpace J (f x)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_linearIndepOn_id_extension : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V},
  LinearIndepOn K id s → s ⊆ t → ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndepOn K id b
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.instInhabited : (α : Type u_2) → [inst : Mul α] → [inst_1 : Add α] → [inst_2 : LE α] → Inhabited (α ≃+*o α)
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- This is the `iff` version of `Matrix.isSymm.fromBlocks`.  -/
Matrix.isSymm_fromBlocks_iff : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
  {D : Matrix n n α}, (Matrix.fromBlocks A B C D).IsSymm ↔ A.IsSymm ∧ B.transpose = C ∧ C.transpose = B ∧ D.IsSymm
-- Lean.HeadIndex
Lean.HeadIndex.sort : Lean.HeadIndex
-- Mathlib.Topology.Maps.Proper.Basic
/-- By definition, if `f` is a proper map and `ℱ` is any filter on `X`, then any cluster point of
`map f ℱ` is the image by `f` of some cluster point of `ℱ`.  -/
IsProperMap.clusterPt_of_mapClusterPt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
-- Mathlib.Geometry.Manifold.Instances.Icc
mdifferentiableWithinAt_comp_projIcc_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x y : ℝ}
  [h : Fact (x < y)] {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)},
  MDiffAt[Set.Icc x y] (f ∘ Set.projIcc x y ⋯) ↑w ↔ MDiffAt f w
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_smul_left_of_tower : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N)
  [inst_5 : CommSemiring S] [inst_6 : Algebra S R] [inst_7 : Module S M] [IsScalarTower S R M] [inst_9 : Module S N]
  [IsScalarTower S R N] (a : S) (x y : M), QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.toExistsAddOfLE : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R],
  ExistsAddOfLE R
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.SemiCartesianMonoidalCategory.snd`. -/
CategoryTheory.Functor.chosenProd.snd : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Y
-- Mathlib.NumberTheory.NumberField.DedekindZeta
NumberField.dedekindZeta_residue_pos : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 < NumberField.dedekindZeta_residue K
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cone for `J`.
In `limitOfDiagramInitial` we show it is a limit cone.  -/
CategoryTheory.Limits.coneOfDiagramInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} → CategoryTheory.Limits.IsInitial X → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cone F
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_of_isEmpty_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α] {l : ρ},
  (Std.DHashMap.Const.insertManyIfNewUnit m l).isEmpty = true → m.isEmpty = true
-- Init.Control.Lawful.Instances
EStateM.run_throw : ∀ {ε σ : Type u_1} (e : ε) (s : σ), (throw e).run s = EStateM.Result.error e s
-- Mathlib.Analysis.Convex.Body
ConvexBody.ext_iff : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] {K L : ConvexBody V},
  K = L ↔ ↑K = ↑L
-- Mathlib.Logic.Equiv.Basic
Equiv.swapCore_self : ∀ {α : Sort u_1} [inst : DecidableEq α] (r a : α), Equiv.swapCore a a r = r
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
/-- The categories of coherent sheaves and extensive sheaves on `C` are equivalent if `C` is
preregular, finitary extensive, and every object is projective.
 -/
CategoryTheory.Presheaf.coherentExtensiveEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
        [inst_2 : CategoryTheory.Preregular C] →
          [inst_3 : CategoryTheory.FinitaryExtensive C] →
            [∀ (X : C), CategoryTheory.Projective X] →
              CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌
                CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvOneClassOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : InvOneClass Mᵐᵒᵖ], DomMulAct.instInvOneClassOfMulOpposite = inst
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedState : Inhabited Lean.Elab.Tactic.State
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.centroidWeightsWithCircumcenter.eq_2 : ∀ {n : ℕ} (fs : Finset (Fin (n + 1))),
  Affine.Simplex.centroidWeightsWithCircumcenter fs Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = 0
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The preimage of an `OpenAddSubgroup` along a continuous `AddMonoid` homomorphism
is an `OpenAddSubgroup`.  -/
OpenAddSubgroup.comap : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      {N : Type u_2} →
        [inst_2 : AddGroup N] →
          [inst_3 : TopologicalSpace N] → (f : G →+ N) → Continuous ⇑f → OpenAddSubgroup N → OpenAddSubgroup G
-- Mathlib.Topology.Algebra.Field
/-- If `f, g` are functions `α → 𝕜`, both continuous on a preconnected set `S`, with
`f ^ 2 = g ^ 2` on `S`, and `g z ≠ 0` all `z ∈ S`, then either `f = g` or `f = -g` on
`S`.  -/
IsPreconnected.eq_or_eq_neg_of_sq_eq : ∀ {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace 𝕜]
  [T1Space 𝕜] [inst_3 : Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜],
  IsPreconnected S →
    ContinuousOn f S →
      ContinuousOn g S → Set.EqOn (f ^ 2) (g ^ 2) S → (∀ {x : α}, x ∈ S → g x ≠ 0) → Set.EqOn f g S ∨ Set.EqOn f (-g) S
-- Init.GrindInstances.ToInt
Lean.Grind.instLEUSizeUintNumBits : Lean.Grind.ToInt.LE USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Order.Category.FinBddDistLat
_private.Mathlib.Order.Category.FinBddDistLat.0.FinBddDistLat.Hom.mk.sizeOf_spec : ∀ {X Y : FinBddDistLat} (hom' : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Any permutation matrix is column stochastic.  -/
Matrix.permMatrix_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {σ : Equiv.Perm n},
  Equiv.Perm.permMatrix R σ ∈ Matrix.colStochastic R n
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.ext_iff : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] {f g : A →⋆ₐ[R] B},
  f = g ↔ ∀ (x : A), f x = g x
-- Init.Data.String.Defs
String.Pos.Raw.offsetBy_sliceRawEndPos_left : ∀ {p : String.Pos.Raw} {s : String.Slice}, s.rawEndPos.offsetBy p = p + s
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.isoMk_hom_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber),
  (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.fiber = e₂.hom
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching a real from within a convex set, `HasDerivWithinAt` version.
This does not require anything about the situation at `a`  -/
HasDerivWithinAt.lhopital_zero_nhdsWithin_convex : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ} {s : Set ℝ},
  Convex ℝ s →
    (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), HasDerivWithinAt f (f' x) (s \ {a}) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), HasDerivWithinAt g (g' x) (s \ {a}) x) →
        (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), g' x ≠ 0) →
          Filter.Tendsto f (nhdsWithin a (s \ {a})) (nhds 0) →
            Filter.Tendsto g (nhdsWithin a (s \ {a})) (nhds 0) →
              Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (s \ {a})) l →
                Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (s \ {a})) l
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.exists_isCompact_not_null : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.Regular],
  (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal Y)
  (c : CategoryTheory.Limits.BinaryFan X Y), Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadExceptError : MonadExcept IO.Error Std.Async.ContextAsync
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.instAdditiveObjFunctorAdditiveFunctor : ∀ (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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : C ⥤+ D), F.obj.Additive
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.range_dualMap_eq_dualAnnihilator_ker : ∀ {K : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V₁ →ₗ[K] V₂), f.dualMap.range = f.ker.dualAnnihilator
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.patterns : Array Aesop.CasesPattern → Aesop.CasesTarget
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postEquiv_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D), (CategoryTheory.Under.postEquiv X F).functor = CategoryTheory.Under.post F.functor
-- Lean.Parser.Command
/-- Adds more documentation as an extension of the documentation for a given tactic.

The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
list, so it should be brief.
 -/
Lean.Parser.Command.tactic_extension : Lean.Parser.Parser
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_map_right : ∀ {α : Type u} {β : Type v} {γ : Type w} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : β → β')
  (g : α → β' → γ), Stream'.Seq.zipWith g s₁ (Stream'.Seq.map f s₂) = Stream'.Seq.zipWith (fun a b => g a (f b)) s₁ s₂
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasStrictDerivAt.clog : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasStrictDerivAt f f' x → f x ∈ Complex.slitPlane → HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_bot : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ↑⊥ = ⊥
-- Mathlib.Data.PFun
PFun.preimage_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.preimage s = f.core s ∩ f.Dom
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.normalizedFactorsEquivSpanNormalizedFactors.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r : R} (hr : r ≠ 0),
  Ideal.normalizedFactorsEquivSpanNormalizedFactors hr = Equiv.ofBijective (fun d => ⟨Ideal.span {↑d}, ⋯⟩) ⋯
-- Mathlib.Order.Disjoint
Codisjoint.sup_right' : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α} (c : α),
  Codisjoint a b → Codisjoint a (c ⊔ b)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The inclusion functor `CofibrantObject C ⥤ C`.  -/
HomotopicalAlgebra.CofibrantObject.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] → CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) C
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.iUnion_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X), ⋃ n, K n = Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_eq_support_getElem? : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v), n ≤ p.length → some (p.getVert n) = p.support[n]?
-- Mathlib.Topology.Algebra.Group.Compact
/-- Every topological additive group
in which there exists a compact set with nonempty interior is locally compact.  -/
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  (K : TopologicalSpace.PositiveCompacts G), LocallyCompactSpace G
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_pos_iff' : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], 0 < Metric.ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  m.contains a = false → m.get? a = none
-- Mathlib.Logic.Function.Defs
Function.diag_def : ∀ {α : Type u_1}, Function.diag = fun a => (a, a)
-- Mathlib.Algebra.Ring.Pi
Pi.distrib : {I : Type u} → {f : I → Type v} → [(i : I) → Distrib (f i)] → Distrib ((i : I) → f i)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.mem_unop : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {x : R} {S : Subsemiring Rᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mk.inj : ∀ {Ω : Type u_1} {ι : Type u_2} {inst : Preorder ι} {m : MeasurableSpace Ω} {seq : ι → MeasurableSpace Ω}
  {mono' : Monotone seq} {le' : ∀ (i : ι), seq i ≤ m} {seq_1 : ι → MeasurableSpace Ω} {mono'_1 : Monotone seq_1}
  {le'_1 : ∀ (i : ι), seq_1 i ≤ m},
  { seq := seq, mono' := mono', le' := le' } = { seq := seq_1, mono' := mono'_1, le' := le'_1 } → seq = seq_1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.not_matchesAt_of_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  p (pos.get h) = false → ¬String.Slice.Pattern.Model.MatchesAt p pos
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_bot_top : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.IsComplement' ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (F : CategoryTheory.Functor X.HomotopyCategory C)
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })} (e : SSet.Truncated.Edge x y),
  (CategoryTheory.ConcreteCategory.hom
        ((SSet.Truncated.HomotopyCategory.homToNerveMk F).app
          (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })))
      e.edge =
    CategoryTheory.ComposableArrows.mk₁ (F.map (SSet.Truncated.HomotopyCategory.homMk e))
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.cons : ∀ {F : PFunctor.{uA, uB}} (xs : PFunctor.Approx.Path F) {a : F.A} (x : F.M) (f : F.B a → F.M) (i : F.B a),
  x = PFunctor.M.mk ⟨a, f⟩ → PFunctor.M.IsPath xs (f i) → PFunctor.M.IsPath (⟨a, i⟩ :: xs) x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, (Std.ExtDHashMap.Const.alter m k f).size ≤ m.size + 1
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_sub : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R ≃+* S)
  (x y : R), f (x - y) = f x - f y
-- Mathlib.Algebra.Group.Center
Set.mul_mem_center : ∀ {M : Type u_1} [inst : Mul M] {z₁ z₂ : M}, z₁ ∈ Set.center M → z₂ ∈ Set.center M → z₁ * z₂ ∈ Set.center M
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getKey? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
        Std.Internal.List.getKey? k l₁
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} {n : ℕ},
  (∀ (i : ι), Function.IsPeriodicPt (f i) n (x i)) → Function.IsPeriodicPt (Pi.map f) n x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.min?.get ⋯ = km → t.get km hc = km
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The yoneda embedding `yoneda.obj X : Cᵒᵖ ⥤ Type v` for `X : C` preserves limits.  -/
CategoryTheory.yoneda_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (CategoryTheory.yoneda.obj X)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.hom_ext_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {X : C}
  {f f' : X ⟶ CategoryTheory.Limits.limit F},
  f = f' ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π F j) =
        CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π F j)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_part_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, a ∈ P.part a ↔ a ∈ s
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.hull_min : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C : ConvexCone R M} {s : Set M}, s ⊆ ↑C → ConvexCone.hull R s ≤ C
-- Mathlib.Order.DirectedInverseSystem
/-- Extend a natural family of bijections to a limit ordinal.  -/
InverseSystem.piEquivLim : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
            {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j} →
              InverseSystem.IsNatEquiv f equiv →
                F i ≃ ↑(InverseSystem.limit f i) →
                  Order.IsSuccPrelimit i → (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.ext_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) (hobj : ∀ (X : C), F.obj X = G.obj X),
  autoParam (∀ (X : C), e.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Functor.ext_of_iso._auto_1 → F = G
-- Mathlib.Logic.Equiv.Prod
/-- `Empty` type is a right absorbing element for type product up to an equivalence.  -/
Equiv.prodEmpty : (α : Type u_9) → α × Empty ≃ Empty