mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_pos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPreorder R]
  [Lean.Grind.OrderedRing R] {a b : R}, 0 < a → 0 < b → 0 < a * b
-- Mathlib.RingTheory.Morita.Matrix
/-- `ModuleCat.toMatrixModCat R ι` and `MatrixModCat.toModuleCat R i` together form
an equivalence of categories.  -/
ModuleCat.matrixEquivalence : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] → [inst_1 : Fintype ι] → [inst_2 : DecidableEq ι] → ι → (ModuleCat R ≌ ModuleCat (Matrix ι ι R))
-- Init.Core
false_of_ne : ∀ {α : Sort u} {a : α}, a ≠ a → False
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
instZeroLieRinehartSubalgebra : (A : Type u_1) →
  (L : Type u_2) → [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → Zero (LieRinehartSubalgebra A L)
-- Mathlib.Logic.Encodable.Basic
Encodable.encodeSubtype.eq_1 : ∀ {α : Type u_1} {P : α → Prop} [encA : Encodable α] (v : α) (property : P v),
  Encodable.encodeSubtype ⟨v, property⟩ = Encodable.encode v
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivAt_iff_tendsto : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (nhds x) (nhds 0)
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor is said to reflect filtered colimits, if it reflects all colimits of shape `J`, where
`J` is a filtered category which is small relative to the universe in which morphisms of the source
live.
 -/
CategoryTheory.Limits.ReflectsFilteredColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofSetSetoid_parts : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Setoid α) (x : Finset α) [inst_1 : DecidableRel ⇑s],
  (Finpartition.ofSetSetoid s x).parts = Finset.image (fun a => {b ∈ x | s a b}) x
-- Mathlib.CategoryTheory.GradedObject
/-- The total object of a graded object is the coproduct of the graded components.
 -/
CategoryTheory.GradedObject.total : (β : Type) →
  (C : Type u) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [CategoryTheory.Limits.HasCoproducts C] → CategoryTheory.Functor (CategoryTheory.GradedObject β C) C
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The canonical morphism from the colimit of `E ⋙ F` to the colimit of `F`.
 -/
CategoryTheory.Limits.colimit.pre : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            (F : CategoryTheory.Functor J C) →
              [inst_3 : CategoryTheory.Limits.HasColimit F] →
                (E : CategoryTheory.Functor K J) →
                  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] →
                    CategoryTheory.Limits.colimit (E.comp F) ⟶ CategoryTheory.Limits.colimit F
-- Mathlib.Order.Minimal
IsGreatest.maximal : ∀ {α : Type u_2} {x : α} {s : Set α} [inst : Preorder α], IsGreatest s x → Maximal (fun x => x ∈ s) x
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsCofibrantPOfIsVeryGood : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [inst_5 : CategoryTheory.Limits.HasBinaryProduct A A]
  [inst_6 : CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.IsCofibrant A] [P.IsVeryGood],
  HomotopicalAlgebra.IsCofibrant P.P
