mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Disjoint
Set.disjoint_iff_forall_ne : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.Array.MergeSort.merge.go_eq_listMerge : ∀ {α : Type u_1} {xs ys : Subarray α} {hxs : 0 < Std.Slice.size xs} {hys : 0 < Std.Slice.size ys} {le : α → α → Bool}
  {acc : Array α},
  (Array.MergeSort.Internal.merge.go✝ le xs ys hxs hys acc).toList =
    acc.toList ++ (Std.Slice.toList xs).merge (Std.Slice.toList ys) le
-- Mathlib.Data.Finset.Basic
Finset.filter_ne : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), {a ∈ s | b ≠ a} = s.erase b
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_extendOfLE_of_lt : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a < b), (P.extendOfLE ⋯).parts = insert (b \ a) P.parts
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveOn.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  IsIntegralCurveOn γ v s → ContinuousOn γ s
-- Mathlib.Analysis.Complex.Exponential
Real.exp_add : ∀ (x y : ℝ), Real.exp (x + y) = Real.exp x * Real.exp y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.homEquiv_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D} {X Y : C} {X' Y' : D}
  (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (f : X' ⟶ Y'),
  (CategoryTheory.Localization.Preadditive.homEquiv eX eY) f =
    CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.CategoryStruct.comp f eY.inv)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.Rel₃ : (m : Type w → Type w') →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [Std.Iterators.Productive α₁ m] →
            [Std.Iterators.Productive α₂ m] → Std.IterM m (β₁ × β₂) → Std.IterM m (β₁ × β₂) → Prop
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite : ∀ {w : ℕ} {a b : BitVec (w + 1)} {c : Bool}, (a == ~~~bif c then a else b) = (!c && a == ~~~b)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.mk.inj : ∀ {A : Type u_1} {B : Type u_2} {inst : NonUnitalNonAssocSemiring A} {inst_1 : Star A}
  {inst_2 : NonUnitalNonAssocSemiring B} {inst_3 : Star B} {toNonUnitalRingHom : A →ₙ+* B}
  {map_star' : ∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a)}
  {toNonUnitalRingHom_1 : A →ₙ+* B}
  {map_star'_1 : ∀ (a : A), toNonUnitalRingHom_1.toFun (star a) = star (toNonUnitalRingHom_1.toFun a)},
  { toNonUnitalRingHom := toNonUnitalRingHom, map_star' := map_star' } =
      { toNonUnitalRingHom := toNonUnitalRingHom_1, map_star' := map_star'_1 } →
    toNonUnitalRingHom = toNonUnitalRingHom_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The second projection functor `ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.π₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Init.Data.Int.Order
Int.mul_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare)
  (P : CategoryTheory.Functor Cᵒᵖ (Type v')), S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.toRingHom_eq_toRingHom : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), ↑f = ↑f
-- Lean.Parser.Command
Lean.Parser.Command.structImplicitBinder : Lean.Parser.Parser
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.iSupIndep_genWeightSpace' : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M],
  iSupIndep fun χ => LieModule.genWeightSpace M ⇑χ
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- The numerator of a fraction after clearing the denominators
of a `Finset`-indexed family of fractions.  -/
IsLocalizedModule.integerMultiple : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {M' : Type u_3} →
              [inst_3 : AddCommMonoid M'] →
                [inst_4 : Module R M'] →
                  (f : M →ₗ[R] M') → [IsLocalizedModule S f] → {ι : Type u_4} → (s : Finset ι) → (ι → M') → ↥s → M
-- Mathlib.Order.Atoms.Finite
Finite.to_isAtomic : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] [Finite α], IsAtomic α
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasStrictDerivAt c c' x → ∀ (d : 𝕜'), HasStrictDerivAt (fun x => c x / d) (c' / d) x
-- Init.Data.Ord.Basic
/-- Constructs a `BEq` instance from an `Ord` instance.
 -/
Ord.toBEq : {α : Type u_1} → Ord α → BEq α
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Additive version of `Prod.nnnorm_def'`.
Earlier, this name was used for the multiplicative version.  -/
Prod.nnnorm_def : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] (x : E × F),
  ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctorObj'_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D) (X : D),
  e.inverseFunctorObj'.inv.app X = CategoryTheory.CategoryStruct.id (e.inverse.obj X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  Std.DTreeMap.Raw.Const.unitOfList l cmp = Std.DTreeMap.Raw.Const.insertManyIfNewUnit ∅ l
-- Mathlib.Logic.Function.Basic
Function.invFun_comp : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β}, Function.Injective f → Function.invFun f ∘ f = id
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_pred : ∀ (q₁ q₂ : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (q₁.pred q₂) =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit0))
        (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit1)
          (Turing.TM2.Stmt.goto fun x => q₁.pred q₂))
        (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd (s.getD default))
          (Turing.TM2.Stmt.goto fun x => q₁)
          (Turing.PartrecToTM2.peek' Turing.PartrecToTM2.K'.main
            (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd (s.getD default))
              (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂)
              (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0)
                (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂))))))
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → 0 < r' → r' ≤ r → HasFPowerSeriesWithinOnBall f p s x r'
-- Mathlib.Analysis.Meromorphic.Complex
MeromorphicOn.Gamma : ∀ {s : Set ℂ}, MeromorphicOn Complex.Gamma s
-- Mathlib.Data.Nat.Prime.Defs
/-- This definition is faster in the virtual machine than `decidablePrime`,
but slower in the kernel.
 -/
