mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.DHashMap.Raw.filterMap f m} (h : m.WF), (Std.DHashMap.Raw.filterMap f m).getKey k h' = m.getKey k ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertManyIfNewUnit_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit}, m.insertManyIfNewUnit [] = m
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.takeWhile.go : {α : Type u} → (α → Bool) → Array α → ℕ → Array α → Array α
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.metricSpace : (p : ℕ) → [inst : Fact (Nat.Prime p)] → MetricSpace ℚ_[p]
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_add : ∀ (a b c : Ordinal.{u_1}), a ^ (b + c) = a ^ b * a ^ c
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_diff_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get! (m₁.diff m₂) k = default
-- Mathlib.RingTheory.Length
Submodule.height_strictMono : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M], StrictMono Order.height
-- Lean.DeprecatedModule
Lean.linter.deprecated.module : Lean.Option Bool
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.custom.sizeOf_spec : ∀ (msgData : Lean.MessageData), sizeOf (Lean.Elab.Term.MVarErrorKind.custom msgData) = 1 + sizeOf msgData
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.orderOf_five : ∀ (n : ℕ), orderOf 5 = 2 ^ n
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instIsAddApplyReal : ∀ {E : Type u_3} [inst : Group E], IsAddApply (GroupNorm E) E ℝ
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iUnion₂_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α}
  {t : (i : ι) → κ i → Set β} {f : α → β},
  (∀ (i : ι) (j : κ i), Set.SurjOn f (s i j) (t i j)) → Set.SurjOn f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j)
