mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
      Option.map (f k) (Std.Internal.List.getValueCast? k l)
-- Mathlib.Order.WithBot
WithBot.eq_unbot_iff : ∀ {α : Type u_1} {a : α} {b : WithBot α} (h : b ≠ ⊥), a = b.unbot h ↔ ↑a = b
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realMixedSpace K),
  HasFDerivAt (↑(NumberField.mixedEmbedding.polarCoordReal K).symm)
    (NumberField.mixedEmbedding.FDerivPolarCoordRealSymm K x) x
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.npow_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a : α) (n : ℕ) (v₁ v : ℚ),
  (v == v₁ ^ n) = true → a = Lean.Grind.Field.NormNum.ofRat v₁ → a ^ n = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.T_inv_mul_apply_one : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), ↑(ModularGroup.T⁻¹ * g) 1 = ↑g 1
-- Lean.DocString.Types
Lean.Doc.instReprInline.repr : {i : Type u_1} → [Repr i] → Lean.Doc.Inline i → ℕ → Std.Format
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LeapSecond.mk.injEq : ∀ (transitionTime correction transitionTime_1 correction_1 : ℤ),
  ({ transitionTime := transitionTime, correction := correction } =
      { transitionTime := transitionTime_1, correction := correction_1 }) =
    (transitionTime = transitionTime_1 ∧ correction = correction_1)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The left inclusion of `F` into `coprod F G`.  -/
CategoryTheory.FunctorToTypes.coprod.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → F ⟶ CategoryTheory.FunctorToTypes.coprod F G
-- Mathlib.Data.Fin.SuccPred
Fin.succ_predAbove_zero : ∀ {n : ℕ} [inst : NeZero n] {j : Fin (n + 1)}, j ≠ 0 → (Fin.predAbove 0 j).succ = j
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {fallback : α},
  (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Order.PartialSups
partialSups_eq_sup'_range : ∀ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α) (n : ℕ), (partialSups f) n = (Finset.range (n + 1)).sup' ⋯ f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey!_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_top : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  IntermediateField.lift ⊤ = K
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- Consider a set of sets `S` containing arbitrarily small neighborhoods of any point, and a
probability measure. Then any open set can be approximated arbitrarily well in measure from inside
by a finite union of elements of `S`.

This is a technical lemma for `IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem`, which is
why it is formulated for a `ProbabilityMeasure`. If needed, this could be generalized to finite
measures or to general measures.
 -/
MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [SecondCountableTopology Ω] {S : Set (Set Ω)}
  (ν : MeasureTheory.ProbabilityMeasure Ω),
  (∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ nhds x ∧ s ⊆ u) →
    ∀ {G : Set Ω}, IsOpen G → ∀ {r : NNReal}, r < ν G → ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
-- Mathlib.Order.Monotone.Defs
MonotoneOn.reflect_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → a < b
-- Mathlib.Topology.Connected.LocallyConnected
/-- The product of two locally connected spaces is locally connected.  -/
Prod.locallyConnectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [LocallyConnectedSpace α]
  [LocallyConnectedSpace β], LocallyConnectedSpace (α × β)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isAmalgamation_sieveExtend : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (t : P.obj (Opposite.op X)),
  x.IsAmalgamation t → x.sieveExtend.IsAmalgamation t
-- Mathlib.Analysis.BoundedVariation
BoundedVariationOn.smul : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α},
  BoundedVariationOn f s → BoundedVariationOn g s → BoundedVariationOn (f • g) s
-- Init.Sym.Lemmas
Lean.Sym.Char.eq_eq_true : ∀ (a b : Char), decide (a = b) = true → (a = b) = True
-- Mathlib.LinearAlgebra.Span.Basic
/-- There is no vector subspace between `s` and `K ∙ x ⊔ s`, `CovBy` version.  -/
Submodule.covBy_span_singleton_sup : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V}
  {s : Submodule K V}, x ∉ s → s ⋖ K ∙ x ⊔ s