Nat.decidablePrime' : (p : ℕ) → Decidable (Nat.Prime p)
-- Mathlib.Algebra.Category.ModuleCat.Semi
LinearEquiv.toModuleIsoₛ_hom : ∀ {R : Type u} [inst : Semiring R] {X₁ X₂ : Type v} {g₁ : AddCommMonoid X₁} {g₂ : AddCommMonoid X₂} {m₁ : Module R X₁}
  {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂), e.toModuleIsoₛ.hom = SemimoduleCat.ofHom ↑e
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.comm_trans_lTensor_trans_comm_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N ≃ₗ[R] P),
  TensorProduct.comm R N Q ≪≫ₗ LinearEquiv.lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = LinearEquiv.rTensor Q g
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCongr_trans : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} {γ₁ : Type u_13} {γ₂ : Type u_14} (e : α₁ ≃ β₁)
  (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂), (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)
-- Mathlib.Analysis.Convex.EGauge
/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.

This version assumes that `𝕜` is a nontrivially normed division ring.
See also `egauge_univ_pi` for when `s = univ`,
and `egauge_pi'` for a version with more choices of the technical assumptions.
 -/
egauge_pi : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [(nhdsWithin 0 {0}ᶜ).NeBot] {I : Set ι} {U : (i : ι) → Set (E i)},
  I.Finite → (∀ i ∈ I, Balanced 𝕜 (U i)) → ∀ (x : (i : ι) → E i), egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)
-- Mathlib.Algebra.MvPolynomial.Rename
/-- **Alias** of `MvPolynomial.rename_eq_aeval`. -/
MvPolynomial.rename_eq : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  MvPolynomial.rename f = MvPolynomial.aeval (MvPolynomial.X ∘ f)
-- Mathlib.Algebra.Algebra.Prod
AlgHom.snd_apply : ∀ (R : Type u_1) {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (a : A × B), (AlgHom.snd R A B) a = a.2
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- `NonarchAddGroupNormClass F α` states that `F` is a type of nonarchimedean norms on the
additive group `α`.

You should extend this class when you extend `NonarchAddGroupNorm`.  -/
NonarchAddGroupNormClass : (F : Type u_6) → (α : outParam (Type u_7)) → [AddGroup α] → [FunLike F α ℝ] → Prop
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.algebraMap_eval_C : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R) (n : ℤ),
  (algebraMap R R') (Polynomial.eval x (Polynomial.Chebyshev.C R n)) =
    Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.C R' n)
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.toEvalsTo : {σ : Type u_1} →
  {f : σ → Option σ} →
    {a : σ} → {b : Option σ} → {m : ℕ} → StateTransition.EvalsToInTime f a b m → StateTransition.EvalsTo f a b
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_upperSemicontinuous_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderTopology δ] {g : γ → δ}
  {f : α → γ}, Continuous g → UpperSemicontinuous f → Antitone g → LowerSemicontinuous (g ∘ f)
