mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.GaugeRescale
/-- Given two convex bounded sets in a topological vector space with nonempty interiors,
there exists a homeomorphism of the ambient space
that sends the interior, the closure, and the frontier of one set
to the interior, the closure, and the frontier of the other set.

In particular, if both `s` and `t` are open set or both `s` and `t` are closed sets,
then `e` maps `s` to `t`.  -/
exists_homeomorph_image_eq : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] [T1Space E] {s t : Set E},
  Convex ℝ s →
    (interior s).Nonempty →
      Bornology.IsVonNBounded ℝ s →
        Convex ℝ t →
          (interior t).Nonempty →
            Bornology.IsVonNBounded ℝ t →
              ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t ∧ ⇑e '' frontier s = frontier t
-- Mathlib.LinearAlgebra.Contraction
/-- An inverse to `TensorProduct.dualDistrib` given bases.
 -/
TensorProduct.dualDistribInvOfBasis : {R : Type u_7} →
  {M : Type u_8} →
    {N : Type u_9} →
      {ι : Type u_10} →
        {κ : Type u_11} →
          [DecidableEq ι] →
            [DecidableEq κ] →
              [Fintype ι] →
                [Fintype κ] →
                  [inst : CommSemiring R] →
                    [inst_1 : AddCommMonoid M] →
                      [inst_2 : AddCommMonoid N] →
                        [inst_3 : Module R M] →
                          [inst_4 : Module R N] →
                            Module.Basis ι R M →
                              Module.Basis κ R N →
                                Module.Dual R (TensorProduct R M N) →ₗ[R]
                                  TensorProduct R (Module.Dual R M) (Module.Dual R N)
-- Init.Data.BitVec.Lemmas
BitVec.msb_or : ∀ {w : ℕ} {x y : BitVec w}, (x ||| y).msb = (x.msb || y.msb)
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_unitIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.Preadditive.commGrpEquivalence.unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Batteries.Data.Char.AsciiCasing
Char.toLower_eq_of_not_isUpper : ∀ {c : Char}, ¬c.isUpper = true → c.toLower = c
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_center_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⁅AddSubgroup.center G, H⁆ = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformlyOn.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], MultipliableUniformlyOn f s → ∃ g, HasProdUniformlyOn f g s
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubDuration : HSub Std.Time.Timestamp Std.Time.Duration Std.Time.Timestamp
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.bind₁_frobeniusPolyRat_wittPolynomial : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.bind₁ (WittVector.frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)
-- Std.Sync.CancellationContext
/-- Waits for cancellation. Returns a task that completes when the context is cancelled.
 -/
Std.CancellationContext.done : Std.CancellationContext → IO (Std.Async.AsyncTask Unit)
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.smul : {G : Type u_1} → {α : Type u_3} → {β : Type u_4} → [inst : Group G] → [MulAction G β] → SMul G (α ↪ β)
-- Mathlib.Analysis.Calculus.FDeriv.Star
DifferentiableOn.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {s : Set E} [TrivialStar 𝕜],
  DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun y => star (f y)) s
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {f : ι → M → G},
  (LocallyFinite fun i => Function.support (f i)) →
    ∀ {x₀ : M},
      (∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∑ᶠ (i : ι), f i x) s x₀
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.mclosure_iUnion_range_of : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)],
  Submonoid.closure (⋃ i, Set.range ⇑Monoid.CoprodI.of) = ⊤
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.inf` -/
MeasureTheory.AEStronglyMeasurable.fun_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : SemilatticeInf β] [ContinuousInf β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i ⊓ g i) μ
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.add.injEq : ∀ (e : Lean.Expr) (k : ℕ) (e_1 : Lean.Expr) (k_1 : ℕ),
  (Lean.Meta.Sym.Offset.add e k = Lean.Meta.Sym.Offset.add e_1 k_1) = (e = e_1 ∧ k = k_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.coe_toPartialEquiv_symm`. -/
OpenPartialHomeomorph.coe_coe_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.symm = ↑e.symm
-- Init.Data.List.Perm
List.Perm.refl : ∀ {α : Type u_1} (l : List α), l.Perm l
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
the distance between `x` and `y`.  -/
Metric.infDist_le_infDist_add_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α}, Metric.infDist x s ≤ Metric.infDist y s + dist x y
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The volume measure in a finite-dimensional inner product space gives measure `1` to the
parallelepiped spanned by any orthonormal basis.  -/
OrthonormalBasis.volume_parallelepiped : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F]
  (b : OrthonormalBasis ι ℝ F), MeasureTheory.volume (parallelepiped ⇑b) = 1
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.denseRange : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → DenseRange Subtype.val
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNormedAddCommGroup : {α : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] →
        [inst_2 : Zero α] → [inst_3 : NormedAddCommGroup R] → NormedAddCommGroup (ContinuousMapZero α R)
