mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.eval.congr_simp : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  (f f_1 : HahnEmbedding.Partial seed),
  f = f_1 → ∀ [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] (x x_1 : M), x = x_1 → f.eval x = f_1.eval x_1
-- Mathlib.Data.Finset.Density
/-- Density of a finset.

`dens s` is the number of elements of `s` divided by the size of the ambient type `α`.  -/
Finset.dens : {α : Type u_2} → [Fintype α] → Finset α → ℚ≥0
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppAux : Lean.Syntax →
  Array Lean.Elab.Term.NamedArg → Array Lean.Elab.Term.Arg → Bool → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.subtype.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A),
  AddMemClass.subtype S' = { toFun := Subtype.val, map_add' := ⋯ }
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_sup_hom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.π_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : ↑(groupHomology.cycles A n)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ n))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A n)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.π B n))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesMap f φ n)) x)
-- Mathlib.Order.Hom.Basic
/-- An order isomorphism is also an order isomorphism between dual orders.  -/
OrderIso.dual : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → αᵒᵈ ≃o βᵒᵈ
-- Mathlib.Data.PEquiv
PEquiv.trans_eq_none : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α),
  (f.trans g) a = none ↔ ∀ (b : β) (c : γ), b ∉ f a ∨ c ∉ g b
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] (r : A) (s : Set B)
  (B' : Subalgebra R B),
  r • s ⊆ ↑B' → ∀ {x : B}, x ∈ Algebra.adjoin R s → (algebraMap A B) r ∈ B' → ∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ B'
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈_diag : ∀ (i : Fin 8), CartanMatrix.E₈ i i = 2
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_one : ∀ {R : Type u_1} [inst : Semiring R], (HahnSeries.ofPowerSeries ℤ R) 1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → Sort u_3)
  (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hl),
  (match Std.DTreeMap.Internal.Impl.leaf, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl => h_2 sz k' v' l' r' hl) =
    h_1 hl
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_restrict_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (V : X.Opens)
  (hV : Dense ↑V) (hV' : V ≤ U), ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.rfl : ∀ {x : PSet.{u_1}}, x.Equiv x
-- Std.Time.Date.ValidDate
_private.Std.Time.Date.ValidDate.0.Std.Time.Month.Ordinal.days.eq_1 : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.days leap month =
    if ↑month = 2 then if leap = true then 29 else 28
    else
      match Std.Time.Month.Ordinal.monthSizesNonLeap✝ with
      | ⟨months, p⟩ =>
        let index := (Std.Time.Internal.Bounded.LE.sub month 1).toFin Std.Time.Month.Ordinal.days._proof_1✝;
        let idx := Fin.cast ⋯ index;
        months[idx]
-- Mathlib.Topology.Compactness.SigmaCompact
SigmaCompactSpace.exists_compact_covering : ∀ {X : Type u_1} [inst : TopologicalSpace X] [h : SigmaCompactSpace X],
  ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
-- Mathlib.Data.List.Sigma
List.keys_nil : ∀ {α : Type u} {β : α → Type v}, [].keys = []
-- Mathlib.Algebra.Ring.Subsemiring.Order
/-- A subsemiring of an ordered semiring is an ordered semiring.  -/
SubsemiringClass.toIsOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : SetLike S R] (s : S) [inst_1 : Semiring R] [inst_2 : PartialOrder R]
  [IsOrderedRing R] [inst_4 : SubsemiringClass S R], IsOrderedRing ↥s
-- Mathlib.Order.Compare
LT.lt.cmp_eq_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x < y → cmp y x = Ordering.gt
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.toPlus_plusLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
  CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The range of an `AddHom` is an `AddSubsemigroup`.  -/