-- Mathlib.AlgebraicTopology.SimplicialObject.II
/-- Auxiliary definition for the definition of the action of the
functor `SimplexCategory.II` on morphisms.  -/
SimplexCategory.II.map' : {n m : ℕ} → (Fin (n + 1) →o Fin (m + 1)) → Fin (m + 2) → Fin (n + 2)
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- **Alias** of `Valued.toNormedField.setOfPred_mem_integer_eq_closedBall`. -/
Valued.toNormedField.setOf_mem_integer_eq_closedBall : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], {x | x ∈ Valued.v.integer} = Metric.closedBall 0 1
-- Std.Internal.UV.UDP
_private.Std.Internal.UV.UDP.0.Std.Internal.UV.UDP.SocketImpl : NonemptyType
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.exists_bucket : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < m.size) (k : α),
  ∃ l,
    (Std.DHashMap.Internal.toListModel m).Perm ((Std.DHashMap.Internal.bucket m h k).toList ++ l) ∧
      ∀ [LawfulHashable α],
        Std.DHashMap.Internal.IsHashSelf m → ∀ (k' : α), hash k = hash k' → Std.Internal.List.containsKey k' l = false
-- Init.Omega.Constraint
Lean.Omega.Constraint.div_sat' : ∀ {c : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs},
  x.gcd ≠ 0 → c.sat (x.dot y) = true → (c.div x.gcd).sat' (x.sdiv ↑x.gcd) y = true
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_isLocalization_isMaximal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3) [inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)]
  [inst_4 : (p : Ideal R) → [inst_4 : p.IsMaximal] → Algebra R (Rₚ p)] (Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4)
  [inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)]
  [inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)]
  [inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)]
  [inst_8 : (p : Ideal R) → [inst_8 : p.IsMaximal] → Algebra R (Sₚ p)]
  [∀ (p : Ideal R) [inst_9 : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)]
  [inst_10 : ∀ (p : Ideal R) [inst_10 : p.IsMaximal], IsScalarTower R S (Sₚ p)]
  [∀ (p : Ideal R) [inst_11 : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p]
  [∀ (p : Ideal R) [inst_12 : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))],
  (∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))) →
    Function.Injective ⇑(algebraMap R S)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.load a q with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_4 (Turing.TM2.Stmt.load a q) a q ⋯
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.le_div_iff_mul_le : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I J J' : FractionalIdeal (nonZeroDivisors R₁) K},
  J' ≠ 0 → (I ≤ J / J' ↔ I * J' ≤ J)
-- Aesop.Util.Tactic
/-- A `MetaM` version of the `replace` tactic. If `fvarId` refers to the
hypothesis `h`, this tactic asserts a new hypothesis `h : type` with proof
`proof : type` and then tries to clear `fvarId`. Unlike `replaceLocalDecl`,
`replaceFVar` always adds the new hypothesis at the end of the local context.

`replaceFVar` returns the new goal, the `FVarId` of the newly asserted
hypothesis and whether the old hypothesis was cleared.
 -/
Aesop.replaceFVar : Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.Expr → Lean.MetaM (Lean.MVarId × Lean.FVarId × Bool)
-- Mathlib.Algebra.GroupWithZero.Basic
zero_zpow_eq : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (n : ℤ), 0 ^ n = if n = 0 then 1 else 0
-- Mathlib.Logic.Basic
Ne.ite_ne_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, a ≠ b → ((if P then a else b) ≠ b ↔ P)
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counit.eq_1 : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P],
  CompHausLike.LocallyConstant.counit P hs =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (CompHausLike.LocallyConstant.counitApp X.obj),
      naturality := ⋯ }
