mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.single_add : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (a : Γ) (r s : R),
  (HahnSeries.single a) (r + s) = (HahnSeries.single a) r + (HahnSeries.single a) s
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_empty : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Projectivization.IsCollinear ∅
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N),
  TensorProduct.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.map f₁ g₁ * TensorProduct.map f₂ g₂
-- Mathlib.Data.FunLike.Graded
/-- **Alias** of the forward direction of `Graded.map_mem_iff`. -/
Graded.mem_of_map_mem : ∀ {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι}
  {x : A}, e x ∈ ℬ i → x ∈ 𝒜 i
-- Mathlib.Data.Finset.Basic
Finset.erase_insert_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ≠ b → (insert a s).erase b = insert a (s.erase b)
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank.eq_1 : ∀ (α : Type u) (A : α → PSet.{u}), (PSet.mk α A).rank = ⨆ a, Order.succ (A a).rank
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A bounded convergence theorem for a finite measure:
If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant
and tend pointwise to a limit, then their integrals (`MeasureTheory.lintegral`) against the finite
measure tend to the integral of the limit.

A related result with more general assumptions is
`MeasureTheory.tendsto_lintegral_nn_filter_of_le_const`.
 -/
MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω) {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal},
  (∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
    ∀ {f : Ω → NNReal},
      (∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (nhds (f ω))) →
        Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCircuit_copy : ∀ {V : Type u} {G : SimpleGraph V} {u u' : V} (p : G.Walk u u) (hu : u = u'), (p.copy hu hu).IsCircuit ↔ p.IsCircuit
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toPartialOrderPackage : {α : Type u} → [self : Std.LinearOrderPackage α] → Std.PartialOrderPackage α
-- Init.SimpLemmas
false_implies : ∀ (p : Prop), (False → p) = True
-- Mathlib.Topology.Compactification.OnePoint.Basic
_private.Mathlib.Topology.Compactification.OnePoint.Basic.0.instReprOnePoint.match_1.splitter : {X : Type u_1} →
  (motive : OnePoint X → Sort u_2) → (o : OnePoint X) → (Unit → motive none) → ((a : X) → motive (some a)) → motive o
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.lcomapDomain.congr_simp : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : Type u_9} (f f_1 : α → β) (e_f : f = f_1) (hf : Function.Injective f),
  Finsupp.lcomapDomain f hf = Finsupp.lcomapDomain f_1 ⋯
-- Init.Data.Nat.Lemmas
Nat.lt_mul_iff_one_lt_right : ∀ {a b : ℕ}, 0 < a → (a < a * b ↔ 1 < b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → Std.DHashMap.Const.get? (m₁.diff m₂) k = none
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubmonoid_mono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Monotone Submodule.toAddSubmonoid
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (toSubstructure : L.Substructure M)
  (isElementary' : toSubstructure.IsElementary) (toSubstructure_1 : L.Substructure M)
  (isElementary'_1 : toSubstructure_1.IsElementary),
  ({ toSubstructure := toSubstructure, isElementary' := isElementary' } =
      { toSubstructure := toSubstructure_1, isElementary' := isElementary'_1 }) =
    (toSubstructure = toSubstructure_1)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isIdLike : Lean.Expr → Bool
-- Mathlib.Algebra.Group.AddChar
AddChar.ne_one_iff : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {ψ : AddChar A M}, ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.rel_of_inner : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Productive α m] {remaining : ℕ} {it it' : Std.IterM m β},
  it'.finitelyManySkips.Rel it.finitelyManySkips →
    Std.Iterators.Types.Take.Rel m (Std.IterM.take remaining it') (Std.IterM.take remaining it)
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.continuous_op : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous AddOpposite.op
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.comp_id : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), f.comp (MulSemiringActionHom.id M) = f
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_adj : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {x y : α'} (f : α → α'),
  (Graph.map f G).Adj x y ↔ Relation.Map G.Adj f f x y
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_localized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  (∀ (J : Ideal R) [inst_5 : J.IsMaximal], Function.Injective ⇑((LocalizedModule.map J.primeCompl) f)) →
    Function.Injective ⇑f
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltSubmodule_v_le_of_mem : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] {v : Valuation K Γ₀}
  {S : Submodule (↥v.integer) K} {x : K}, x ∈ S → ∀ (hxv : v x ≠ 0), v.ltSubmodule (Units.mk0 (v x) hxv) ≤ S
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.edist_eq_tsum : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → EDist (F i)] (x y : (i : ι) → F i),
  edist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (edist (x i) (y i))
-- Mathlib.Algebra.Group.Indicator
Set.apply_indicator_symmDiff : ∀ {α : Type u_1} {β : Type u_2} {G : Type u_6} [inst : AddGroup G] {g : G → β},
  (∀ (x : G), g (-x) = g x) →
    ∀ (s t : Set α) (f : α → G) (x : α), g ((symmDiff s t).indicator f x) = g (s.indicator f x - t.indicator f x)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₃ = CategoryTheory.Limits.cokernel.π g
-- Mathlib.NumberTheory.LucasLehmer
/-- Helper function for `sMod''`.  -/
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go : ℕ → ℕ → ℕ → ℕ
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.consumerNode : Lean.Meta.SynthInstance.ConsumerNode → Lean.Meta.SynthInstance.Waiter
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The `R`-bialgebra map from the group algebra on the group-like elements of `A` to `A`.  -/
MonoidAlgebra.liftGroupLikeBialgHom : {R : Type u_1} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → MonoidAlgebra R (GroupLike R A) →ₐc[R] A
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.PD.eq_1 : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.PD l R = Matrix.fromBlocks 1 (-1) 1 1
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The domain, taken in `Fib p R`, of some Cartesian morphism lifting a given
`f : R ⟶ S` in `𝒮`  -/
HasFibers.mkPullback : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] → [p.IsPreFibered] → {R S : 𝒮} → {a : 𝒳} → (R ⟶ S) → p.obj a = S → HasFibers.Fib p R
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_toSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A} {x : A},
  x ∈ S.toSubring ↔ x ∈ S
