mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.Map.instFinite : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : Std.Iterator α m β]
  {lift : ⦃α : Type w⦄ → m α → n α} {f : β → Std.Iterators.PostconditionT n γ} [Std.Iterators.Finite α m],
  Std.Iterators.Finite (Std.Iterators.Types.Map α m n lift f) n
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_le_mk_iff_ratCast : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] {x y : R},
  ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ∃ q, 0 < q ∧ ↑q * |y| ≤ |x|
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.modular_T_smul : ∀ (z : UpperHalfPlane), ModularGroup.T • z = 1 +ᵥ z
-- Mathlib.Tactic.GrindAttrs
/-- The `compactness` attribute is a custom grind-set specialized to prove that sets are compact.
It is called by the `compactness` tactic.  -/
Lean.Parser.Attr.compactness : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_eq_span_right_iff_dvd : ∀ {α : Type u} [inst : CommSemiring α] {x y : α}, Ideal.span {x, y} = Ideal.span {y} ↔ y ∣ x
-- Lean.Data.Json.Parser
Lean.Json.Parser.nat : Std.Internal.Parsec.String.Parser ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isSome_apply_of_containsKey_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ}
  {l : List ((_ : α) × β)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  (h :
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      true),
  (f (Std.Internal.List.getKey k l ⋯) (Std.Internal.List.getValue k l ⋯)).isSome = true
-- Mathlib.Analysis.Normed.Group.Basic
nndist_one_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), nndist 1 a = ‖a‖₊
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_lt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} {C : ℝ}, 0 < C → (dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem** for an annulus. If `f : ℂ → E` is continuous on the closed annulus
`r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`, and is complex differentiable at all but countably many points of
its interior, then the integrals of `f` over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are equal
to each other.  -/
Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r R : ℝ},
  0 < r →
    r ≤ R →
      ∀ {f : ℂ → E} {s : Set ℂ},
        s.Countable →
          ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
            (∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
              ∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(c, r), f z
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_zmodeq' : ∀ (b b' : ℤ) (k : ℕ), b ≡ b' [ZMOD ↑k] → ∀ (L : List ℕ), Nat.ofDigits b L ≡ Nat.ofDigits b' L [ZMOD ↑k]
-- Mathlib.Order.Filter.Lift
Filter.lift_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Set α → Set β → Filter γ},
  (f.lift fun s => g.lift (h s)) = g.lift fun t => f.lift fun s => h s t
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.shrinkFunctorHomEquiv_symm_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (t : { x // x.Compatible }) (X_1 : Cᵒᵖ),
  (CategoryTheory.Presieve.shrinkFunctorHomEquiv.symm t).app X_1 =
    TypeCat.ofHom fun f => ↑t (CategoryTheory.shrinkYonedaObjObjEquiv ↑f) ⋯
-- ProofWidgets.Component.Basic
/-- Present a structured Lean message.  -/
ProofWidgets.InteractiveMessage : ProofWidgets.Component ProofWidgets.InteractiveMessageProps
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts.0.CategoryTheory.Limits.Fan.combPairHoms.match_1.splitter : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    (motive : ι₁ ⊕ ι₂ → Sort u_3) →
      (x : ι₁ ⊕ ι₂) → ((a : ι₁) → motive (Sum.inl a)) → ((a : ι₂) → motive (Sum.inr a)) → motive x
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C}
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  [A.IsVerdierLeftLocalizing B] {X Y : C} (s : X ⟶ Y),
  A Y → B.trW s → ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp a s = s'
-- Mathlib.Algebra.Lie.Subalgebra
instInhabitedLieSubalgebra : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Inhabited (LieSubalgebra R L)
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_sub : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommGroup β] [inst_4 : Module R α]
  [inst_5 : Module S β] (f g : α →ₛₗ[σᵣₛ] β), (f - g).mapMatrix = f.mapMatrix - g.mapMatrix
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_eq_of_le`. -/
Eq.trans_le : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a = b → b ≤ c → a ≤ c
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.mul.inj : ∀ {J : Type v} {inst : CategoryTheory.Category.{u, v} J} {F : CategoryTheory.Functor J MonCat}
  {a a_1 a_2 a_3 : MonCat.Colimits.Prequotient F}, a.mul a_1 = a_2.mul a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- Construct an element of the polynomial module `M[[]]` from its coefficients `ℕ →₀ M`.  -/
PolynomialModule.ofCoeff : (R : Type u_1) →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (ℕ →₀ M) → PolynomialModule R M
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_le_iff : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : AddSubmonoid M}
  {t : AddSubmonoid N} {u : AddSubmonoid (M × N)},
  s.prod t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedDef.default : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.comm : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (self : F.Hom G) (n a a' : A)
  (ha' : n + a = a'),
  CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (self.hom a) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (self.hom a') (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.Hom.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C) (i j : M.ι),
  CategoryTheory.Mat_.Hom.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C],
  CategoryTheory.IsPushout f g h i → ∀ [CategoryTheory.Mono f], CategoryTheory.IsPullback f g h i
-- Init.Data.UInt.BasicAux
Fin.Internal.ofNat.congr_simp : ∀ (n : ℕ) (hn : 0 < n) (a a_1 : ℕ), a = a_1 → Fin.Internal.ofNat n hn a = Fin.Internal.ofNat n hn a_1
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_bot : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrder ι] [inst_5 : OrderBot ι]
  [inst_6 : WellFoundedLT ι] (f : ι → E), InnerProductSpace.gramSchmidt 𝕜 f ⊥ = f ⊥
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_impl_5 : Array (Lean.Name × Lean.Name) → Array Lean.EnvExtensionEntry
-- Init.Data.Array.Lemmas
Array.isEmpty_empty : ∀ {α : Type u_1}, #[].isEmpty = true
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Converting an augmented cosimplicial object to an augmented simplicial
object and back is isomorphic to the given object.  -/
CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) → X.leftOp.rightOp ≅ X
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.map_pt : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ'),
  f.f default = default
-- Init.Data.String.Lemmas.Basic
String.Slice.copy_eq_copy_slice : ∀ {s : String.Slice} {pos₁ pos₂ : s.Pos} {h : pos₁ ≤ pos₂},
  s.copy = (s.sliceTo pos₁).copy ++ (s.slice pos₁ pos₂ h).copy ++ (s.sliceFrom pos₂).copy
-- Std.Data.DTreeMap.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.DTreeMap.any : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ((a : α) → β a → Bool) → Bool
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates.0.Tactic.ComputeAsymptotics.UnitMonomial.sign.match_1.eq_2 : ∀ (motive : Tactic.ComputeAsymptotics.UnitMonomial → Sort u_1) (hd : ℝ) (tl : List ℝ) (h_1 : Unit → motive [])
  (h_2 : (hd : ℝ) → (tl : List ℝ) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_inl : ∀ {𝕜 : 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] {s : Set M} {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q : M}, HasMFDerivAt[s] Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.Model.positionsFrom.eq_def : ∀ {s : String.Slice} (p : s.Pos),
  String.Slice.Model.positionsFrom p =
    if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Slice.Model.positionsFrom (p.next h)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- The obvious element in `d.Extension val₀ ⊥`.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension.zero : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        (d : F.WellOrderInductionData) → [inst_2 : OrderBot J] → (val₀ : F.obj (Opposite.op ⊥)) → d.Extension val₀ ⊥
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ioo_zero : ∀ {a : ℝ}, 0 < a → Real.log '' Set.Ioo 0 a = Set.Iio (Real.log a)
-- Mathlib.Algebra.GroupWithZero.Defs
IsRightCancelMulZero.mk : ∀ {M₀ : Type u} [inst : Mul M₀] [inst_1 : Zero M₀], (∀ {a : M₀}, a ≠ 0 → IsRightRegular a) → IsRightCancelMulZero M₀
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- The multicospan associated to a cover `S : J.Cover X` and a presheaf of the form `P ⋙ F`
is isomorphic to the composition of the multicospan associated to `S` and `P`,
composed with `F`.  -/
CategoryTheory.GrothendieckTopology.Cover.multicospanComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            {J : CategoryTheory.GrothendieckTopology C} →
              (F : CategoryTheory.Functor A B) →
                (P : CategoryTheory.Functor Cᵒᵖ A) →
                  {X : C} → (S : J.Cover X) → (S.index (P.comp F)).multicospan ≅ (S.index P).multicospan.comp F
-- Std.Http.Server
Std.Http.Server.mk.injEq : ∀ (context : Std.CancellationContext) (activeConnections : Std.Mutex ℕ) (connectionLimit : Option Std.Semaphore)
  (shutdownPromise : Std.Channel Unit) (config : Std.Http.Config) (localAddr : Option Std.Net.SocketAddress)
  (context_1 : Std.CancellationContext) (activeConnections_1 : Std.Mutex ℕ) (connectionLimit_1 : Option Std.Semaphore)
  (shutdownPromise_1 : Std.Channel Unit) (config_1 : Std.Http.Config) (localAddr_1 : Option Std.Net.SocketAddress),
  ({ context := context, activeConnections := activeConnections, connectionLimit := connectionLimit,
        shutdownPromise := shutdownPromise, config := config, localAddr := localAddr } =
      { context := context_1, activeConnections := activeConnections_1, connectionLimit := connectionLimit_1,
        shutdownPromise := shutdownPromise_1, config := config_1, localAddr := localAddr_1 }) =
    (context = context_1 ∧
      activeConnections = activeConnections_1 ∧
        connectionLimit = connectionLimit_1 ∧
          shutdownPromise = shutdownPromise_1 ∧ config = config_1 ∧ localAddr = localAddr_1)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_lt_inv : ∀ {a b : ENNReal}, a⁻¹ < b⁻¹ ↔ b < a
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A trivial cofibration is a morphism that is both a cofibration and a weak equivalence.  -/
HomotopicalAlgebra.trivialCofibrations : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] →
      [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → CategoryTheory.MorphismProperty C
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between two vectors is 0 if and only if the angle is 0 or π.  -/
InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  Real.sin (InnerProductGeometry.angle x y) = 0 ↔
    InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.token.injEq : ∀ (val val_1 : Lean.Parser.Token),
  (Lean.Parser.ParserExtension.OLeanEntry.token val = Lean.Parser.ParserExtension.OLeanEntry.token val_1) =
    (val = val_1)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.coe_id : ∀ (X : UniformSpaceCat), ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.BlockMem.instBoundedOrder.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X),
  AddAction.BlockMem.instBoundedOrder G a = { top := ⟨Set.univ, ⋯⟩, le_top := ⋯, bot := ⟨{a}, ⋯⟩, bot_le := ⋯ }
-- Mathlib.Order.Filter.ENNReal
ENNReal.eventually_le_limsup : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : α → ENNReal), ∀ᶠ (y : α) in f, u y ≤ Filter.limsup u f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.fromOpcyclesNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.fromOpcyclesNatTrans C).app S = S.fromOpcycles
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_pos_of_exists : ∀ {G : Type u} [inst : AddMonoid G] (n : ℕ), 0 < n → (∀ (g : G), n • g = 0) → 0 < AddMonoid.exponent G
-- Plausible.Testable
Plausible.And.printableProp : {x y : Prop} → [Plausible.PrintableProp x] → [Plausible.PrintableProp y] → Plausible.PrintableProp (x ∧ y)
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
/-- The tautological fully faithful functor `Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C)`.  -/
CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
          (CategoryTheory.Functor J (CategoryTheory.Idempotents.Karoubi C))
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : LocallyCompactSpace X]
  [inst_6 : LocallyCompactSpace Y], AbstractMeasure.prodMk = AbstractMeasure.prodMk
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 004W](https://stacks.math.columbia.edu/tag/004W) ((1)) -/
isIrreducible_iff_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible (closure s) ↔ IsIrreducible s
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree : (A : Type u_1) → SetLike (↥(Descriptive.tree A)) (List A)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A version of `cellFrontier_subset_base_union_finite_closedCell` using open cells:
The boundary of a cell is contained in a finite union of open cells of a lower dimension.  -/
Topology.RelCWComplex.cellFrontier_subset_finite_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.openCell m j
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instCategory : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → CategoryTheory.Category.{max u_1 v, max (max u_1 u) v} (HomologicalComplex V c)
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
measurable_IocProdIoc : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : (i : ι) → MeasurableSpace (X i)] {a b c : ι}, Measurable (IocProdIoc a b c)
-- Lean.Environment
Lean.Kernel.Exception.other.inj : ∀ {msg msg_1 : String}, Lean.Kernel.Exception.other msg = Lean.Kernel.Exception.other msg_1 → msg = msg_1
-- Mathlib.Topology.Category.FinTopCat
/-- The forgetful functor from finite types to topological spaces, forgetting discreteness.
This is a scoped instance.  -/
FintypeCatDiscrete.instHasForget₂FintypeCatFunObjFiniteTopCatContinuousMapCarrier : CategoryTheory.HasForget₂ FintypeCat TopCat
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofFin : ∀ {n : Fin UInt16.size}, (UInt16.ofFin n).toUSize = USize.ofNatLT ↑n ⋯
-- Mathlib.Order.Sublattice
Sublattice.coe_bot : ∀ {α : Type u_2} [inst : Lattice α], ↑⊥ = ∅
-- Mathlib.Topology.UniformSpace.Defs
nhdsWithin_eq_comap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} (S : Set α),
  nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (Set.univ ×ˢ S))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, Std.DTreeMap.Internal.Impl.contains a t = false → t.getKeyD a fallback = fallback
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.tail.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (n : ℕ), WittVector.tail n = WittVector.select fun i => n ≤ i
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Directed.le_ciSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → ∀ (i : ι), f i ≤ ⨆ j, f j
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Uniqueness of the lift.
Given a compatible family of linear maps `f n : M →ₗ[R] N ⧸ (I ^ n • ⊤)`.
If `F : M →ₗ[R] N` makes the following diagram commute
```
  N
  | \
 F|  \ f n
  |   \
  v    v
  M --> M ⧸ (I ^ n • ⊤)
