mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_one_div_le_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I : Submodule R A}, I * (1 / I) ≤ 1
-- Mathlib.Analysis.CStarAlgebra.Exponential
selfAdjoint.continuous_expUnitary : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A], Continuous selfAdjoint.expUnitary
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioo a b).OrdConnected
-- Mathlib.Algebra.Module.Basic
Units.neg_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (u : Rˣ) (x : M),
  -u • x = -(u • x)
-- Init.Data.String.Defs
/-- The underlying byte offset of the `Pos`.  -/
String.Pos.offset : {s : String} → s.Pos → String.Pos.Raw
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tprod_setProd_singleton_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β) (t : Set γ)
  (f : β × γ → α), ∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.completeTheory_eq : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N → L.completeTheory M = L.completeTheory N
-- Std.Sync.CancellationContext
Std.CancellationContext.mk.sizeOf_spec : ∀ (state : Std.Mutex Std.CancellationContext.State) (token : Std.CancellationToken) (id : UInt64),
  sizeOf { state := state, token := token, id := id } = 1 + sizeOf state + sizeOf token + sizeOf id
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] → [DecidableEq α] → (a : α) → DecidablePred fun x => x ∈ AddAction.stabilizer G a
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.inductiveFixpoint.sizeOf_spec : sizeOf Lean.Elab.PartialFixpointType.inductiveFixpoint = 1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGT? k = t₂.getGT? k
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.of_pow' : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {n : ℕ},
  (f ^ n).Separable → IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
-- Lean.AuxRecursor
Lean.isAuxRecursor : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Hom.ext_iff : ∀ {R : Type u} {inst : Ring R} {M N : ModuleCat R} {x y : M.Hom N}, x = y ↔ x.hom' = y.hom'
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.h : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.right_invariance' : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H},
      e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_sub_eq_sub_val : ∀ {α : Type u} [inst : SubtractionMonoid α] (u₁ u₂ : AddUnits α), ↑(u₁ - u₂) = ↑u₁ - ↑u₂
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_inter_le_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev.eq_1 : ∀ {α : Type u} (w : List (α × Bool)), FreeGroup.invRev w = (List.map (fun g => (g.1, !g.2)) w).reverse
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr_symm_apply_left : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₂ ⋊[φ₂] G₂),
  ((SemidirectProduct.congr fn fg h).symm x).left = fn.symm x.left
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- If `F` is a normed `ℝ`-algebra with a multiplicative norm (and such that `‖1‖ = 1`),
e.g., a normed division ring, then every `x : F` is the root of a monic quadratic polynomial
with real coefficients.  -/
NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] [NormOneClass F] [NormMulClass F] (x : F),
  ∃ p, p.IsMonicOfDegree 2 ∧ (Polynomial.aeval x) p = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, a ∈ t → t[a]? = some t[a]!
-- Aesop.Nanos
Aesop.Nanos.instHDivNat : HDiv Aesop.Nanos ℕ Aesop.Nanos
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)),
  (f.comp g).comp h = f.comp (g.comp h)
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_and : ∀ (a b : UInt64), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Order.Preorder.Finsupp
Finsupp.support_inf_union_support_sup : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Lattice M] (f g : ι →₀ M) [inst_2 : DecidableEq ι],
  (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.enorm_ae_le_eLpNormEssSup : ∀ {α : Type u_1} {ε : Type u_8} [inst : ENorm ε] {x : MeasurableSpace α} (f : α → ε) (μ : MeasureTheory.Measure α),
  ∀ᵐ (x_1 : α) ∂μ, ‖f x_1‖ₑ ≤ MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Data.Analysis.Topology
locallyFinite_iff_exists_realizer : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (F : Ctop.Realizer α) {f : β → Set α},
  LocallyFinite f ↔ Nonempty (LocallyFinite.Realizer F f)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFiltered_of_directed_le_nonempty : ∀ (α : Type u) [inst : Preorder α] [IsDirectedOrder α] [Nonempty α], CategoryTheory.IsFiltered α
-- Lean.Meta.Tactic.Grind.Types
/-- Equations and propositions to be processed.  -/
Lean.Meta.Grind.GoalState.newFacts : Lean.Meta.Grind.GoalState → Array Lean.Meta.Grind.NewFact
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_mk0 : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B]
  (I : ↥(nonZeroDivisors (Ideal A))),
  (ClassGroup.extendedHom A B) (ClassGroup.mk0 I) = ClassGroup.mk0 (ClassGroup.extendedIdeal A B I)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- Condition that a `LocalizerMorphism` induces an equivalence on the localized categories  -/
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set α} {t : Set β},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s ×ˢ t)
-- Init.Grind.AC
Lean.Grind.AC.Context.op : {α : Sort u} → Lean.Grind.AC.Context α → α → α → α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_inv_mul_iff₀'` for a version with multiplication on the other side.  -/
lt_inv_mul_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a < c⁻¹ * b ↔ c * a < b)
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.coe_mulSupport : ∀ {G : Type u_1} [inst : Group G] (M : Submonoid G), ↑M.mulSupport = ↑M ∩ (↑M)⁻¹
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.toOuterMeasure_bindOnSupport_apply : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β),
  (p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Each element of the monoid defines an additive monoid homomorphism.  -/
DistribMulAction.toAddMonoidHom : {M : Type u_1} → (A : Type u_7) → [inst : Monoid M] → [inst_1 : AddMonoid A] → [DistribMulAction M A] → M → A →+ A
-- Lean.Environment
Lean.Kernel.Exception.exprTypeMismatch.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr expectedType : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.exprTypeMismatch env lctx expr expectedType) =
    1 + sizeOf env + sizeOf lctx + sizeOf expr + sizeOf expectedType
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_lt_mul_of_neg_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], b < a → c < 0 → a * c < b * c
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.continuousOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {s : Set 𝕜} {f f' : 𝕜 → F}, (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → ContinuousOn f s
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry'_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] {f f' : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y},
  CategoryTheory.MonoidalClosed.uncurry' f = CategoryTheory.MonoidalClosed.uncurry' f' → f = f'
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colim.map α) =
    CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.Limits.colimit.ι G j)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.nsmulFn : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- IO ref for reassociation handlers `reassoc` attribute, so that it can be extended