-- Init.SizeOf
Lean.Name.str.sizeOf_spec : ∀ (p : Lean.Name) (s : String), sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- Consider an additive content `m` on a semi-ring of measurable sets `C`, which is dominated
by a finite measure `μ`.
Then `m` extends to a countably additive vector measure which is dominated by `μ`.  -/
MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure : ∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)}
  {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) → (∀ s ∈ C, MeasurableSet s) → ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.induction_on_reflect : ∀ {ι : 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} {b : P.Base}
  [inst_5 : CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι},
  b.IsPos i →
    ∀ {p : ι → Prop}, (∀ i ∈ b.support, p i) → (∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)) → p i
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Given a continuous multilinear map `f` on `n` variables (parameterized by `Fin n`) and a subset
`s` of `k` of these variables, one gets a new continuous multilinear map on `Fin k` by varying
these variables, and fixing the other ones equal to a given value `z`. It is denoted by
`f.restr s hk z`, where `hk` is a proof that the cardinality of `s` is `k`. The implicit
identification between `Fin k` and `s` that we use is the canonical (increasing) bijection.  -/
ContinuousMultilinearMap.restr : {𝕜 : Type u} →
  {G : Type wG} →
    {G' : Type wG'} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : SeminormedAddCommGroup G'] →
              [inst_4 : NormedSpace 𝕜 G'] →
                {k n : ℕ} → (G [×n]→L[𝕜] G') → (s : Finset (Fin n)) → s.card = k → G → G [×k]→L[𝕜] G'
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.ord : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfLEArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    Ord α
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.one_div_ne_zero' : ∀ {p q r : ℝ}, p.HolderTriple q r → 1 / r ≠ 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_pos_of_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀],
  0 < a → 0 < a ^ 2
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_neg : ∀ {α : Type u_1} [inst : Neg α] (a : α), SymAlg.sym (-a) = -SymAlg.sym a
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Not an instance since `𝕜` can't be inferred. See `NormedSpace.toLocallyConvexSpace` for a
slightly weaker instance version.  -/
NormedSpace.toLocallyConvexSpace' : ∀ (𝕜 : Type u_2) {E : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedSpace ℝ 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : Module ℝ E] [IsScalarTower ℝ 𝕜 E], LocallyConvexSpace ℝ E
-- Mathlib.Data.Fintype.Prod
Set.toFinset_offDiag : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑s.offDiag], s.offDiag.toFinset = s.toFinset.offDiag
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instRepresentablyFlatOppositeOpOfRepresentablyCoflat : ∀ {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.RepresentablyCoflat F], CategoryTheory.RepresentablyFlat F.op
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.IsAnisotropic.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] {P : RootPairing ι R M N},
  (∀ (i : ι), (P.RootForm (P.root i)) (P.root i) ≠ 0) →
    (∀ (i : ι), (P.CorootForm (P.coroot i)) (P.coroot i) ≠ 0) → P.IsAnisotropic
-- Mathlib.Logic.Basic
not_ne_iff : ∀ {α : Sort u_1} {a b : α}, ¬a ≠ b ↔ a = b
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects (small) colimits if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
 -/