-- Lean.Parser.Command
Lean.Parser.Command.namedPrio.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Free
FreeSemigroup.instLawfulMonad : LawfulMonad FreeSemigroup
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.id_indexEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (a : ι),
  (↑(RootPairing.Equiv.id P)).indexEquiv a = a
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.Hom.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2) (a : C)
  (x : CategoryTheory.WithInitial C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithInitial.of X) (CategoryTheory.WithInitial.of Y))
  (h_2 : (a : C) → (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of a) x)
  (h_3 : (x : CategoryTheory.WithInitial C) → motive CategoryTheory.WithInitial.star x),
  (∀ (Y : C), x = CategoryTheory.WithInitial.of Y → False) →
    (match CategoryTheory.WithInitial.of a, x with
      | CategoryTheory.WithInitial.of X, CategoryTheory.WithInitial.of Y => h_1 X Y
      | CategoryTheory.WithInitial.of a, x => h_2 a x
      | CategoryTheory.WithInitial.star, x => h_3 x) =
      h_2 a x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f (t.get? k)).isNone)
-- Mathlib.Algebra.Ring.Defs
/-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`.  -/
Ring.intCast_ofNat : ∀ {R : Type u} [self : Ring R] (n : ℕ), IntCast.intCast ↑n = ↑n
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andLeft.sizeOf_spec : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.andLeft ak p) = 1 + sizeOf ak + sizeOf p
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_add : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv),
  CauSeq.Completion.mk f + CauSeq.Completion.mk g = CauSeq.Completion.mk (f + g)
-- Aesop.Forward.Match.Types
Aesop.instEmptyCollectionCompleteMatch : EmptyCollection Aesop.CompleteMatch
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_algebraMap_inv_atTop_nhds_zero_nat : ∀ {𝕜 : Type u_4} (A : Type u_5) [inst : Semifield 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [ContinuousSMul ℚ≥0 𝕜] [inst_4 : Semiring A] [inst_5 : Algebra 𝕜 A] [inst_6 : TopologicalSpace A]
  [ContinuousSMul 𝕜 A], Filter.Tendsto (⇑(algebraMap 𝕜 A) ∘ fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
-- Aesop.RuleTac.RuleTerm
Aesop.instToMessageDataRuleTerm : Lean.ToMessageData Aesop.RuleTerm
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_obj_obj_σ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)),
  (((CategoryTheory.SimplicialObject.whiskering C D).obj F).obj X).σ i = F.map (X.σ i)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} {U : Set α} {h : IsOpen U},
  x ∈ { carrier := U, is_open' := h } ↔ x ∈ U
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_sup : ∀ {N : Type u_4} [inst : AddCommMonoid N] {s t : AddSubmonoid N} {x : N}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
-- Mathlib.Topology.Algebra.Module.Complement
/-- Two complementary submodules are topological complements if and only if the linear equivalence
`Submodule.quotientEquivOfIsCompl` is continuous.  -/
Submodule.IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ Continuous ⇑(p.quotientEquivOfIsCompl q h)
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.NatTrans.commShift_op : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {F G : CategoryTheory.Functor C D}
  [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] (τ : F ⟶ G) [CategoryTheory.NatTrans.CommShift τ A],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.OppositeShift.natTrans A τ) A
-- Mathlib.Topology.Algebra.Group.Basic
continuousInv_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Inv H] [IndiscreteTopology H], ContinuousInv H
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_id : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R], MvPowerSeries.rename id = AlgHom.id R (MvPowerSeries σ R)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.groupObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) (j : J),
  GrpCat.groupObj F j =
    { toMul := GrpCat.groupObj._aux_1 F j, mul_assoc := ⋯, toOne := GrpCat.groupObj._aux_4 F j, one_mul := ⋯,
      mul_one := ⋯, toNPow := GrpCat.groupObj._aux_8 F j, npow_zero := ⋯, npow_succ := ⋯,
      toInv := GrpCat.groupObj._aux_12 F j, toDiv := GrpCat.groupObj._aux_14 F j, toZPow := GrpCat.groupObj._aux_16 F j,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
NNReal.nnrpow_def : ∀ (a b : NNReal), a.nnrpow b = a ^ ↑b
-- Mathlib.Data.NNRat.Defs
NNRat.val_eq_cast : ∀ (q : ℚ≥0), ↑q = ↑q
-- 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`.
- `w a = 1`.

Then there is a common divergent point `k` 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_eq_one : ∀ {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) →
      w a = 1 → 1 < (v i) b → w b < 1 → ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn.go : {motive_1 : ProofWidgets.Html → Sort u} →
  {motive_2 : Array ProofWidgets.Html → Sort u} →
    {motive_3 : List ProofWidgets.Html → Sort u} →
      (t : ProofWidgets.Html) →
        ((t : ProofWidgets.Html) → t.below → motive_1 t) →
          ((t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t) →
            ((t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_le_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {a b : R},
  (IsDiscreteValuationRing.addVal R) a ≤ (IsDiscreteValuationRing.addVal R) b ↔ a ∣ b
-- Mathlib.Tactic.Translate.Reorder
/-- Permute a list of either universe levels or universe parameters.  -/
Mathlib.Tactic.Translate.Permutation.permuteList! : {α : Type u_1} → [Inhabited α] → Mathlib.Tactic.Translate.Permutation → List α → List α
-- Mathlib.Tactic.Choose
/-- Parsed information from a `choose` argument, which may include a type annotation.  -/
Mathlib.Tactic.Choose.ChooseArg : Type
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- `(0)` is a sub-dp-ideal of the dp-ideal `I`.  -/
DividedPowers.SubDPIdeal.instBot : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Bot hI.SubDPIdeal
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgHom_id : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], MonoidAlgebra.mapAlgHom M (AlgHom.id R A) = AlgHom.id R (MonoidAlgebra A M)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkTrans' : Option Lean.Expr → Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_pred_iff_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  ¬IsMin b → ¬IsMin a → (Order.pred b ≤ Order.pred a ↔ b ≤ a)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_orderTop : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ),
  (AddOpposite.unop (HahnSeries.addOppositeEquiv x)).orderTop = x.orderTop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : β → β},
      (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), Int.fract a + ↑⌊a⌋ = a
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCategory.eq_1 : CommMonCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @CommMonCat.instCategory._proof_1,
    comp_id := @CommMonCat.instCategory._proof_2, assoc := @CommMonCat.instCategory._proof_3 }