-- Mathlib.Analysis.Convex.Gauge
/-- The gauge is always nonnegative.  -/
gauge_nonneg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} (x : E), 0 ≤ gauge s x
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift.eq_1 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₁)
  (b : β₁), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f₁ a b)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
  {Z : C₄} (h_1 : (⋯.mapBifunctor K₃ G c₄).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp ⋯ h_1) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h_1
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Presheaf.coveringOfPresieve_apply : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U)
  (f : (V : TopologicalSpace.Opens ↑X) × { f // R f }), TopCat.Presheaf.coveringOfPresieve U R f = f.fst
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- A local subring is maximal with respect to the domination order
if and only if it is a valuation ring.  -/
LocalSubring.isMax_iff : ∀ {K : Type u_3} [inst : Field K] {A : LocalSubring K}, IsMax A ↔ ∃ B, B.toLocalSubring = A
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonUnitalNonAssocSemiring : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalNonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonUnitalNonAssocSemiring (TensorProduct R A B)
-- Mathlib.Logic.Relation
Relation.instTransReflTransGenTransGen : {α : Type u_1} → {r : α → α → Prop} → Trans (Relation.ReflTransGen r) (Relation.TransGen r) (Relation.TransGen r)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Compute the hash of a `RefinedDiscrTree.Key`.

Note: at the root, `.const` is the most common key, and it is very uncommon
to get the same constant name with a different arity.
So for performance, we just use `hash name` to hash `.const name _`.
 -/
Lean.Meta.RefinedDiscrTree.Key.hash : Lean.Meta.RefinedDiscrTree.Key → UInt64
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one`.  -/
Left.mul_lt_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, a < 1 → b < 1 → a * b < 1
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y} {α : Type u_1} {A B : α → C}
  (g : (i : α) → A i ⟶ B i) (c : HomotopicalAlgebra.RelativeCellComplex (fun x => g) f),
  (HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape g c).toTransfiniteCompositionOfShape =
    c.toTransfiniteCompositionOfShape
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.eventually_mem : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β},
  Filter.Tendsto f l₁ l₂ → s ∈ l₂ → ∀ᶠ (x : α) in l₁, f x ∈ s
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.match_1.eq_2 : ∀ {α : Type u_1} (motive : α ⊕ List (Computation α) → Sort u_2) (ls : List (Computation α))
  (h_1 : (a : α) → motive (Sum.inl a)) (h_2 : (ls : List (Computation α)) → motive (Sum.inr ls)),
  (match Sum.inr ls with
    | Sum.inl a => h_1 a
    | Sum.inr ls => h_2 ls) =
    h_2 ls
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.eraseₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.eraseₘ k t h =
    (Std.DTreeMap.Internal.Impl.updateCell k (fun x => Std.DTreeMap.Internal.Cell.empty) t h).impl
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_eq_natCast : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.C ↑n = ↑n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.mk.injEq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (obj obj_1 : B), ({ obj := obj } = { obj := obj_1 }) = (obj = obj_1)
-- Mathlib.Order.Extension.Well
/-- Any well-founded relation can be extended to a well-ordering on that type.  -/
IsWellFounded.exists_well_order_ge : ∀ {α : Type u} (r : α → α → Prop) [IsWellFounded α r], ∃ s, r ≤ s ∧ IsWellOrder α s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_get : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {h : Std.DTreeMap.Internal.Impl.contains a t = true},
      Std.DTreeMap.Internal.Impl.Const.get? t a = some (Std.DTreeMap.Internal.Impl.Const.get t a h)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.eval_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (f : σ → R) (φ : MvPolynomial σ R),
  (MvPolynomial.eval f) ((MvPolynomial.expand p) φ) = (MvPolynomial.eval (f ^ p)) φ
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_le_left : ∀ {a b : Ordinal.{u_4}}, a ≤ b → ∀ (c : Ordinal.{u_4}), a / c ≤ b / c
-- Mathlib.Topology.WithTopology
WithTopology.instLE : {X : Type u_1} → (t : TopologicalSpace X) → [LE X] → LE (WithTopology X t)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.congr_linearEquiv_trans : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Type u_3}
  {X : Type u_4} [inst_3 : AddCommGroup W] [inst_4 : Module R W] [inst_5 : AddCommGroup X] [inst_6 : Module R X]
  (e : V ≃ₗ[R] W) (f : W ≃ₗ[R] X),
  (SpecialLinearGroup.congr_linearEquiv e).trans (SpecialLinearGroup.congr_linearEquiv f) =
    SpecialLinearGroup.congr_linearEquiv (e ≪≫ₗ f)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_toAddSubmonoid : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), H.op.toAddSubmonoid = H.op
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {n : ℕ} {s : Batteries.BinomialHeap.Imp.HeapNode α},
  Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → Batteries.BinomialHeap.Imp.Heap.WF le 0 s.toHeap
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.of_image_filter : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] [inst_2 : DecidableEq H] (f : G →ₙ* H) {A B : Finset G}
  {aG bG : G} {aH bH : H},
  f aG = aH →
    f bG = bH →
      UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH →
        UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG → UniqueMul A B aG bG
-- Mathlib.Order.Completion
DedekindCut.lt_principal_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} {c : DedekindCut α}, c < DedekindCut.principal a ↔ ∃ b ∈ c.right, b < a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f V)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) h
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- If `I : InjectiveResolution X`, then the chosen `(injectiveResolutions C).obj X`
is isomorphic (in the homotopy category) to `I.cocomplex`.  -/
CategoryTheory.InjectiveResolution.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasInjectiveResolutions C] →
        {X : C} →
          (I : CategoryTheory.InjectiveResolution X) →
            (CategoryTheory.injectiveResolutions C).obj X ≅
              (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj I.cocomplex
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.algebraMap_residueField_surjective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsMaximal],
  Function.Surjective ⇑(algebraMap R I.ResidueField)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The weighted homogeneous submodules form a graded monoid.  -/
MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M},
  SetLike.GradedMonoid (MvPolynomial.weightedHomogeneousSubmodule R w)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.hom_inr_inl_false : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {Y : D} (f : Sum.inr X ⟶ Sum.inl Y), False
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f),
  CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) J.subschemeι =
    CategoryTheory.CategoryStruct.comp I.subschemeι f
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.op_sum : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
  {ι : Type u_2} (s : Finset ι) (f : ι → (X ⟶ Y)), (s.sum f).op = ∑ i ∈ s, (f i).op
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_surjective_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Surjective ⇑f → Function.Surjective (Submodule.map f)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Auxiliary definition for `extend.leftHomologyData`.  -/
HomologicalComplex.extend.leftHomologyData.cokernelCofork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        (hj' : e.f j = j') →
                          c.prev j = i →
                            c'.prev j' = i' →
                              (hk : c.next j = k) →
                                (hk' : c'.next j' = k') →
                                  (cone : CategoryTheory.Limits.KernelFork (K.d j k)) →
                                    (hcone : CategoryTheory.Limits.IsLimit cone) →
                                      CategoryTheory.Limits.CokernelCofork
                                          (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)) →
                                        CategoryTheory.Limits.CokernelCofork
                                          ((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk'
                                                cone hcone).lift
                                            (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.norm_star_mul_mul_self_of_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A] [CStarRing A]
  [inst_4 : NormedSpace ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A} (b : A),
  autoParam (0 ≤ a) CFC.norm_star_mul_mul_self_of_nonneg._auto_1 → ‖star b * a * b‖ = ‖CFC.sqrt a * b‖ ^ 2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} [inst_3 : Inhabited (γ k)],
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).get! k = (Option.map (f k) (m.get? k)).get!
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.natCast_inj : ∀ {m n : ℕ} {R : Type u_1} [inst : Semiring R] [CharZero R], ↑m = ↑n ↔ m = n
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.replaceHead.match_1.eq_2 : ∀ {ι : Type u_2} {M : ι → Type u_1} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → (x_2 : M x) → x_2 ≠ 1 → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x x_1 : ι) (x_2 : M x)
  (h : x_2 ≠ 1) (j k : ι) (w₁ : Monoid.CoprodI.NeWord M x j) (hne : j ≠ k) (w₂ : Monoid.CoprodI.NeWord M k x_1)
  (h_1 :
    (x : ι) →
      (x_3 : M x) →
        (h : x_3 ≠ 1) → (x_4 : M x) → (a : x_4 ≠ 1) → motive x x x_3 h (Monoid.CoprodI.NeWord.singleton x_4 a))
  (h_2 :
    (x x_3 : ι) →
      (x_4 : M x) →
        (h : x_4 ≠ 1) →
          (j k : ι) →
            (w₁ : Monoid.CoprodI.NeWord M x j) →
              (hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 x_4 h (w₁.append hne w₂)),
  (match x, x_1, x_2, h, w₁.append hne w₂ with
    | x, .(x), x_3, h, Monoid.CoprodI.NeWord.singleton x_4 a => h_1 x x_3 h x_4 a
    | x, x_3, x_4, h, w₁.append hne w₂ => h_2 x x_3 x_4 h j k w₁ hne w₂) =
    h_2 x x_1 x_2 h j k w₁ hne w₂
-- Mathlib.Topology.Category.Compactum
Compactum.cl_eq_closure : ∀ {X : Compactum} (A : Set X.A), Compactum.cl✝ A = closure A
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge.congr_simp : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) (v v_1 : ↑M.verts),
  v = v_1 → h.toEdge v = h.toEdge v_1
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- This prevents `ofMeasure x` being printed as `{ toMeasure := x }` by `delabStructureInstance`.
 -/
MeasureTheory.LevyProkhorov.delabOfMeasure : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyFlat.of_isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsRightAdjoint], CategoryTheory.RepresentablyFlat F
-- Mathlib.Data.Finset.Erase
Finset.erase_ne_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, s.erase a ≠ s ↔ a ∈ s
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- `0` has infinite radius of convergence  -/
FormalMultilinearSeries.zero_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  FormalMultilinearSeries.radius 0 = ⊤
-- Lean.Widget.InteractiveCode
Lean.Widget.instFromJsonDiffTag : Lean.FromJson Lean.Widget.DiffTag
-- Lean.Server.References
/-- Yields the first reference in `module` at `pos`.  -/
Lean.Server.References.findRange? : Lean.Server.References → Lean.Name → Lean.Lsp.Position → optParam Bool false → Option Lean.Lsp.Range
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_of_eq_of_le` -/
subset_of_eq_of_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LE α], a = b → b ⊆ c → a ⊆ c
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_equiv_triangle : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map (CategoryTheory.shiftShiftNeg X n).inv)
      (CategoryTheory.shiftNegShift ((CategoryTheory.shiftFunctor C n).obj X) n).hom =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C n).obj X)