-- Mathlib.Order.Hom.Lattice
SupHom.instBoundedOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → [BoundedOrder β] → BoundedOrder (SupHom α β)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.whiskeringEquivalence`.

---

Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
CategoryTheory.Limits.Cones.whiskeringEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (e : K ≌ J) → CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (e.functor.comp F)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_bif' : ∀ (d a b c : Bool), ((bif d then a else c) == bif d then b else c) = (!d || a == b)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.comp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ ⟶ M₂) (g : M₂ ⟶ M₃) (X : Cᵒᵖ),
  (CategoryTheory.CategoryStruct.comp f g).app X = CategoryTheory.CategoryStruct.comp (f.app X) (g.app X)
-- Mathlib.RingTheory.Nilpotent.Lemmas
isRadical_iff_span_singleton : ∀ {R : Type u_1} {y : R} [inst : CommSemiring R], IsRadical y ↔ (Ideal.span {y}).IsRadical
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- A category "has enough injectives" if every object has an injective presentation,
i.e. if for every object `X` there is an injective object `J` and a monomorphism `X ↪ J`.  -/
CategoryTheory.EnoughInjectives.presentation : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.EnoughInjectives C] (X : C),
  Nonempty (CategoryTheory.InjectivePresentation X)
-- Mathlib.Tactic.CancelDenoms.Core
/-- `findCancelFactor e` produces a natural number `n`, such that multiplying `e` by `n` will
be able to cancel all the numeric denominators in `e`. The returned `Tree` describes how to
distribute the value `n` over products inside `e`.
 -/
Mathlib.Tactic.CancelDenoms.findCancelFactor : Lean.Expr → ℕ × BinaryTree ℕ
-- Mathlib.Topology.Order.Bornology
BddBelow.isBounded_inter : ∀ {α : Type u_1} {s t : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddBelow s → BddAbove t → Bornology.IsBounded (s ∩ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.of_is_bilimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPushout b.fst b.snd 0 0
-- Init.Data.Float.Float32
instHomogeneousPowFloat32 : HomogeneousPow Float32
-- Init.Data.Sum.Lemmas
Sum.getRight?.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (val : α), (Sum.inl val).getRight? = none
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects finite coproducts, then `F.rightOp : C ⥤ Dᵒᵖ` reflects finite
products.  -/
CategoryTheory.Limits.reflectsFiniteProducts_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsFiniteCoproducts F],
  CategoryTheory.Limits.ReflectsFiniteProducts F.rightOp
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.pre_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (k : K) {Z : C} (h : F.obj (E.obj k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (E.comp F) k) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (E.obj k)) h
-- Lean.Server.Requests
Lean.Server.RequestM.runCoreM : {α : Type} → Lean.Server.Snapshots.Snapshot → Lean.Server.RequestT Lean.CoreM α → Lean.Server.RequestM α
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_div : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (I J : Submodule R A) (h : A ≃ₐ[R] B),
  Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeOp_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.mapConeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
-- Mathlib.CategoryTheory.Presentable.Limits
/-- Auxiliary definition for `isCardinalAccessible_of_isLimit`.  -/
CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} K] →
        {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} →
          (c : CategoryTheory.Limits.Cone F) →
            ((Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c)) →
              (κ : Cardinal.{w}) →
                [inst_2 : Fact κ.IsRegular] →
                  HasCardinalLT (CategoryTheory.Arrow K) κ →
                    {J : Type w} →
                      [inst_3 : CategoryTheory.SmallCategory J] →
                        [CategoryTheory.IsCardinalFiltered J κ] →
                          {X : CategoryTheory.Functor J C} →
                            (cX : CategoryTheory.Limits.Cocone X) →
                              ((k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) →
                                CategoryTheory.Limits.IsColimit (c.pt.mapCocone cX)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.flatMapTR.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → List β) (a : Array β) (a_1 : α) (as : List α),
  List.flatMapTR.go✝ f (a_1 :: as) a = List.flatMapTR.go✝ f as (a ++ f a_1)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d')
  (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c''),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g₁ g₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₁ g₁)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₂ g₂)
-- Mathlib.Algebra.Order.Monovary
monovaryOn_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f (-g) s ↔ AntivaryOn f g s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).isEmpty = false →
    ((Std.DTreeMap.Const.alter t k f).maxKey! = k ↔
      (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.algebraMap_eq_gen_self : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  (algebraMap ↥F[x] ↥F⟮x⟯) ⟨x, ⋯⟩ = IntermediateField.AdjoinSimple.gen F x
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtension.instInhabited : {α σ : Type} → [Inhabited σ] → Inhabited (Lean.SimplePersistentEnvExtension α σ)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.homTo.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.WithInitial.homTo X = CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj X)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) →
      (motive : { u // u.toNat < buckets.size } → Sort u_3) →
        (x : { u // u.toNat < buckets.size }) →
          ((i : USize) → (hi : i.toNat < buckets.size) → motive ⟨i, hi⟩) → motive x
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum of two natural transformations, where all functors have the same target category.  -/
CategoryTheory.NatTrans.sum' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F G : CategoryTheory.Functor A C} →
              {H I : CategoryTheory.Functor B C} → (F ⟶ G) → (H ⟶ I) → (F.sum' H ⟶ G.sum' I)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_le_compl : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, t.compl ≤ s.compl ↔ t ≤ s
-- Mathlib.Algebra.DirectSum.Algebra
/-- Two `AlgHom`s out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas].  -/
DirectSum.algHom_ext' : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (A i)] [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι]
  [inst_4 : DirectSum.GSemiring A] [inst_5 : Semiring B] [inst_6 : DirectSum.GAlgebra R A] [inst_7 : Algebra R B]
  [inst_8 : DecidableEq ι] ⦃f g : (DirectSum ι fun i => A i) →ₐ[R] B⦄,
  (∀ (i : ι), f.toLinearMap ∘ₗ DirectSum.lof R ι A i = g.toLinearMap ∘ₗ DirectSum.lof R ι A i) → f = g
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.steps_le_m : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {m : ℕ} (self : StateTransition.EvalsToInTime f a b m),
  self.steps ≤ m
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.mem_toFinset : ∀ {α : Type u} {s : Set α} {a : α} (hs : s.Finite), a ∈ hs.toFinset ↔ a ∈ s
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_zero_of_dvd : ∀ {a b : ℤ}, a ∣ b → b.fmod a = 0
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- A monoid homomorphism from a monoid `M` to a group `G` lifts to a group homomorphism from the
Grothendieck group of `M` to `G`.  -/
Algebra.GrothendieckGroup.lift : {M : Type u_1} →
  {G : Type u_2} → [inst : CommMonoid M] → [inst_1 : CommGroup G] → (M →* G) ≃ (Algebra.GrothendieckGroup M →* G)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.instIsValuedInFlip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [P.IsValuedIn S], P.flip.IsValuedIn S
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instInhabited : (M : Type u_1) → [inst : TopologicalSpace M] → [inst_1 : Add M] → Inhabited (M ≃ₜ+ M)
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- For all `G`-split pairs `f,g`, `G` creates colimits of `parallelPair f g`.  -/
CategoryTheory.Monad.CreatesColimitOfIsSplitPair.out : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₁, u₂} D} →
        {G : CategoryTheory.Functor D C} →
          [self : CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] →
            {A B : D} →
              (f g : A ⟶ B) →
                [G.IsSplitPair f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.γ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (j : J),
  (CategoryTheory.Comonad.ForgetCreatesColimits'.γ D).app j = (D.obj j).a
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.hasNatScalar : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → SMul ℕ (LeftInvariantDerivation I G)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.tryTheoremWithExtraArgs? : Lean.Expr → Lean.Meta.SimpTheorem → ℕ → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.iterate : ∀ {α : Type u} [inst : Preorder α] {f : α → α}, RightOrdContinuous f → ∀ (n : ℕ), RightOrdContinuous f^[n]
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_div_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ
-- Mathlib.RingTheory.TensorProduct.Quotient
Ideal.subtype_rTensor_range : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  (↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)).range = I • ⊤