mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Slope
isSeparable_range_derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [TopologicalSpace.SeparableSpace 𝕜] (f : 𝕜 → F) (s : Set 𝕜),
  TopologicalSpace.IsSeparable (Set.range (derivWithin f s))
-- Mathlib.Topology.Separation.SeparatedNhds
/-- `SeparatedNhds` is a predicate on pairs of sub`Set`s of a topological space.  It holds if the two
sub`Set`s are contained in disjoint open sets.
 -/
SeparatedNhds : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X → Prop
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.noncommProd_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G}
  (comm : (↑t).Pairwise (Function.onFun Commute f)), (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K
-- Batteries.Recycling.RBTree.Alter
/-- The `alter` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.alter : ∀ {α : Type u_1} {cut : α → Ordering} {f : Option α → Option α} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  (∀ {x : α} {t' : RBTree.RBNode α} {p : RBTree.RBNode.Path α},
      RBTree.RBNode.zoom cut t = (t', p) →
        f t'.root? = some x →
          RBTree.RBNode.Path.RootOrdered cmp p x ∧ RBTree.RBNode.OnRoot (RBTree.RBNode.cmpEq cmp x) t') →
    RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.alter cut f t)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_eq_sub_fract_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p
-- Mathlib.Data.Sym.NatCard
/-- A version of `card_sym_eq_choose` that does not need finiteness.  -/
Sym.natCard_sym_eq_choose : ∀ (α : Type u_1) (k : ℕ), Nat.card (Sym α k) = (Nat.card α + k - 1).choose k
-- Mathlib.Condensed.Discrete.Module
Condensed.discrete.congr_simp : ∀ (C : Type w) [inst : CategoryTheory.Category.{u + 1, w} C]
  [inst_1 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C],
  Condensed.discrete C = Condensed.discrete C
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
ofMul_image_zpowers_eq_zmultiples_ofMul : ∀ {G : Type u_1} [inst : Group G] {x : G},
  ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isAddInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Order.Max
IsMin.prodMk : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMin a → IsMin b → IsMin (a, b)
-- Mathlib.Data.Seq.Computation
Computation.map_pure : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Computation.map f (Computation.pure a) = Computation.pure (f a)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- A function `f` that approximates a linear equivalence on the whole space is a homeomorphism.  -/
ApproximatesLinearOn.toHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                (f : E → F) →
                  {f' : E ≃L[𝕜] F} →
                    {c : NNReal} →
                      [CompleteSpace E] →
                        ApproximatesLinearOn f (↑f') Set.univ c → Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → E ≃ₜ F
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_eq_const : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  {f : α → ENNReal} {c : ENNReal}, (∀ᵐ (x : α) ∂μ, f x = c) → ∫⁻ (x : α), f x ∂μ = c
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.arrowCongrLeft_refl : ∀ {α : Sort u} {γ : Sort w} [inst : Inhabited γ],
  (Function.Embedding.refl α).arrowCongrLeft = Function.Embedding.refl (α → γ)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k} {w : k ∈ m}, m.get k w = v → k ∈ m
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Definition of the trailing coefficient in case where `f` is meromorphic and a presentation of the
form `f = (z - x) ^ order • g z` is given, with `g` analytic at `x`.
 -/
AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜},
  AnalyticAt 𝕜 g x →
    (f =ᶠ[nhdsWithin x {x}ᶜ] fun z => (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) →
      meromorphicTrailingCoeffAt f x = g x
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Affine equivalences preserve affine independence of subsets.  -/
AffineEquiv.affineIndependent_set_of_eq_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] {s : Set P} (e : P ≃ᵃ[k] P₂),
  AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset : HSub Std.Time.Timestamp Std.Time.Day.Offset Std.Time.Timestamp
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
/-- The category of radicals on `C`, defined as the full subcategory of
`Preradical C` consisting of preradicals `Φ` such that `toColon Φ Φ` is an isomorphism.  -/
CategoryTheory.Abelian.Radical : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Abelian C] → Type (max u_1 v_1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.exists_finset_of_mem_supr' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type u_3}
  {f : ι → IntermediateField F E} {x : E}, x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯
-- Mathlib.NumberTheory.Height.Basic
_private.Mathlib.NumberTheory.Height.Basic.0.Height.max_eq_iSup : ∀ {α : Type u_5} [inst : ConditionallyCompleteLattice α] (a b : α), a ⊔ b = iSup ![a, b]
-- Mathlib.Tactic.Find
Mathlib.Tactic.Find.findType : Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.brecOn : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  {a a_1 : CommRingCat.Colimits.Prequotient F} (t : CommRingCat.Colimits.Relation F a a_1),
  (∀ (a a_2 : CommRingCat.Colimits.Prequotient F) (t : CommRingCat.Colimits.Relation F a a_2),
      CommRingCat.Colimits.Relation.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.Array.Lemmas
Array.foldl_map_hom' : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} {stop : ℕ},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) →
    stop = xs.size → Array.foldl f' (g a) (Array.map g xs) 0 stop = g (Array.foldl f a xs)
-- Mathlib.Algebra.Group.End
MulAut.mul_apply : ∀ (M : Type u_2) [inst : Mul M] (e₁ e₂ : MulAut M) (m : M), (e₁ * e₂) m = e₁ (e₂ m)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (f f_1 : M.X ⟶ N.X) (e_f : f = f_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Mon.Hom.mk' f one_f mul_f = CategoryTheory.Mon.Hom.mk' f_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product) when `N` is normal.  -/
Subgroup.mul_normal : ∀ {G : Type u_2} [inst : Group G] (H N : Subgroup G) [hN : N.Normal], ↑(H ⊔ N) = ↑H * ↑N
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Construct an object of the category `(F ↓ Δ)` from a cocone on `F`. This is part of an
equivalence, see `Cocone.equivStructuredArrow`.  -/
CategoryTheory.Limits.Cocone.toStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Functor (CategoryTheory.Limits.Cocone F)
            (CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J))
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.coe_fourierTransform : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)), ⇑(Real.Lp.fourierTransform f) = FourierTransform.fourier ↑↑f
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_abs : ∀ {w i : ℕ} {x : BitVec w}, x.abs.getLsbD i = if x.msb = true then (-x).getLsbD i else x.getLsbD i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- Extension for `Real.cos (Real.arctan _)`.  -/
Mathlib.Meta.Positivity.evalRealCosArctan : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.decidableLE : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : IsOrderedCancelMonoid α] → {s : Submonoid α} → [DecidableLE α] → DecidableLE (Localization s)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.vadd_eq_vadd_of_subset : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X} {g₁ g₂ : G},
  AddAction.IsBlock G B → g₁ +ᵥ B ⊆ g₂ +ᵥ B → g₁ +ᵥ B = g₂ +ᵥ B
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
/-- If `X` is a simplicial object and `n + i = m`, this is the morphism
`X _⦋m⦌ ⟶ X _⦋n⦌` obtained by iterating `i` times the face map `X.δ 0`.  -/
CategoryTheory.SimplicialObject.δ₀Iter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n m : ℕ} →
        (i : ℕ) →
          autoParam (n + i = m) CategoryTheory.SimplicialObject.δ₀Iter._auto_1 →
            (X.obj (Opposite.op { len := m }) ⟶ X.obj (Opposite.op { len := n }))
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.degree_optionEquivLeft : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] {f : MvPolynomial (Option σ) R},
  f ≠ 0 → ((MvPolynomial.optionEquivLeft R σ) f).degree = ↑(MvPolynomial.degreeOf none f)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_sub_right : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (v₁ v₂ : V), midpoint R v₁ v₂ - v₂ = ⅟2 • (v₁ - v₂)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv (K.homologyπ j) =
    CategoryTheory.CategoryStruct.id (K.homology j)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_ofSliceTo_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  q < String.Slice.Pos.ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h < p
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- Suppose that
- `v i` and `w` are absolute values on a field `R`.
- `v i` is inequivalent to `v j` for all `j ≠ i` via the divergent point `a : R`.
- `v i` is inequivalent to `w` via the divergent point `b : R`.
- `1 < w a`.