-- Lean.DocString.Parser
/-- Are we in a link?  -/
Lean.Doc.Parser.InlineCtxt.inLink : Lean.Doc.Parser.InlineCtxt → Bool
-- Mathlib.GroupTheory.Perm.ViaEmbedding
Equiv.Perm.viaEmbeddingHom_apply : ∀ {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (ι : α ↪ β), (Equiv.Perm.viaEmbeddingHom ι) e = e.viaEmbedding ι
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.ofNat_ctorIdx : ∀ (x : Lean.Lsp.CompletionItemKind), Lean.Lsp.CompletionItemKind.ofNat x.ctorIdx = x
-- Lean.Meta.Tactic.Intro
/-- Similar to `Lean.Core.mkFreshUserName`, but takes into account the `tactic.hygienic` option value.
If `tactic.hygienic = true`, then fresh macro scopes are applied to `binderName`.
If not, then returns an (accessible) name based on `binderName` that is unused in the local context.
 -/
Lean.Meta.mkFreshBinderNameForTactic : Lean.Name → Lean.MetaM Lean.Name
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false_of_lt_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] (a b : α) (k₁ k₂ : ℤ),
  (k₂ + k₁).ble' 0 = true → a < b + ↑k₁ → (b < a + ↑k₂) = False
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLE.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero α] [PosSMulReflectLE α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → PosSMulReflectLE α β
-- Batteries.Control.Lemmas
ReaderT.run_tryCatchThe : ∀ {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [inst : MonadExceptOf ε m] (body : ReaderT ρ m α)
  (handler : ε → ReaderT ρ m α) (ctx : ρ),
  (tryCatchThe ε body handler).run ctx = tryCatchThe ε (body.run ctx) fun x => (handler x).run ctx
-- Init.Data.Vector.Lemmas
Vector.swapAt_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ} {x : α} (hi : i < n),
  (Vector.mk xs h).swapAt i x hi = ((xs.swapAt i x ⋯).1, Vector.mk (xs.swapAt i x ⋯).2 ⋯)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_int_lt_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, ↑n < x
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.nontrivial_iff_exists_ne_zero : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 0
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_right_iff : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b⁻¹ ↔ Commute a b
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.mk.injEq : ∀ (before after before_1 after_1 : Lean.Syntax),
  ({ before := before, after := after } = { before := before_1, after := after_1 }) =
    (before = before_1 ∧ after = after_1)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.coeFn_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g)
  (g0 : g 0 = 0) (f : ↥(MeasureTheory.Lp E p μ)), ↑↑(hg.compLp g0 f) =ᵐ[μ] g ∘ ↑↑f
-- Mathlib.Data.Multiset.Sort
Multiset.mem_sort : ∀ {α : Type u_1} {a : α} {s : Multiset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], a ∈ s.sort r ↔ a ∈ s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
Std.Tactic.BVDecide.BVPred.bitblast_aig_IsPrefix : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig),
  Std.Sat.AIG.IsPrefix aig.decls (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig.decls