mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of `f`, see `integrable_cfc'` for a statement
with weaker assumptions.  -/
integrable_cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : TopologicalSpace X] [OpensMeasurableSpace X]
  (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ spectrum 𝕜 a) →
    (∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
      MeasureTheory.HasFiniteIntegral bound μ →
        autoParam (p a) integrable_cfc._auto_1 → MeasureTheory.Integrable (fun x => cfc (f x) a) μ
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.high.sizeOf_spec : sizeOf Batteries.Tactic.Lint.LintVerbosity.high = 1
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instCommutativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.CommSemiring α], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Data.Nat.MaxPowDiv
Nat.padicValNat_lt_self : ∀ {p n : ℕ}, n ≠ 0 → padicValNat p n < n
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet : ∀ {z : ℂ}, z ∈ UpperHalfPlane.upperHalfPlaneSet → DifferentiableAt ℂ ModularForm.eta z
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.comp_apply : ∀ {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toDistLat),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.DocString.Types
/-- Sub-parts (e.g. subsections of a section, sections of a chapter)  -/
Lean.Doc.Part.subParts : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p → Array (Lean.Doc.Part i b p)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleMk (f - g) h =
    CochainComplex.HomComplex.Cochain.toSingleMk f h - CochainComplex.HomComplex.Cochain.toSingleMk g h
-- Lean.Elab.Tactic.Omega.Frontend
/-- Given a fact `h` with type `¬ P`, return a more useful fact obtained by pushing the negation.  -/
Lean.Elab.Tactic.Omega.MetaProblem.pushNot : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Order.LatticeIntervals
Set.Icc.coe_bot : ∀ {α : Type u_1} [inst : Preorder α] (a b : α) [inst_1 : Fact (a ≤ b)], ↑⊥ = a
-- Mathlib.Algebra.Group.Graph
/-- The graph of a group homomorphism as a subgroup.