-- Mathlib.Order.SymmDiff
Codisjoint.bihimp_eq_inf : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → bihimp a b = a ⊓ b
-- Mathlib.Algebra.DirectSum.Basic
_private.Mathlib.Algebra.DirectSum.Basic.0.DFinsupp.extendWith.match_1.eq_1 : ∀ {ι : Type u_1} (motive : Option ι → Sort u_2) (h_1 : Unit → motive none) (h_2 : (val : ι) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some val => h_2 val) =
    h_1 ()
-- Mathlib.Data.WSeq.Basic
/-- Get the head of a weak sequence. This involves a possibly
infinite computation.  -/
Stream'.WSeq.head : {α : Type u} → Stream'.WSeq α → Computation (Option α)
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_singleton_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).ncard = s.ncard - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- If `f,g` is coreflexive, then `g,f` is coreflexive.  -/
CategoryTheory.IsCoreflexivePair.swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} [CategoryTheory.IsCoreflexivePair f g],
  CategoryTheory.IsCoreflexivePair g f
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_product'`  -/
Finset.sum_product : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β),
  ∑ x ∈ s ×ˢ t, f x = ∑ x ∈ s, ∑ y ∈ t, f (x, y)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.subsingleton_indep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} [M.Loopless],
  I.Subsingleton → autoParam (I ⊆ M.E) Matroid.subsingleton_indep._auto_1 → M.Indep I
-- Mathlib.Data.Sum.Basic
Sum.map_injective : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ},
  Function.Injective (Sum.map f g) ↔ Function.Injective f ∧ Function.Injective g
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.nsmul_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} (n : ℕ), a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p]
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.leftCompReflexion_eq : CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion =
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.left
    CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux : ∀ {H : Type u_1} {H' : Type u_3} {M' : Type u_4} {X : Type u_5} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace H'] [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H' M']
  [inst_4 : TopologicalSpace X] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : OpenPartialHomeomorph M' H'}
  {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {g : X → M'} {e : OpenPartialHomeomorph X H} {x : X} {s : Set X},
      x ∈ e.source →
        f ∈ StructureGroupoid.maximalAtlas M' G' →
          g x ∈ f.source →
            ContinuousWithinAt g s x →
              (P (↑(chartAt H' (g x)) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
                P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Init.Data.Rat.Lemmas
Rat.den_inv : ∀ (a : ℚ), a⁻¹.den = if a.num = 0 then 1 else a.num.natAbs
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteMulSupport.pow` -/
Function.HasFiniteMulSupport.fun_pow : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] {f : α → M},
  Function.HasFiniteMulSupport f → ∀ (n : ℕ), Function.HasFiniteMulSupport fun i => f i ^ n
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_ker : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} [inst_1 : Group G'] (f : G →* G') [Finite ↥f.range], f.ker.FiniteIndex
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoApp M).hom.hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- If `x` is a root of an irreducible polynomial `p`, then `x` is integral
iff the leading coefficient of `p` is a unit.  -/
minpoly.IsIntegrallyClosed.isIntegral_iff_isUnit_leadingCoeff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {x : S} {p : Polynomial R},
  Irreducible p → (Polynomial.aeval x) p = 0 → (IsIntegral R x ↔ IsUnit p.leadingCoeff)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_of_notMem_closure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, x ∉ closure s → ContinuousWithinAt f s x
-- Std.Data.HashMap.Raw
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.HashMap.Raw.insertMany : {α : Type u} →
  {β : Type v} →
    [BEq α] → [Hashable α] → {ρ : Type w} → [ForIn Id ρ (α × β)] → Std.HashMap.Raw α β → ρ → Std.HashMap.Raw α β
-- Mathlib.GroupTheory.Congruence.Defs
/-- The coercion to the quotient of an additive congruence relation
commutes with addition (by definition).  -/
AddCon.coe_add : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M} (x y : M), ↑(x + y) = ↑x + ↑y
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.maxHeartbeats : Lean.Meta.SynthInstance.Context → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_even_cos : ∀ (n : ℕ), iteratedDeriv (2 * n) Complex.cos = (-1) ^ n * Complex.cos