Then there is a common divergent point `k : R` causing both `v i` and `w` to be inequivalent to
each `v j` for `j ≠ i`.
 -/
_private.Mathlib.Analysis.AbsoluteValue.Equivalence.0.AbsoluteValue.exists_one_lt_lt_one_pi_of_one_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Field S] [inst_2 : LinearOrder S]
  [inst_3 : TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [OrderTopology S] {ι : Type u_3} [Finite ι]
  {v : ι → AbsoluteValue R S} {w : AbsoluteValue R S} {a b : R} {i : ι},
  1 < (v i) a →
    (∀ (j : ι), j ≠ i → (v j) a < 1) →
      1 < w a → 1 < (v i) b → w b < 1 → ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.nonempty : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WSameSide x y → (↑s).Nonempty
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalCommRing : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalCommRing β] → NonUnitalCommRing (α →₀ β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List α} {k fallback : α},
  l.contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKeyD k fallback =
      fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  k' ∈ Std.DTreeMap.Const.alter t k f ↔
    if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).isSome = true else k' ∈ t
-- Mathlib.Data.Finset.Sups
Finset.compls_union : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ∪ t).compls = s.compls ∪ t.compls
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.val_neg_inj : ∀ {α : Type u} [inst : AddMonoid α] {u₁ u₂ : AddUnits α}, ↑(-u₁) = ↑(-u₂) ↔ ↑u₁ = ↑u₂
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_469✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_471✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_473✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_475✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_477✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 1 = app₁
-- Mathlib.Topology.Irreducible
/-- If `∅ ≠ U ⊆ S ⊆ t` such that `U` is open and `t` is preirreducible, then `S` is irreducible.  -/
IsPreirreducible.subset_irreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t S U : Set X},
  IsPreirreducible t → U.Nonempty → IsOpen U → U ⊆ S → S ⊆ t → IsIrreducible S
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToStringTextDocumentPositionParams : ToString Lean.Lsp.TextDocumentPositionParams
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k k' : α} {f : β → β},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.modify t k f) k' =
        if cmp k k' = Ordering.eq then Option.map f (Std.DTreeMap.Raw.Const.get? t k)
        else Std.DTreeMap.Raw.Const.get? t k'
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- Transport the property of being Cartesian closed across an equivalence of categories.