AddHom.srange : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → AddSubsemigroup N
-- Batteries.Data.UnionFind.Lemmas
_private.Batteries.Data.UnionFind.Lemmas.0.Batteries.UnionFind.root_link.go : ∀ {self : Batteries.UnionFind} {x y : Fin self.size},
  self.parent ↑x = ↑x →
    self.parent ↑y = ↑y →
      ∀ {m : Batteries.UnionFind},
        (∀ (i : ℕ), m.parent i = if ↑y = i then ↑x else self.parent i) →
          ∀ (i : ℕ), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.List.toFinmap'.eq_1 : ∀ {α : Type u} {β : Type v} (xs : List (α × β)),
  Plausible.TotalFunction.List.toFinmap' xs =
    List.map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      xs
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm.inj : ∀ {c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {e : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {p : Lean.Grind.CommRing.Poly} {c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr}
  {e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {p_1 : Lean.Grind.CommRing.Poly},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm c_1 e_1 p_1 →
    c = c_1 ∧ e = e_1 ∧ p = p_1
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_norm_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  (x : A), ‖WithLp.toLp 1 ↑x‖ = ‖x‖
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_sub_lt_descFactorial' : ∀ {n k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
-- Batteries.Lean.Except
Except.map_pmap : ∀ {β γ : Type u_1} {ε : Type u_2} {α : Type u_1} (g : β → γ) (x : Except ε α) (f : (a : α) → x = Except.ok a → β),
  g <$> x.pmap f = x.pmap fun a h => g (f a h)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Roc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Roc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_vadd_pure : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] (v : V) (p : P),
  AffineSpace.asymptoticNhds k V v +ᵥ pure p = AffineSpace.asymptoticNhds k P v
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are two independent and integrable random variables, and `B` is a function of
two variables such that `‖B x y‖ₑ ≤ C * ‖x‖ₑ * ‖y‖ₑ`, then `B X Y` is integrable.

This is useful in particular if `B` is a continuous bilinear map.  -/
ProbabilityTheory.IndepFun.integrable_op : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_4 : TopologicalSpace F] [inst_5 : ContinuousENorm F] [inst_6 : MeasurableSpace F] [OpensMeasurableSpace F]
  [inst_8 : TopologicalSpace G] [inst_9 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ →
      MeasureTheory.Integrable Y μ →
        ∀ (B : E → F → G),
          Continuous (Function.uncurry B) →
            ∀ (C : NNReal),
              (∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ) → MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ici_add_one_eq_Ioi : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a : α),
  Set.Ici (a + 1) = Set.Ioi a
-- Mathlib.Analysis.Convex.Topology
/-- A convex set `s` is strictly convex provided that for any two distinct points of
`s \ interior s`, the line passing through these points has nonempty intersection with
`interior s`.  -/
Convex.strictConvex' : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ((s \ interior s).Pairwise fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior s) → StrictConvex 𝕜 s
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Splitting` of an additive group extension is a section homomorphism.  -/
AddGroupExtension.Splitting : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] → [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → AddGroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.Topology.Compactness.Lindelof
Quotient.lindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X} [LindelofSpace X], LindelofSpace (Quotient s)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_pow_atTop_nhds_zero_iff : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜]
  [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜},
  Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0) ↔ |r| < 1
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_of_inner_tendsto : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E]
  (𝕜 : Type u_2) [inst_1 : RCLike 𝕜] [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E],
  (∀ (y : E), Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖inner 𝕜 y x‖}) Filter.atTop (nhds 0)) →
    MeasureTheory.IsTightMeasureSet S
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_balanceR : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.balanceR x r).dual = r.dual.balanceL x l.dual
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜], analyticOrderAt id 0 = 1
-- Mathlib.RingTheory.Congruence.Hom
/-- Surjective ring homomorphisms constant on the equivalence classes
of a ring congruence relation induce a surjective homomorphism on the quotient.  -/
RingCon.lift_surjective_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  {h : c ≤ RingCon.ker f}, Function.Surjective ⇑(c.lift f h) ↔ Function.Surjective ⇑f
-- Init.Grind.Lemmas
Lean.Grind.of_eq_eq_false : ∀ {a b : Prop}, (a = b) = False → a ∧ ¬b ∨ ¬a ∧ b
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], ‖0‖₊ = 0
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.isQuadraticExtension : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K],
  Algebra.IsQuadraticExtension (↥(NumberField.maximalRealSubfield K)) K
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_zero : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Zero β], (UniformOnFun.toFun 𝔖) 0 = 0
-- Mathlib.Data.Sum.Interval
Sum.instLocallyFiniteOrderTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [LocallyFiniteOrderTop α] → [LocallyFiniteOrderTop β] → LocallyFiniteOrderTop (α ⊕ β)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_id : ∀ {V : Type u_1} (G : SimpleGraph V), SimpleGraph.map id G = G
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_splits : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat ++ t₂)
-- Mathlib.Algebra.Prime.Lemmas
pow_injective_of_not_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {q : M},
  ¬IsUnit q → q ≠ 0 → Function.Injective fun n => q ^ n
-- Init.Data.UInt.Lemmas
UInt16.size_le_usizeSize : UInt16.size ≤ USize.size
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_roo : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((compare e.1 lowerBound).isGT = true ∧ (compare e.1 upperBound).isLT = true))
          (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_neg_vadd_symmDiff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (symmDiff (-c +ᵥ s) t) = μ (symmDiff s (c +ᵥ t))
-- Mathlib.Order.Interval.Set.Image
StrictMono.mapsTo_Ioo : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
-- Init.Data.Iterators.Basic
Std.IterM.Step.toPure_done : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.IterM Id β} {h : it.IsPlausibleStep Std.IterStep.done},
  Std.IterM.Step.toPure ⟨Std.IterStep.done, h⟩ = Std.PlausibleIterStep.done h
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) (c c' : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxRightLinear.δᵣ F
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) c'))
-- Mathlib.Data.Nat.Upto
/-- The successor of `n` is in `Nat.Upto p` provided that `n` doesn't satisfy `p`.  -/
Nat.Upto.succ : {p : ℕ → Prop} → (x : Nat.Upto p) → ¬p ↑x → Nat.Upto p
-- Mathlib.RingTheory.Valuation.Basic
/-- Two additive valuations on `R` are defined to be equivalent if they induce the same
preorder on `R`.  -/
AddValuation.IsEquiv : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
          [inst_2 : LinearOrderedAddCommMonoidWithTop Γ'₀] → AddValuation R Γ₀ → AddValuation R Γ'₀ → Prop
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.compl_mem_cofinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, sᶜ ∈ μ.cofinite ↔ μ s < ⊤
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The bijection `(g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h)` induced by an adjunction
`l ⊣ r` in a bicategory.  -/
CategoryTheory.Bicategory.Adjunction.homEquiv₁ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {b c d : B} →
      {l : b ⟶ c} →
        {r : c ⟶ b} →
          CategoryTheory.Bicategory.Adjunction l r →
            {g : b ⟶ d} →
              {h : c ⟶ d} → (g ⟶ CategoryTheory.CategoryStruct.comp l h) ≃ (CategoryTheory.CategoryStruct.comp r g ⟶ h)
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInv_le_isUnit : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M), S.leftInv ≤ IsUnit.submonoid M
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.instTotalComplexShapeSymmetryIntUp : TotalComplexShapeSymmetry (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)
-- Init.Data.AC
Lean.Data.AC.EvalInformation.mk : {α : Sort u} → {β : Sort v} → (α → β) → (α → β → β → β) → (α → ℕ → β) → Lean.Data.AC.EvalInformation α β
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.const_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.CosimplicialObject.Augmented.const.map f).left = f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.instIsEquivalenceOppositeOpOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.opOp C).IsEquivalence
-- Mathlib.LinearAlgebra.Pi
Submodule.pi_empty : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (p : (i : ι) → Submodule R (φ i)), Submodule.pi ∅ p = ⊤
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instOne : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → One (A →A[R] A)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.multiplicity_eq_iff : ∀ {α : Type u_1} [inst : Monoid α] {a b : α},
  FiniteMultiplicity a b → ∀ {n : ℕ}, multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G),
  CategoryTheory.Pseudofunctor.Grothendieck.map α =
    { obj := fun a => { base := a.base, fiber := (α.app { as := a.base }).toFunctor.obj a.fiber },
      map := fun {a b} f =>
        { base := f.base,
          fiber :=
            CategoryTheory.CategoryStruct.comp ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber)
              ((α.app { as := b.base }).toFunctor.map f.fiber) },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α), κ.sectR a = κ.comap (fun b => (a, b)) ⋯
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_top : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), x ∈ ⊤
-- Mathlib.GroupTheory.Subgroup.Center
/-- A group is commutative if the center is the whole group.  -/
Group.commGroupOfCenterEqTop : {G : Type u_1} → [inst : Group G] → Subgroup.center G = ⊤ → CommGroup G
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.dim_eq : ∀ {X : SSet} {x y : X.S}, x.IsUniquelyCodimOneFace y → y.dim = x.dim + 1
-- Mathlib.GroupTheory.Subgroup.Saturated
Submonoid.powSaturated_iff_npow : ∀ {G : Type u_1} [inst : Monoid G] {H : Submonoid G}, H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.Order.LiminfLimsup
Filter.sup_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α),
  a ⊔ Filter.liminf u f = Filter.liminf (fun x => a ⊔ u x) f
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_fdiv_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), b ≠ 0 → (a + b * c).fdiv b = a.fdiv b + c
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- If `R` and `n` have decidable equality then so does `SL(n, R)`.  -/
Matrix.SpecialLinearGroup.instDecidableEq : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → [DecidableEq R] → DecidableEq (Matrix.SpecialLinearGroup n R)
-- Qq.ForLean.ToExpr
instToExprExpr_qq : Lean.ToExpr Lean.Expr
-- Mathlib.Topology.UniformSpace.Basic
IsClosed.relImage_of_finite : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → ∀ {t : Set α}, t.Finite → IsClosed (s.image t)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_eq_of_not_isMax : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [DenselyOrdered ι]
  (𝓕 : MeasureTheory.Filtration ι m) {i : ι}, ¬IsMax i → ↑𝓕.rightCont i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
-- Mathlib.Data.WSeq.Basic
/-- The monadic `return a` is a singleton list containing `a`.  -/
Stream'.WSeq.ret : {α : Type u} → α → Stream'.WSeq α
-- Mathlib.Algebra.RingQuot
RingQuot.instAlgebra : {R : Type uR} →
  [inst : Semiring R] →
    {S : Type uS} → [inst_1 : CommSemiring S] → [Algebra S R] → (r : R → R → Prop) → Algebra S (RingQuot r)