CategoryTheory.Limits.ReflectsColimits : {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.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpTrimToLpMeasSubgroup` is a left inverse of `lpMeasSubgroupToLpTrim`.  -/
MeasureTheory.lpMeasSubgroupToLpTrim_left_inv : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0),
  Function.LeftInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
-- Mathlib.Topology.Algebra.Constructions
AddUnits.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [DiscreteTopology M], DiscreteTopology (AddUnits M)
-- Mathlib.Order.GameAdd
/-- Recursion on the well-founded `Sym2.GameAdd` relation.  -/
Sym2.GameAdd.recursion : {α : Type u_1} →
  {rα : α → α → Prop} →
    {C : α → α → Sort u_3} →
      WellFounded rα →
        ((a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → (a b : α) → C a b
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.mk.injEq : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} (W : CategoryTheory.MorphismProperty J)
  (P : CategoryTheory.ObjectProperty J) (src : ∀ {i j : J} {f : i ⟶ j}, W f → P i)
  (tgt : ∀ {i j : J} {f : i ⟶ j}, W f → P j) (hW : W.HasCardinalLT κ) (hP : P.HasCardinalLT κ)
  (W_1 : CategoryTheory.MorphismProperty J) (P_1 : CategoryTheory.ObjectProperty J)
  (src_1 : ∀ {i j : J} {f : i ⟶ j}, W_1 f → P_1 i) (tgt_1 : ∀ {i j : J} {f : i ⟶ j}, W_1 f → P_1 j)
  (hW_1 : W_1.HasCardinalLT κ) (hP_1 : P_1.HasCardinalLT κ),
  ({ W := W, P := P, src := src, tgt := tgt, hW := hW, hP := hP } =
      { W := W_1, P := P_1, src := src_1, tgt := tgt_1, hW := hW_1, hP := hP_1 }) =
    (W = W_1 ∧ P = P_1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toDiv : {α : Type u_3} → [self : LinearOrderedCommGroupWithZero α] → Div α
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] [Module.Projective S Ω[S⁄R]], Module.Finite S (Algebra.H1Cotangent R S)
-- Mathlib.Algebra.CharP.Basic
/-- The characteristic of the product of rings is the least common multiple of the
characteristics of the two rings.  -/
Nat.lcm.charP : ∀ (R : Type u_1) (S : Type u_2) [inst : AddMonoidWithOne R] [inst_1 : AddMonoidWithOne S] (p q : ℕ) [CharP R p]
  [CharP S q], CharP (R × S) (p.lcm q)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.documentation? : Lean.Lsp.CompletionItem → Option Lean.Lsp.MarkupContent
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_init : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  ↑1 * Lean.Grind.CommRing.Poly.denote ctx p = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Algebra.Group.Action.Defs
/-- Associativity of `+ᵥ`  -/
VAddAssocClass.vadd_assoc : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} {inst : VAdd M N} {inst_1 : VAdd N α} {inst_2 : VAdd M α}
  [self : VAddAssocClass M N α] (x : M) (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z
-- Mathlib.RingTheory.Coprime.Lemmas
Nat.isCoprime_iff_coprime : ∀ {m n : ℕ}, IsCoprime ↑m ↑n ↔ m.Coprime n
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.of_forall_mem_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α],
  m₁.WF → m₂.WF → (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂
-- Mathlib.Order.Concept
/-- The extent consists of all elements related to all elements of the intent.  -/
Concept.lowerPolar_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r), lowerPolar r self.intent = self.extent
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instIsLeftCancelMulOfMulOpposite : ∀ {M : Type u_1} [inst : Mul Mᵐᵒᵖ] [IsLeftCancelMul Mᵐᵒᵖ], IsLeftCancelMul Mᵈᵐᵃ
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticStx.sizeOf_spec : ∀ (stx : Lean.Syntax), sizeOf (Aesop.RuleTacDescr.tacticStx stx) = 1 + sizeOf stx
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `none` if no such element exists.
 -/
Std.TreeSet.getLT? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Option α
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.inductionOn : ∀ {motive : Cardinal.{u_1} → Prop} (c : Cardinal.{u_1}), (∀ (α : Type u_1), motive (Cardinal.mk α)) → motive c
-- Mathlib.Data.EReal.Basic
EReal.top_ne_zero : ⊤ ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft_eq_zero_iff` for matrix multiplication.  -/
mulLeftLinearMap_eq_zero_iff : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : Semiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A] [Nonempty n] (a : Matrix l m A),
  mulLeftLinearMap n R a = 0 ↔ a = 0
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.closedEBall x ε ↔ edist y x ≤ ε
-- Mathlib.Algebra.Order.Floor.Ring
Int.succ.eq_1 : ∀ (a : ℤ), a.succ = a + 1
-- Init.Data.UInt.BasicAux
/-- Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
 -/
USize.lt : USize → USize → Prop
-- Mathlib.CategoryTheory.Category.Basic
/-- The category structure on `ULift C` that is induced from the category
structure on `C`. This is not made a global instance because of a diamond
when `C` is a preordered type.  -/
CategoryTheory.uliftCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, max u' u} (ULift.{u', u} C)
-- Mathlib.Data.Option.NAry
Option.map₂_none_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : Option β), Option.map₂ f none b = none
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.Raw.map f m} (h : m.WF),
  (Std.HashMap.Raw.map f m)[k] = f k m[k]
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_sub_iff_zpow_eq_zpow : ∀ {G : Type u_1} [inst : Group G] {x : G} {a b : ℤ}, ↑(orderOf x) ∣ a - b ↔ x ^ a = x ^ b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y'),
  (f.homMk' g).left = CategoryTheory.CategoryStruct.id f.left