-- Mathlib.Algebra.Group.Pi.Basic
Function.comp_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero β] [inst_1 : Zero γ] (f : α → β) {g : β → γ},
  Function.Injective g → g 0 = 0 → (g ∘ f = 0 ↔ f = 0)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_nonpos`. -/
le_of_sub_nonpos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a - b ≤ 0 → a ≤ b
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for sets of compact convex sets.

If `F` is a set of compact convex sets in a vector space of finite dimension `d`, and any
`k ≤ d + 1` sets from `F` intersect nontrivially, then all sets from `F` intersect nontrivially.  -/
Convex.helly_theorem_set_compact' : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_6 : TopologicalSpace E] [T2Space E]
  {F : Set (Set E)},
  (∀ X ∈ F, Convex 𝕜 X) →
    (∀ X ∈ F, IsCompact X) →
      (∀ (G : Finset (Set E)), ↑G ⊆ F → G.card ≤ Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) → (⋂₀ F).Nonempty
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (ictx : Lean.Parser.InputContext) (stx : Lean.Syntax) (result? : Option Lean.Language.Lean.HeaderParsedState)
  (toSnapshot_1 : Lean.Language.Snapshot) (metaSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (ictx_1 : Lean.Parser.InputContext) (stx_1 : Lean.Syntax) (result?_1 : Option Lean.Language.Lean.HeaderParsedState),
  ({ toSnapshot := toSnapshot, metaSnap := metaSnap, ictx := ictx, stx := stx, result? := result? } =
      { toSnapshot := toSnapshot_1, metaSnap := metaSnap_1, ictx := ictx_1, stx := stx_1, result? := result?_1 }) =
    (toSnapshot = toSnapshot_1 ∧ metaSnap = metaSnap_1 ∧ ictx = ictx_1 ∧ stx = stx_1 ∧ result? = result?_1)
-- Mathlib.Tactic.FunProp.FunctionData
/-- Of the form `⇑f` i.e. missing argument.  -/
Mathlib.Meta.FunProp.MorApplication.underApplied : Mathlib.Meta.FunProp.MorApplication
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_right' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp (a + p) b = toIcoMod hp a b + p
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperHemicontinuousWithinAt_iff_frequently`. -/
UpperHemicontinuousWithinAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  UpperHemicontinuousWithinAt f s x →
    ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.Data.Finset.Image
Finset.filterMap_some : ∀ {α : Type u_1} {s : Finset α}, Finset.filterMap some s ⋯ = s
-- Mathlib.Analysis.Calculus.VectorField
/-- We have `[W, 0] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. Version within a set.  -/
VectorField.lieBracketWithin_zero_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {W : E → E} {s : Set E}, VectorField.lieBracketWithin 𝕜 W 0 s = 0
-- Mathlib.GroupTheory.HNNExtension
/-- the equivalence given by multiplication on the left by `t`  -/
HNNExtension.NormalWord.unitsSMulEquiv : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      ↥A ≃* ↥B →
        {d : HNNExtension.NormalWord.TransversalPair G A B} → HNNExtension.NormalWord d ≃ HNNExtension.NormalWord d
-- Mathlib.Algebra.Category.Grp.Zero
GrpCat.instHasZeroObject : CategoryTheory.Limits.HasZeroObject GrpCat
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.Info.fmtHover?.isAtomicFormat : Std.Format → Bool
-- Mathlib.Algebra.Group.Conj
IsAddConj.addConjugatesOf_eq : ∀ {α : Type u} [inst : AddMonoid α] {a b : α}, IsAddConj a b → addConjugatesOf a = addConjugatesOf b
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is an `AddMonoid` under pointwise operations if `α` is.  -/
Finset.addMonoid : {α : Type u_2} → [DecidableEq α] → [AddMonoid α] → AddMonoid (Finset α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a fallback : α},
  (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Init.Data.Array.Lemmas
Array.foldr_map_hom : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → Array.foldr f' (g a) (Array.map g xs) = g (Array.foldr f a xs)
-- Mathlib.Data.Fintype.Pi
Set.iUnion_cons : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → Set α) (s : Set α), Set.iUnion (Fin.cons s f) = s ∪ ⋃ i, f i
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.getKey k₁ h₁ = m.getKey k₂ ⋯
-- Mathlib.Topology.MetricSpace.Contracting
/-- Banach fixed-point theorem for maps contracting on a complete subset.  -/
ContractingWith.exists_fixedPoint' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α},
  IsComplete s →
    ∀ (hsf : Set.MapsTo f s s),
      ContractingWith K (Set.MapsTo.restrict f s s hsf) →
        ∀ {x : α},
          x ∈ s →
            edist x (f x) ≠ ⊤ →
              ∃ y ∈ s,
                Function.IsFixedPt f y ∧
                  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) ∧
                    ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.qExpansion_add`. -/