-- Mathlib.Algebra.Group.Commute.Basic
Commute.function_commute_mul_left : ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, Commute a b → Function.Commute (fun x => a * x) fun x => b * x
-- Batteries.Data.MLList.Basic
/-- Embed a non-monadic thunk as a lazy list.  -/
MLList.thunk : {m : Type u_1 → Type u_1} → {α : Type u_1} → (Unit → MLList m α) → MLList m α
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_lt_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R),
  vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete`.

---

For filtrations indexed by a discrete order, `StronglyAdapted` and `IsStronglyProgressive` are
equivalent. This lemma provides `StronglyAdapted f u → IsStronglyProgressive f u`.
See `IsStronglyProgressive.stronglyAdapted` for the reverse direction, which is true more generally.
 -/
MeasureTheory.StronglyAdapted.progMeasurable_of_discrete : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι] [DiscreteTopology ι]
  [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.mono_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsSeparating →
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Mono f ↔
        ∀ (G : C),
          P G →
            ∀ (g₁ g₂ : G ⟶ X),
              CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → g₁ = g₂
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 31 → (Int32.ofNat n).toNatClampNeg = n
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.TreeMap.Raw.minEntry! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α × β
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonnegg.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (a a_1 : ℕ) (h_1 : (a b : ℕ) → motive (Int.ofNat a) (Int.ofNat b))
  (h_2 : (a b : ℕ) → motive (Int.ofNat a) (Int.negSucc b)) (h_3 : (a b : ℕ) → motive (Int.negSucc a) (Int.ofNat b))
  (h_4 : (a a_2 : ℕ) → motive (Int.negSucc a) (Int.negSucc a_2)),
  (match Int.negSucc a, Int.negSucc a_1 with
    | Int.ofNat a, Int.ofNat b => h_1 a b
    | Int.ofNat a, Int.negSucc b => h_2 a b
    | Int.negSucc a, Int.ofNat b => h_3 a b
    | Int.negSucc a, Int.negSucc a_2 => h_4 a a_2) =
    h_4 a a_1
-- Mathlib.FieldTheory.Galois.Basic
/-- Let $E / F$ be a finite extension of fields. If $|\text{Aut}(E/F)| = [E : F]$, then
$E$ is Galois over $F$.  -/
IsGalois.of_card_aut_eq_finrank : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  Nat.card Gal(E/F) = Module.finrank F E → IsGalois F E
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_C_mul : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : T} (p : Polynomial T),
  a ≠ 0 → (Polynomial.C a * p).aroots S = p.aroots S
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.eq_2 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (x_2 : 0 ≤ n), Array.ofFn.go✝ f acc 0 x_2 = acc
-- Mathlib.Order.Hom.Bounded
BotHom.dual_id : ∀ {α : Type u_2} [inst : LE α] [inst_1 : OrderBot α], BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.natCoe_apply : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {f : ArithmeticFunction ℕ} {x : ℕ}, ↑f x = ↑(f x)
-- Mathlib.Logic.Equiv.Embedding
/-- Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings,
in which the second embedding cannot take values in the range of the first.  -/
Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) } ≃ (f : α ↪ γ) × (β ↪ ↑(Set.range ⇑f)ᶜ)
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_add_right_lt : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LT α] [DenselyOrdered α] [AddLeftStrictMono α] {a b c : α},
  a + b < c → ∃ b' > b, a + b' < c
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.response.inj : ∀ {β : Type} {x x_1 : Except IO.Error (Std.Http.Response β)},
  Std.Http.Server.Connection.Recv.response✝ x = Std.Http.Server.Connection.Recv.response✝ x_1 → x = x_1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_inv_hom'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f.inv) (CategoryTheory.CategoryStruct.comp (F.map f.hom) h) = h
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A Smith normal form basis for a submodule `N` of a module `M` consists of
bases for `M` and `N` such that the inclusion map `N → M` can be written as a
(rectangular) matrix with `a` along the diagonal: in Smith normal form.  -/
Module.Basis.SmithNormalForm : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → Type u_4 → ℕ → Type (max (max u_2 u_3) u_4)
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsFunctor_hom_ext : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A : Rep.{w, u, v} k G} {M : ModuleCat k}
  {f g : (Rep.coinvariantsFunctor k G).obj A ⟶ M},
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) f =
      CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) g →
    f = g
-- Mathlib.Condensed.Light.Instances
LightProfinite.instWEqualsLocallyBijectiveCoherentTopology : ∀ (A : Type u') [inst : CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A]
  [CategoryTheory.Limits.HasColimits A] {FA : A → A → Type v} {CA : A → Type u}
  [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_4 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms],
  (CategoryTheory.coherentTopology LightProfinite).WEqualsLocallyBijective A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeInv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)),
  H.mapConeInv c = (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).inverse.obj c
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_eq_iSup : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : ENorm ε],
  (∀ (a : α), μ {a} ≠ 0) → ∀ (f : α → ε), MeasureTheory.eLpNormEssSup f μ = ⨆ a, ‖f a‖ₑ
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_add_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E), Metric.ball 0 δ + s = Metric.thickening δ s
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Composing two partial equivs, by restricting to the maximal domain where their composition
is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ f` for this.
 -/
Manifold.«term_≫_» : Lean.TrailingParserDescr
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.aemeasurable_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {u v : ℝ},
  u ≠ v →
    MeasureTheory.Integrable (fun ω => Real.exp (u * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (v * X ω)) μ → AEMeasurable X μ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Functor.mapSquare_map_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (F.mapSquare.map φ).τ₄ = F.map φ.τ₄
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂)[k]? = none
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_symm3 : ∀ {a b : EReal}, ContinuousAt (fun p => p.1 * p.2) (a, b) → ContinuousAt (fun p => p.1 * p.2) (-a, -b)
-- Mathlib.Order.RelClasses
Std.Antisymm.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Antisymm r], Std.Antisymm (Function.swap r)
-- Mathlib.NumberTheory.FLT.Three
/-- To prove `FermatLastTheoremFor 3`, it is enough to prove `FermatLastTheoremForThreeGen`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThree_of_FermatLastTheoremThreeGen : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K], FermatLastTheoremForThreeGen✝ hζ → FermatLastTheoremFor 3
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.piScalarRight_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {ι : Type u_4}
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : A) (y : ι → R),
  (Algebra.TensorProduct.piScalarRight R S A ι) (x ⊗ₜ[R] y) = fun i => y i • x
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_iff_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l → (⟨k, v⟩ ∈ l ↔ Std.Internal.List.getValue? k l = some v)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom)
        (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.ChosenPullbacksAlong.fst S.hom T.hom)
