mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.prepathObject_p₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  K.prepathObject.p₀ = HomologicalComplex.pathObject.π₀ K
-- Init.Data.SInt.Lemmas
Int8.toInt32_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
-- Mathlib.GroupTheory.OrderOfElement
/-- If `p • x = 0` for some odd `p`, then every multiple of `x` is an even
multiple of `x`.  -/
exists_nsmul_eq_nsmul_two_add : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {p : ℕ}, p • x = 0 → Odd p → ∀ (n : ℕ), ∃ m, n • x = (2 * m) • x
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseLocalTimeType : Std.Internal.Parsec.ByteArray.Parser Std.Time.TimeZone.TZif.LocalTimeType
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of a measurable function over `UnitAddCircle` is equal to the integral over an
interval $(t, t + 1]$ in `ℝ` of its lift to `ℝ`.  -/
UnitAddCircle.lintegral_preimage : ∀ (t : ℝ) (f : UnitAddCircle → ENNReal), ∫⁻ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫⁻ (b : UnitAddCircle), f b
-- Mathlib.Data.List.Lattice
List.cons_bagInter : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α],
  (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableEMatchDiagNode.hash : Lean.Meta.Grind.EMatchDiagNode → UInt64
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmallSubtypeEq : ∀ {α : Type v} {x : α}, Std.Internal.Small { x_1 // x = x_1 }
-- Mathlib.Algebra.Lie.Nilpotent
/-- A generalisation of the lower central series. The zeroth term is a specified Lie submodule of
a Lie module. In the case when we specify the top ideal `⊤` of the Lie algebra, regarded as a Lie
module over itself, we get the usual lower central series of a Lie algebra.

It can be more convenient to work with this generalisation when considering the lower central series
of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic
expression of the fact that the terms of the Lie submodule's lower central series are also Lie
submodules of the enclosing Lie module.

See also `LieSubmodule.lowerCentralSeries_eq_lcs_comap` and
`LieSubmodule.lowerCentralSeries_map_eq_lcs` below, as well as `LieSubmodule.ucs`.  -/
LieSubmodule.lcs : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → ℕ → LieSubmodule R L M → LieSubmodule R L M
-- Mathlib.Tactic.GCongr.Core
/-- The monad used internally in the `gcongr` tactic.  -/
Mathlib.Tactic.GCongr.GCongrM : Type → Type
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
/-- The counit functor establishing the equivalence `StructuredArrow.commaMapEquivalence`.  -/
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
                                                  (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X) ≅
                                                CategoryTheory.Functor.id
                                                  (CategoryTheory.Comma
                                                    (CategoryTheory.StructuredArrow.map₂
                                                      (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
                                                    (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.eq_const : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] [MeasurableSingletonClass β]
  {f : α → β}, Measurable f → ∀ (a : β), Measurable fun x => f x = a
-- Batteries.Control.Nondet.Basic
Nondet.mk.inj : ∀ {σ : Type} {m : Type → Type} {inst : Lean.MonadBacktrack σ m} {α : Type} {toMLList toMLList_1 : MLList m (α × σ)},
  { toMLList := toMLList } = { toMLList := toMLList_1 } → toMLList = toMLList_1
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.val_smul : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : ↥s), ↑(r • x) = r • ↑x
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} (F : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  {g : ι → E → 𝕜} {s : Finset ι},
  (∀ i ∈ s, Function.HasTemperateGrowth (g i)) →
    (SchwartzMap.fourierMultiplierCLM F fun x => ∑ i ∈ s, g i x) = ∑ i ∈ s, SchwartzMap.fourierMultiplierCLM F (g i)
-- Lean.Elab.PreDefinition.WF.PackMutual
Lean.Elab.WF.mutualName : Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Array Lean.Elab.PreDefinition → Lean.Name
-- Mathlib.Data.Quot
/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`.  -/
Quotient.hrecOn₂' : {α : Sort u_1} →
  {β : Sort u_2} →
    {s₁ : Setoid α} →
      {s₂ : Setoid β} →
        {φ : Quotient s₁ → Quotient s₂ → Sort u_5} →
          (qa : Quotient s₁) →
            (qb : Quotient s₂) →
              (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)) →
                (∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂) → φ qa qb
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- **Alias** of `Convex.locallyPathConnectedSpace`.

---

Convex subsets of locally convex spaces are locally path-connected.  -/
Convex.locPathConnectedSpace : ∀ (E : Type u_2) [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {S : Set E}, Convex ℝ S → LocallyPathConnectedSpace ↑S
-- Mathlib.CategoryTheory.Join.Final
/-- The category of `Join.inclLeft C D`-costructured arrows with target `right d` is equivalent to
`C`.  -/
CategoryTheory.Join.costructuredArrowEquiv : (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] →
        (d : D) → CategoryTheory.CostructuredArrow (CategoryTheory.Join.inclLeft C D) (CategoryTheory.Join.right d) ≌ C
-- Lean.Elab.Tactic.Try
/-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it.  -/
Lean.Elab.Tactic.Try.checkTactic : Lean.Elab.Tactic.SavedState → Lean.TSyntax `tactic → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coeFn_add : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.FiniteMeasure Ω), ⇑(μ + ν) = ⇑μ + ⇑ν
-- Mathlib.Util.PrintSorries
/-- Prints all uses of `sorry` inside a list of declarations.
Displayed sorries are hoverable and support "go to definition".
 -/
Mathlib.PrintSorries.collectSorries : Array Lean.Name → Lean.MetaM (Array Lean.MessageData)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.mk.inj : ∀ {α : Type u_2} {inst : TopologicalSpace α} {inst_1 : LE α} {toClopens : TopologicalSpace.Clopens α}
  {upper' : IsUpperSet toClopens.carrier} {toClopens_1 : TopologicalSpace.Clopens α}
  {upper'_1 : IsUpperSet toClopens_1.carrier},
  { toClopens := toClopens, upper' := upper' } = { toClopens := toClopens_1, upper' := upper'_1 } →
    toClopens = toClopens_1
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.map_ceil : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {S : Type u_3}
  [inst_3 : Semiring S] [inst_4 : LinearOrder S] [inst_5 : FloorSemiring S] {F : Type u_4} [inst_6 : FunLike F R S]
  [RingHomClass F R S] (f : F), StrictMono ⇑f → ∀ (a : R), ⌈f a⌉₊ = ⌈a⌉₊
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension_obj_obj : ∀ (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.IsIdempotentComplete D]
  (X : CategoryTheory.Functor C D) (X_1 : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.functorExtension C D).obj X).obj X_1 =
    (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.obj
      (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj X_1)
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_iterate_frobeniusEquiv_symm : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (m n : ℕ)
  (x : PreTilt O p), (PreTilt.coeff m) ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x) = (PreTilt.coeff (m + n)) x
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.SemanticTokensState.noConfusionType : Sort v✝ → Lean.Server.FileWorker.SemanticTokensState → Lean.Server.FileWorker.SemanticTokensState → Sort v✝
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_closure : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, TotallyBounded (closure s) ↔ TotallyBounded s
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.sub_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), s - Metric.closedBall x δ = -x +ᵥ Metric.cthickening δ s
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.ofMeasurableSpace_toMeasurableSpace : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α)
  (h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)),
  MeasurableSpace.DynkinSystem.ofMeasurableSpace (d.toMeasurableSpace h_inter) = d
-- Init.Data.Fin.Lemmas
Fin.val_neg : ∀ {n : ℕ} [inst : NeZero n] (x : Fin n), ↑(-x) = if x = 0 then 0 else n - ↑x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.equivOfIsometry_apply : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (a : CliffordAlgebra Q₁),
  (CliffordAlgebra.equivOfIsometry e) a = (CliffordAlgebra.map e.toIsometry) a
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_prod : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_8} {N : Type u_9} [inst_1 : AddZeroClass M] [inst_2 : AddZeroClass N]
  (f : G →+ M) (g : G →+ N), (f.prod g).ker = f.ker ⊓ g.ker