See also `MonoidHom.mgraph` for the graph as a submonoid.  -/
MonoidHom.graph : {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → (G →* H) → Subgroup (G × H)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {Z : C} (h_1 : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.f' (CategoryTheory.CategoryStruct.comp h.i h_1) =
    CategoryTheory.CategoryStruct.comp S.f h_1
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- existence of conical limits (of size) implies existence of limits (of size)  -/
CategoryTheory.Enriched.HasConicalLimitsOfSize.hasLimitsOfSize : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u)
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  [CategoryTheory.Enriched.HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C],
  CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.swap_isSwap_iff : ∀ {α : Type u_2} [inst : DecidableEq α] {a b : α}, (Equiv.swap a b).IsSwap ↔ a ≠ b
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.precoverage.eq_1 : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.precoverage P = AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage ⊓ P.precoverage
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_sup : ∀ {V : Type u_1} (v : V) [inst : DecidableEq V] {G₁ G₂ : SimpleGraph V} [inst_1 : Fintype ↑((G₁ ⊔ G₂).neighborSet v)]
  [inst_2 : Fintype ↑(G₁.neighborSet v)] [inst_3 : Fintype ↑(G₂.neighborSet v)],
  (G₁ ⊔ G₂).neighborFinset v = G₁.neighborFinset v ∪ G₂.neighborFinset v
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.tail_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α], Matrix.vecTail 0 = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} {X Y : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.coconeRightOpOfConeEquiv.functor.map f).hom = f.unop.hom.op
-- Mathlib.Topology.Subpath
/-- For a path `γ`, `γ.subpath` gives a "continuous family of paths", by which we mean
the uncurried function which maps `(t₀, t₁, s)` to `γ.subpath t₀ t₁ s` is continuous.  -/
Path.subpath_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), Continuous fun x => (γ.subpath x.1 x.2.1) x.2.2
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The injection of `X` in the optimal coupling between `X` and `Y` is an isometry.  -/
GromovHausdorff.isometry_optimalGHInjl : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y], Isometry (GromovHausdorff.optimalGHInjl X Y)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_fst_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) =
    0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.support_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), (G.subgraphOfAdj h).support = {u, v}
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.prodMk : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {x : M} {f : M → M'} {g : M → M''}, MDiffAt f x → MDiffAt g x → (MDiffAt fun x => (f x, g x)) x
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The first part of the third simplicial identity  -/
SimplexCategory.δ_comp_σ_self_assoc : ∀ {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategory} (h : { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) =
    h
-- Lean.Parser.Command
Lean.Parser.Command.structParent.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddHom.ofDense.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddSemigroup M] [inst_1 : AddSemigroup N] {s : Set M} (f : M → N)
  (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y),
  AddHom.ofDense f hs hmul = { toFun := f, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- The sequence of sets in `C` with finite measures  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.set : {α : Type u_1} →
  {m0 : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → {C : Set (Set α)} → μ.FiniteSpanningSetsIn C → ℕ → Set α
-- Mathlib.Data.Multiset.Powerset
Multiset.mem_powerset : ∀ {α : Type u_1} {s t : Multiset α}, s ∈ t.powerset ↔ s ≤ t
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instLawfulIteratorLoop : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] [LawfulMonad n], Std.LawfulIteratorLoop (Std.Rxc.Iterator α) Id n
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_pow : ∀ {ι : Type u_2} {M : Type u_5} [inst : CommMonoid M] {m : Multiset ι} {f : ι → M} {n : ℕ},
  (Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
-- Mathlib.Order.Partition.Basic
Partition.top_def : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α], ⊤ = Partition.removeBot {s} ⋯ ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.algebraMap_apply : ∀ {α : Type u} {γ : Type w} {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing γ]
  [inst_3 : NormedAlgebra 𝕜 γ] (k : 𝕜) (a : α), ((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k • 1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- The preimage of a semilinear set under a homomorphism in a finitely generated monoid is
semilinear.  -/
IsSemilinearSet.preimage : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5}
  [inst_3 : FunLike F M N] [AddMonoidHomClass F M N] {s : Set N},
  IsSemilinearSet s → ∀ (f : F), IsSemilinearSet (⇑f ⁻¹' s)
-- Lean.CoreM
Lean.Core.Context.openDecls : Lean.Core.Context → List Lean.OpenDecl
-- Mathlib.Data.EReal.Operations
/-- For any two extended real numbers `a` and `b`, if both `a` and `b` are greater than `0`,
then their sum is also greater than `0`.  -/
EReal.add_pos : ∀ {a b : EReal}, 0 < a → 0 < b → 0 < a + b
-- Mathlib.GroupTheory.Perm.Sign
/-- Permutations of a given sign.  -/
Equiv.Perm.ofSign : {α : Type u} → [DecidableEq α] → [Fintype α] → ℤˣ → Finset (Equiv.Perm α)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_map_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelCommMonoid α] (s : Finset α) (a : α),
  addRothNumber (Finset.map (addLeftEmbedding a) s) = addRothNumber s
-- Init.Data.List.Scan.Lemmas
List.getElem?_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {i : ℕ} {f : α → β → β},
  (List.scanr f b l)[i]? = if i < l.length + 1 then some (List.foldr f b (List.drop i l)) else none
-- Mathlib.Probability.Independence.Process.Basic
/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
$(X_{s_1}, ..., X_{s_p})$.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.Kernel.IndepFun.indepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : Type u_5} {𝓨 : S → Type u_6}
  [inst : MeasurableSpace 𝓧] [inst_1 : (i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i},
  AEMeasurable X (P.bind ⇑κ) →
    (∀ (i : S), AEMeasurable (Y i) (P.bind ⇑κ)) →
      (∀ (I : Finset S), ProbabilityTheory.Kernel.IndepFun X (fun ω i => Y (↑i) ω) κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.Kernel.IndepFun X (fun ω i => Y i ω) κ P
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyLE.isLocalMax : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  g ≤ᶠ[nhds a] f → f a = g a → IsLocalMax f a → IsLocalMax g a
-- Mathlib.Algebra.CharP.Two
CharTwo.eq_add_iff_add_eq : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] {a b c : R}, a = b + c ↔ a + c = b
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.id_iso : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.Localization.Lifting.iso L W L (CategoryTheory.Functor.id D) = L.rightUnitor
-- Aesop.RuleTac.GoalDiff
/-- `FVarId`s that appear in the old goal, but not (or with a different type)
in the new goal.  -/
Aesop.GoalDiff.removedFVars : Aesop.GoalDiff → Std.HashSet Lean.FVarId
-- Mathlib.Algebra.Category.Ring.Basic
/-- The type of morphisms in `RingCat`.  -/
RingCat.Hom : RingCat → RingCat → Type u
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_congr_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_zero : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The matrix `S = [[0, -1], [1, 0]]` as an element of `SL(2, ℤ)`.

This element acts naturally on the Euclidean plane as a rotation about the origin by `π / 2`.

This element also acts naturally on the hyperbolic plane as rotation about `i` by `π`. It
represents the Mobiüs transformation `z ↦ -1/z` and is an involutive elliptic isometry.  -/
ModularGroup.S : Matrix.SpecialLinearGroup (Fin 2) ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isoOverPullback_hom_left_comp_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] {P : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  (h : CategoryTheory.IsPullback fst snd f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left h.isoOverPullback.hom)
      (CategoryTheory.Limits.pullback.snd f g) =
    snd
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertIfNewₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.fix.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : Turing.ToPartrec.Cont} {a_2 : Turing.ToPartrec.Code} {a_3 : Turing.ToPartrec.Cont},
  Turing.ToPartrec.Cont.fix a a_1 = Turing.ToPartrec.Cont.fix a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.SInt.Lemmas
Int8.add_eq_right : ∀ {a b : Int8}, a + b = b ↔ a = 0
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The counit for the equivalence `Mon (C ⥤ D) ≌ C ⥤ Mon D`.
 -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.comp
              CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor ≅
            CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.Mon D))
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_le_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] (x : E),
  ExistsContDiffBumpBase.u x ≤ 1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ringCon_injective : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], Function.Injective TwoSidedIdeal.ringCon
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (fg : (α →₀ M) × (β →₀ M)) (y : β),
  (Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.quotient_mk_eq_mk : ∀ {M : Type u_1} [inst : Monoid M] (a : M), ⟦a⟧ = Associates.mk a
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableOn.smul` -/
DifferentiableOn.fun_smul : ∀ {𝕜 : 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}
  {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun i => c i • f i) s
-- Mathlib.Algebra.Order.Floor.Ring
Int.le_floor_add_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (h₀ : f.obj' 0 _proof_245✝ = g.obj' 0 _proof_245✝) (h₁ : f.obj' 1 _proof_246✝ = g.obj' 1 _proof_246✝)
  (h₂ : f.obj' 2 _proof_247✝ = g.obj' 2 _proof_247✝),
  f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
        (CategoryTheory.CategoryStruct.comp (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          (CategoryTheory.eqToHom ⋯)) →
    f.map' 1 2 _proof_246✝ _proof_247✝ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
          (CategoryTheory.CategoryStruct.comp (g.map' 1 2 _proof_246✝ _proof_247✝) (CategoryTheory.eqToHom ⋯)) →
      f = g
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.starClosure_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A),
  S.starClosure.toSubalgebra = S ⊔ star S
-- Mathlib.Topology.Category.TopPair
/-- The proof that the homotopies fit into a commutative square with the maps of the pairs.  -/
TopPair.Homotopy.w : ∀ {X Y : TopPair} {f g : X ⟶ Y} (self : TopPair.Homotopy f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
      self.fst.h =
    CategoryTheory.CategoryStruct.comp self.snd.h TopPair.map
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_one_le_natCast_iff : ∀ {n : WithBot ℕ∞} {m : ℕ}, n + 1 ≤ ↑m ↔ n < ↑m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instUniformSpace : {A : Type u_1} → [NonUnitalCStarAlgebra A] → {m : Type u_2} → {n : Type u_3} → UniformSpace (CStarMatrix m n A)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductData_bicone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
  (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃)
  (fst : T.obj₂ ⟶ T.obj₁)
  (total :
    CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr =
      CategoryTheory.CategoryStruct.id T.obj₂),
  (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.extension_proj : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : LieAlgebra.IsExtension i p), h.extension.proj = p
-- Mathlib.RingTheory.Artinian.Module
LinearMap.eventually_iInf_range_pow_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : Module.End R M), ∀ᶠ (n : ℕ) in Filter.atTop, ⨅ m, (f ^ m).range = (f ^ n).range
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : CategoryTheory.Category.{w', w} J]
  [Small.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C],
  CategoryTheory.Limits.PreservesColimitsOfShape J (AlgebraicGeometry.SheafedSpace.forget C)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.eq_5 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc m, Int.ofNat n => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_5 m n
-- Lean.Language.Lean.Types
/-- State before the command is elaborated. This snapshot is always fulfilled immediately.  -/
Lean.Language.Lean.CommandParsedSnapshot.elabSnap : Lean.Language.Lean.CommandParsedSnapshot → Lean.Language.Lean.CommandElaboratingSnapshot
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAttemptAllParTac : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.instTensorAddUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.AddGrpObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Topology.Order.Lattice
OrderDual.topologicalLattice : ∀ (L : Type u_1) [inst : TopologicalSpace L] [inst_1 : Lattice L] [TopologicalLattice L], TopologicalLattice Lᵒᵈ
-- Mathlib.Analysis.Convex.Basic
convex_Ioc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β),
  Convex 𝕜 (Set.Ioc r s)
-- Mathlib.Order.Comparable
IncompRel.decidableRel : {α : Type u_1} → {r : α → α → Prop} → [DecidableRel r] → DecidableRel (IncompRel r)