Note we didn't require any coherence between the choice of finite products here, since we transport
along the `prodComparison` isomorphism.
 -/
CategoryTheory.cartesianClosedOfEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (C ≌ D) → [CategoryTheory.MonoidalClosed C] → CategoryTheory.MonoidalClosed D
-- Mathlib.Data.Real.Embedding
/-- The bundled `M →+o ℝ` for archimedean `M` that preserves `1`.  -/
Archimedean.embedReal : (M : Type u_1) →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [IsOrderedAddMonoid M] → [inst_3 : One M] → [ZeroLEOneClass M] → [NeZero 1] → [Archimedean M] → M →+o ℝ
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableWithinAt.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G},
  DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₂ x).2) s x
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.of_isEmpty : ∀ {α : Type v} [inst : LinearOrder α] [IsEmpty α] {s : Set α}, IsClub s
-- Mathlib.Data.EReal.Operations
EReal.sub_lt_iff : ∀ {a b c : EReal}, b ≠ ⊥ ∨ c ≠ ⊥ → b ≠ ⊤ ∨ c ≠ ⊤ → (c - b < a ↔ c < a + b)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A block matrix is invertible if the bottom right corner and the corresponding Schur complement
is.  -/
Matrix.fromBlocks₂₂Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible D] → [Invertible (A - B * ⅟D * C)] → Invertible (Matrix.fromBlocks A B C D)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_comp_inv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv))
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
-- Mathlib.Data.LawfulXor.Basic
xor_left_eq_id_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a : α}, (fun x => a ^^^ x) = id ↔ a = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setZetaDeltaSet : Lean.Meta.Simp.Context → Lean.FVarIdSet → Lean.FVarIdSet → Lean.Meta.Simp.Context
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M],
  IsNoetherian A (TensorProduct R A M) → IsNoetherian R M
-- Mathlib.Data.Bool.Basic
Bool.and_le_left : ∀ (x y : Bool), (x && y) ≤ x
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom (TypeCat.ofHom Prod.fst) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- `AEEqFun.toGerm` as an `AddMonoidHom`.  -/
MeasureTheory.AEEqFun.toGermAddMonoidHom : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : AddMonoid γ] → [inst_3 : ContinuousAdd γ] → (α →ₘ[μ] γ) →+ (MeasureTheory.ae μ).Germ γ
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.mk.inj : ∀ {fvarIds : Array Lean.FVarId} {zetaDeltaAll : Bool} {fvarIds_1 : Array Lean.FVarId} {zetaDeltaAll_1 : Bool},
  { fvarIds := fvarIds, zetaDeltaAll := zetaDeltaAll } = { fvarIds := fvarIds_1, zetaDeltaAll := zetaDeltaAll_1 } →
    fvarIds = fvarIds_1 ∧ zetaDeltaAll = zetaDeltaAll_1
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀] [FaithfulSMul R₀ R] [inst_10 : Fintype σ],
  ∑ i, P.jacobianRelationsOfHasCoeffs R₀ i * Algebra.Presentation.relationOfHasCoeffs R₀ i =
    P.jacobianOfHasCoeffs R₀ * P.invJacobianOfHasCoeffs R₀ - 1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inl_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.fst X Y) =
    CategoryTheory.CategoryStruct.id X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, Std.ExtDTreeMap.Const.get! t a = Std.ExtDTreeMap.Const.getD t a default
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_setOfPred_Odd : schnirelmannDensity (Set.ofPred Odd) = 2⁻¹
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E'), MDiff ⇑f
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit_obj_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  {H : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {k : K} {W : C} {f g : W ⟶ (CategoryTheory.Limits.limit H).obj k},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Limits.limit.π H j).app k) =
        CategoryTheory.CategoryStruct.comp g ((CategoryTheory.Limits.limit.π H j).app k)) →
    f = g