with additional handlers. Handlers take a proof of the equation.

The default handler is `reassocExprHom` for morphism reassociation.
This will be extended in `Tactic.CategoryTheory.IsoReassoc` for isomorphism reassociation.
 -/
_private.Mathlib.Tactic.CategoryTheory.Reassoc.0.Mathlib.Tactic.Reassoc.reassocImplRef : IO.Ref (Array (Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)))
-- Batteries.Data.AssocList
Batteries.AssocList.any_eq : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Batteries.AssocList α β),
  Batteries.AssocList.any p l =
    l.toList.any fun x =>
      match x with
      | (a, b) => p a b
-- Init.Internal.Order.Basic
/-- The least fixpoint of a monotone function is the least upper bound of its transfinite iteration.

The `monotone f` assumption is not strictly necessarily for the definition, but without this the
definition is not very meaningful and it simplifies applying theorems like `fix_eq` if every use of
`fix` already has the monotonicity requirement.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.fix : {α : Sort u} → [inst : Lean.Order.CCPO α] → (f : α → α) → Lean.Order.monotone f → α
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.edges_toPath_subset_edges`. -/
SimpleGraph.Walk.edges_toPath_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).edges ⊆ p.edges
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_monoidHom_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `coprodComparison` morphism in both arguments.  -/
CategoryTheory.Limits.coprodComparison_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B)
      (F.map (CategoryTheory.Limits.coprod.map f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g))
      (CategoryTheory.Limits.coprodComparison F A' B')
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprRingMode : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.RingNF.RingMode
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.Tendsto.prod_map_prod_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ}
  {g : β → γ},
  Filter.Tendsto f F Filter.atTop →
    Filter.Tendsto g G Filter.atTop → Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atTop
-- Init.Data.UInt.Lemmas
UInt32.le_of_lt : ∀ {a b : UInt32}, a < b → a ≤ b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_eq_sum : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R}, Polynomial.eval x p = p.sum fun e a => a * x ^ e
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- A constructor for continuous maps out of a one point compactification, given a continuous map from
the underlying space and a limit value at infinity.
 -/
OnePoint.continuousMapMk : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {Y : Type u_3} →
      [inst_1 : TopologicalSpace Y] →
        (f : C(X, Y)) → (y : Y) → Filter.Tendsto (⇑f) (Filter.coclosedCompact X) (nhds y) → C(OnePoint X, Y)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.mk_eq_rank' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] (v : Module.Basis ι R M),
  Cardinal.lift.{max v m, w} (Cardinal.mk ι) = Cardinal.lift.{max w m, v} (Module.rank R M)
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Multiplicative version of `Prod.nnnorm_def`.
Earlier, this name was used for the additive version.  -/
Prod.nnnorm_def' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] (x : E × F),
  ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊
-- Init.Data.Array.Attach
Array.attachWith_ne_empty_iff : ∀ {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}, xs.attachWith P H ≠ #[] ↔ xs ≠ #[]
-- Mathlib.Data.Fintype.Sets
Prop.fintype : Fintype Prop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_sheaf : ∀ (R : CommRingCat), (AlgebraicGeometry.Spec R).sheaf = AlgebraicGeometry.Spec.structureSheaf ↑R
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `f` is `ℝ`-valued and integrable, then for any `c < 0` the set `{x | f x < c}` has finite
measure.  -/
MeasureTheory.Integrable.measure_lt_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β],
  MeasureTheory.Integrable f μ → ∀ {c : β}, c < 0 → μ {a | f a < c} < ⊤
-- Mathlib.Algebra.Module.GradedModule
_private.Mathlib.Algebra.Module.GradedModule.0.DirectSum.Gmodule.one_smul' : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M]
  (x : DirectSum ιB fun i => M i), 1 • x = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  [hi : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.add_sub_add_comm : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute c d → AddCommute b (-c) → a + b - (c + d) = a - c + (b - d)
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- A set which is `EventuallyEq` to an `EventuallyMeasurableSet`
is an `EventuallyMeasurableSet`.  -/
EventuallyMeasurableSet.congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} {l : Filter α} [inst : CountableInterFilter l],
  EventuallyMeasurableSet m l t → s =ᶠ[l] t → EventuallyMeasurableSet m l s
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestGrindTrace : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.Topology.Sequences
/-- A version of **Bolzano-Weierstrass**: in a (pseudo)metrizable space, a set is compact if and
only if it is sequentially compact.  -/
isCompact_iff_isSeqCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  IsCompact s ↔ IsSeqCompact s
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_uInt16ToBitVec : ∀ (n : UInt16), { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_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 α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (c : ℝ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom map in the oplax left unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                ((CategoryTheory.MonoidalCategory.curriedTensorPre F).obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                  F.comp (CategoryTheory.MonoidalCategory.tensorUnitLeft D))
-- Mathlib.Data.Finset.Max
Finset.max'_subset : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t), s.max' H ≤ t.max' ⋯
-- Lean.Meta.HasAssignableMVar
Lean.Meta.hasAssignableLevelMVar : Lean.Level → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.mk : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        {F : CategoryTheory.Functor C A} →
          {M : Type u_4} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] →
                (sequence : M → CategoryTheory.Functor C A) →
                  (sequence 0 ≅ F) →
                    (shiftIso :
                        (n a a' : M) →
                          n + a = a' → ((CategoryTheory.shiftFunctor C n).comp (sequence a) ≅ sequence a')) →
                      (∀ (a : M),
                          shiftIso 0 a a ⋯ =
                            CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (sequence a) ≪≫
                              (sequence a).leftUnitor) →
                        (∀ (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''),
                            shiftIso (m + n) a a'' ⋯ =
                              CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n)
                                  (sequence a) ≪≫
                                (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n)
                                    (sequence a) ≪≫
                                  (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (shiftIso n a a' ha') ≪≫
                                    shiftIso m a' a'' ha'') →
                          F.ShiftSequence M
-- Init.Data.BitVec.Lemmas
BitVec.lt_trans : ∀ {n : ℕ} {x y z : BitVec n}, x < y → y < z → x < z
-- Mathlib.Topology.Sets.VietorisTopology
/-- Given compact sets `K` and `Lᵢ ⊆ K`, the compact subsets of `K` intersecting every `Lᵢ` form a
compact set. This is an auxiliary result used for proving the local compactness of `Compacts α`
without assuming `T2Space α`.  -/
_private.Mathlib.Topology.Sets.VietorisTopology.0.TopologicalSpace.vietoris.isCompact_aux : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : Set α},
  IsCompact K →
    ∀ {s : Set (Set α)}, s ⊆ 𝒫 K → (∀ L ∈ s, IsCompact L) → IsCompact {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
-- Init.Data.Array.Lemmas
Array.all_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool}, (Array.map f xs).all p = xs.all (p ∘ f)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s t : Set β} {a : α}, a +ᵥ s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a +ᵥ b ∈ t
-- Mathlib.Algebra.Homology.QuasiIso
HomotopyEquiv.quasiIso_inv : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) [inst_2 : ∀ (n : ι), K.HasHomology n]
  [inst_3 : ∀ (n : ι), L.HasHomology n], QuasiIso e.inv
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_id_mul_left : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : Mul α] [inst_3 : AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → m)
  (e₂ : n ≃ o), M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.CreatesColimitOfIsSplitPair.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          ({A B : D} →
              (f g : A ⟶ B) →
                [G.IsSplitPair f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G) →
            CategoryTheory.Monad.CreatesColimitOfIsSplitPair G
-- Lean.Elab.InfoTree.Basic
_private.Lean.Elab.InfoTree.Basic.0.Lean.Elab.CompletionInfo.setStx : Lean.Syntax → Lean.Elab.CompletionInfo → Lean.Elab.CompletionInfo