ModularFormClass.qExpansion_add : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f + ⇑g) = UpperHalfPlane.qExpansion h ⇑f + UpperHalfPlane.qExpansion h ⇑g
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- Transport a `HasColimitsOfShape` instance across an equivalence.  -/
CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor C D) [E.IsEquivalence]
  [CategoryTheory.Limits.HasColimitsOfShape J D], CategoryTheory.Limits.HasColimitsOfShape J C
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR_run_eq_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {n : ℕ} (l : { l // l.length = n }),
  List.MergeSort.Internal.mergeSortTR.run✝ le l = (↑l).mergeSort le
-- Mathlib.Order.PartialSups
partialSups_succ : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : LinearOrder ι] [inst_2 : LocallyFiniteOrderBot ι]
  [inst_3 : SuccOrder ι] (f : ι → α) (i : ι), (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)
-- Mathlib.Topology.TietzeExtension
/-- A class encoding the concept that a space satisfies the Tietze extension property.  -/
TietzeExtension : (Y : Type v) → [TopologicalSpace Y] → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ}, m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.of_smul : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (x : α) (y : β), FreeMonoid.of x • y = f x y
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.kernel_from_eq_kernel : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c)
  [inst_2 : CategoryTheory.Limits.HasKernels V] {i j : ι},
  c.Rel i j → CategoryTheory.Limits.kernelSubobject (C.dFrom i) = CategoryTheory.Limits.kernelSubobject (C.d i j)
-- Mathlib.Analysis.Complex.Tietze
unitInterval.instTietzeExtension : TietzeExtension ↑unitInterval
-- Mathlib.Order.CompactlyGenerated.Basic
iSupIndep.disjoint_biSup_biSup : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} [IsModularLattice α] {f : ι → α}
  {s t : Set ι}, iSupIndep f → Disjoint s t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_eq_prime_iff : ∀ {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)],
  Function.minimalPeriod f x = p ↔ Function.IsPeriodicPt f p x ∧ ¬Function.IsFixedPt f x
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid have subtraction.  -/
AddUnits.instSub : {α : Type u} → [inst : AddMonoid α] → Sub (AddUnits α)
-- Mathlib.Algebra.Divisibility.Basic
Dvd.elim_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} {P : Prop}, a ∣ b → (∀ (c : α), b = c * a → P) → P
-- Mathlib.Algebra.Module.TransferInstance
/-- Transfer `Module.IsTorsionFree` across an `Equiv`  -/
Equiv.moduleIsTorsionFree : ∀ (R : Type u_1) {α : Type u_2} {β : Type u_3} [inst : Semiring R] (e : α ≃ β) [inst_1 : AddCommMonoid β]
  [inst_2 : Module R β] [Module.IsTorsionFree R β],
  let this := e.addCommMonoid;
  have this_1 := Equiv.module R e;
  Module.IsTorsionFree R α
-- Mathlib.Order.Disjoint
Complementeds.instMin : {α : Type u_1} → [inst : DistribLattice α] → [inst_1 : BoundedOrder α] → Min (Complementeds α)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (β_ Z X).inv h) =
    CategoryTheory.CategoryStruct.comp (β_ Y X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) h)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_eq_self : ∀ {V : Type u_1} {G : SimpleGraph V} {s : Set (Sym2 V)}, G.deleteEdges s = G ↔ Disjoint G.edgeSet s
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X.natTrailingDegree = 1
-- Init.Data.Rat.Lemmas
Rat.intCast_ofNat : ∀ {a : ℕ}, ↑(OfNat.ofNat a) = OfNat.ofNat a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- a presentation of the sheaf of modules `M.over (X i)` for any `i : I`  -/
SheafOfModules.QuasicoherentData.presentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → (self : M.QuasicoherentData) → (i : self.I) → (M.over (self.X i)).Presentation