-- Lean.Expr
Lean.instHashableMVarId.hash : Lean.MVarId → UInt64
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} [inst_1 : SizeOf C]
  (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S)
  (I₁ : toPreZeroHypercover.I₀ → toPreZeroHypercover.I₀ → Type w) (Y : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → I₁ i₁ i₂ → C)
  (p₁ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₁)
  (p₂ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₂)
  (w :
    ∀ ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (p₁ j) (toPreZeroHypercover.f i₁) =
        CategoryTheory.CategoryStruct.comp (p₂ j) (toPreZeroHypercover.f i₂)),
  sizeOf { toPreZeroHypercover := toPreZeroHypercover, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } =
    1 + sizeOf toPreZeroHypercover
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_zero_addString : ∀ (s : String), (0 + s).byteIdx = s.utf8ByteSize
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_comp : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {Y : α → Ω} {mβ : MeasurableSpace β} {Ω' : Type u_5}
  {mΩ' : MeasurableSpace Ω'} [inst_4 : StandardBorelSpace Ω'] [inst_5 : Nonempty Ω'] (X : α → β),
  AEMeasurable Y μ →
    ∀ {f : Ω → Ω'},
      Measurable f →
        ⇑(ProbabilityTheory.condDistrib (f ∘ Y) X μ) =ᵐ[MeasureTheory.Measure.map X μ]
          ⇑((ProbabilityTheory.condDistrib Y X μ).map f)
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopMonObj_mul_unmop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.MonObj.mul.unmop = CategoryTheory.MonObj.mul
-- Lean.Meta.Sym.SymM
/-- Reports an issue if both `verbose` and `sym.debug` are enabled. Does nothing otherwise.  -/
Lean.Meta.Sym.reportDbgIssue : Lean.MessageData → Lean.Meta.Sym.SymM Unit
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_unitIso_hom_app_hom_apply_hom_apply : ∀ (X : Type u) (x : X) (x_1 : PUnit.{u + 1}),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.typeEquiv.unitIso.hom.app X)) x))
      x_1 =
    x