```
Then it is the map `IsAdicComplete.lift`.
 -/
IsAdicComplete.eq_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m)
  {F : M →ₗ[R] N}, (∀ (n : ℕ), (I ^ n • ⊤).mkQ ∘ₗ F = f n) → F = IsAdicComplete.lift I f ⋯
-- Std.Http.Protocol.H1.Config
/-- Maximum number of bytes consumed while parsing request/status start-lines (default: 8192 bytes).
 -/
Std.Http.Protocol.H1.Config.maxStartLineLength : Std.Http.Protocol.H1.Config → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f (t.get? k)).isSome else t.contains k'
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.pairwise_disjoint_fundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  Pairwise (Function.onFun Disjoint fun g => g • MeasureTheory.fundamentalInterior G s)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_update : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M),
  (f.update a b).coeff = f.coeff.update a b
-- Init.Data.Int.Order
Int.neg_of_neg_pos : ∀ {a : ℤ}, 0 < -a → a < 0
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Apply the linear equivalence `f` to the basis vectors.  -/
Module.Basis.map : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      {M' : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid M'] →
                [inst_4 : Module R M'] → Module.Basis ι R M → (M ≃ₗ[R] M') → Module.Basis ι R M'
-- Batteries.Data.Vector.Lemmas
Vector.getElem_tail : ∀ {α : Type u_1} {n : ℕ} {v : Vector α n} {i : ℕ} (hi : i < n - 1), v.tail[i] = v[i + 1]
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk_of_inv_mul : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (x : G ⊕ H),
  Monoid.Coprod.mk (FreeMonoid.of (Sum.map Inv.inv Inv.inv x)) * Monoid.Coprod.mk (FreeMonoid.of x) = 1