-- Mathlib.GroupTheory.Index
AddSubgroup.nsmul_mem_of_index_ne_zero_of_dvd : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.index ≠ 0 → ∀ (a : G) {n : ℕ}, (∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) → n • a ∈ H
-- Mathlib.Computability.EpsilonNFA
/-- `M.toεNFA` is an `εNFA` constructed from an `NFA` `M` by using the same start and accept
states and transition functions.  -/
NFA.toεNFA : {α : Type u} → {σ : Type v} → NFA α σ → εNFA α σ
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_sup : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (S T : Submodule R E), ↑(S ⊔ T) = ↑S ⊔ ↑T
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₂ : ∀ {l : List UInt8} {b : ByteArray} (hl : l.length = 2),
  ByteArray.utf8DecodeChar?.parseFirstByte l[0] = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
    (l.toByteArray ++ b).utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₂ l[0] l[1]
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.OptionT.bind.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.ne_bot : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCircuit → G ≠ ⊥
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given `data : OneHypercoverDenseData F J₀ J X` and a morphism `f : F.obj X₀ ⟶ X`,
this is the sieve of `X₀` consisting of morphisms `g : Y₀ ⟶ X₀` such that there
exists `i₀ : data.I₀`, `q : F.obj Y₀ ⟶ F.obj (data.X i₀)` such that
we have a factorization `q ≫ data.f i₀ = F.map g ≫ f`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.sieve : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {X : C} → F.OneHypercoverDenseData J₀ J X → {X₀ : C₀} → (F.obj X₀ ⟶ X) → CategoryTheory.Sieve X₀
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.mk.injEq : ∀ (message? since? message?_1 since?_1 : Option String),
  ({ message? := message?, since? := since? } = { message? := message?_1, since? := since?_1 }) =
    (message? = message?_1 ∧ since? = since?_1)
-- Mathlib.Data.SetLike.Basic
/-- For terms that match the `CoeSort` instance's body, pretty print as `↥S`
rather than as `{ x // x ∈ S }`. The discriminating feature is that membership
uses the `SetLike.instMembership` instance.  -/
SetLike.delabSubtypeSetLike : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
  (a : α), CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) = e a
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α]
  (s : Associates.FactorSet α), s.prod.factors = s
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b`  -/
LocallyFiniteOrder.finset_mem_Ioc : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrder α] (a b x : α),
  x ∈ LocallyFiniteOrder.finsetIoc a b ↔ a < x ∧ x ≤ b
-- Mathlib.Algebra.Field.Defs
Semifield.toDivisionSemiring : {K : Type u_2} → [self : Semifield K] → DivisionSemiring K
-- Mathlib.MeasureTheory.Function.L2Space
/-- The inner product in `L2` of indicators of two sets with finite measure
is the measure of the intersection.  -/
MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one : ∀ {α : Type u_1} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}
  (hs : MeasurableSet s) (ht : MeasurableSet t)
  (hμs : autoParam (μ s ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one._auto_1)
  (hμt : autoParam (μ t ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one._auto_3),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs 1) (MeasureTheory.indicatorConstLp 2 ht hμt 1) = ↑(μ.real (s ∩ t))
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- **Alias** of `Valuation.IsEquiv.uniformContinuous_congr`. -/
Valuation.IsEquiv.uniformContinuous_equivWithVal : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'},
  v.IsEquiv w → UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_3 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x l : ℕ) (_R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.rel _R ts) =
    FirstOrder.Language.BoundedFormula.rel (fr l _R) fun i => ft x (ts i)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given right homology map data for morphisms `φ` and `φ'`, this is the induced
right homology map data for `φ + φ'`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ φ' : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} →
              CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂ →
                  CategoryTheory.ShortComplex.RightHomologyMapData (φ + φ') h₁ h₂
-- Mathlib.Order.Fin.Basic
Fin.succAboveOrderEmb_toEmbedding : ∀ {n : ℕ} (p : Fin (n + 1)), p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Block
/-- `M` is lower triangular: entries above the diagonal vanish.  -/
Matrix.IsLowerTriangular : {m : Type u_3} → {R : Type v} → [Zero R] → [LT m] → Matrix m m R → Prop
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A weaker version of `tendsto_nhds_unique` for `PseudoMetricSpace`.  -/
tendsto_nhds_unique_dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {l : Filter β} {x y : α} [l.NeBot],
  Filter.Tendsto f l (nhds x) → Filter.Tendsto f l (nhds y) → dist x y = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffAt.curry_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'},
  ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y) → ContMDiffAt I' J n (fun y => f x y) y