-- Std.Http.Data.Chunk
/-- Inserts a trailer header field.
 -/
Std.Http.Trailer.insert : Std.Http.Trailer → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Trailer
-- Mathlib.Topology.MetricSpace.Isometry
/-- Post-composition by an isometry does not change the Lipschitz-property of a function.  -/
Isometry.lipschitzWith_iff : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : NNReal),
  Isometry g → (LipschitzWith K (g ∘ f) ↔ LipschitzWith K f)
-- Mathlib.Topology.Algebra.Algebra
algebraMapCLM_apply : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousSMul R A] (a : R),
  (algebraMapCLM R A) a = (algebraMap R A) a
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_comp_le_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.degHom g
-- Mathlib.Topology.Algebra.Support
ContinuousOn.continuous_of_tsupport_subset : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β] {f : α → β}
  {s : Set α}, ContinuousOn f s → IsOpen s → tsupport f ⊆ s → Continuous f
-- Mathlib.Order.Filter.ENNReal
ENNReal.toReal_limsup : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal},
  (∀ᶠ (a : α) in f, u a ≠ ⊤) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => (u a).toReal) ENNReal.toReal_limsup._auto_1 →
      (Filter.limsup u f).toReal = Filter.limsup (fun a => (u a).toReal) f
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instDescScheme : ∀ {U V X : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : V ⟶ X) [AlgebraicGeometry.IsFinite f]
  [AlgebraicGeometry.IsFinite g], AlgebraicGeometry.IsFinite (CategoryTheory.Limits.coprod.desc f g)
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- `A` is in reduced row echelon form: it is in row echelon form, each leading entry is
`1`, and entries above a leading entry vanish (entries below one vanish by
`isRowEchelon`).  -/
Matrix.IsReducedRowEchelon : {m : Type u_1} → {n : Type u_2} → {R : Type v} → [Zero R] → [LT m] → [LT n] → [One R] → Matrix m n R → Prop
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_setOfPred_lt_im : ∀ (a : ℝ), closure {z | a < z.im} = {z | a ≤ z.im}
-- Init.Data.String.Subslice
String.Slice.Subslice.isEmpty_toSlice_iff : ∀ {s : String.Slice} {sl : s.Subslice}, sl.toSlice.isEmpty = true ↔ sl.startInclusive = sl.endExclusive
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.eq_one_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R], v.IsEquiv w → ∀ {x : R}, v x = 1 ↔ w x = 1
-- Mathlib.Data.List.Defs
/-- `l.Forall p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
`List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`.  -/
List.Forall : {α : Type u_1} → (α → Prop) → List α → Prop
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `b i` is the `i`th basis vector.  -/
Module.Basis.instFunLike : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → FunLike (Module.Basis ι R M) ι M
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_eq_iff_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : N ≃+ P} {x : M} {y : P},
  (f.ofAddEquivOfLocalizations k) x = y ↔ f x = k.symm y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The maximal pre-`1`-hypercover containing `E`, where the `1`-components are all relations
on `E`.  -/
CategoryTheory.PreZeroHypercover.saturate : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → CategoryTheory.PreZeroHypercover S → CategoryTheory.PreOneHypercover S
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.h : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A `CorepresentableBy` structure that characterizes maps out of `U ⊛ F`
by leveraging the fact that `U ⊠ F` is a left Kan extension of `(fromPUnit 𝟙_ V) ⊠ F`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                (F : CategoryTheory.Functor C V) →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
                          (CategoryTheory.MonoidalCategory.tensorRight v)] →
                    [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] →
                      (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                                (CategoryTheory.MonoidalCategory.tensor C)).comp
                            (((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete PUnit.{1} × C) (C × C)
                                      V).obj
                                  ((CategoryTheory.Functor.fromPUnit
                                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).prod
                                    (CategoryTheory.Functor.id C))).comp
                              (CategoryTheory.coyoneda.obj
                                (Opposite.op
                                  (CategoryTheory.MonoidalCategory.externalProduct
                                    (CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
                                    F))))).CorepresentableBy
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution U F)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_map_measure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ → (MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.monotone_l : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → Monotone l
-- Mathlib.Order.Bounds.Basic
bot_mem_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] (s : Set α), ⊥ ∈ lowerBounds s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.g_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_3 : CategoryTheory.Epi S.g] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.g (CategoryTheory.CategoryStruct.comp (hS.desc k hk) h) =
    CategoryTheory.CategoryStruct.comp k h
-- Init.Data.UInt.Lemmas
UInt32.neg_ne_zero : ∀ {a : UInt32}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_decide_mod_two_eq_one_shiftRight_one : ∀ (n : ℕ), Nat.bit (decide (n % 2 = 1)) (n >>> 1) = n
-- Mathlib.Data.Finmap
/-- The predicate `a ∈ s` means that `s` has a value associated to the key `a`.  -/
Finmap.instMembership : {α : Type u} → {β : α → Type v} → Membership α (Finmap β)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.toFinset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [inst_1 : DecidableEq β] (s : Set α) (t : Set β) [inst_2 : Fintype ↑s]
  [inst_3 : Fintype ↑t] [inst_4 : Fintype ↑(s +ᵥ t)], (s +ᵥ t).toFinset = s.toFinset +ᵥ t.toFinset
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_lt_omega : ∀ (r : ℝ), ↑r < Hyperreal.omega