mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (a : CategoryTheory.Functor (C × D) E) (k : D) (j : C),
  ((CategoryTheory.Functor.curryingFlipEquiv.symm a).obj k).obj j = a.obj (j, k)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_map_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous (OnePoint.map f) ↔ Continuous f ∧ Filter.Tendsto f (Filter.coclosedCompact X) (Filter.coclosedCompact Y)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instTop : {K : Type u} → [inst : Field K] → Top (ValuationSubring K)
-- Mathlib.LinearAlgebra.Vandermonde
/-- We don't mark this as `@[simp]` because the RHS is not simp-nf,
and simplifying the RHS gives a bothersome `Nat` subtraction.  -/
Matrix.projVandermonde_apply : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {v w : Fin n → R} {i j : Fin n},
  Matrix.projVandermonde v w i j = v i ^ ↑j * w i ^ ↑j.rev
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.BitVec.eq_to_beq : ∀ {w : ℕ} (a b : BitVec w), (a = b) = ((a == b) = true)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.preimage_algebraMap : ∀ (S : Type u_1) {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : A},
  ⇑(algebraMap R S) ⁻¹' spectrum S a = spectrum R a
-- Lean.Meta.Tactic.Simp.Types
/-- The result of simplifying some expression `e`.  -/
Lean.Meta.Simp.Result : Type
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.domExtend_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {s : Set B} (e : Bundle.Pretrivialization F fun z => proj ↑z) [inst_2 : Nonempty (Z → F)],
  e.domExtend.target = e.target
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_eq_top : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  K.toSubmodule = ⊤ ↔ K = ⊤
-- Mathlib.Topology.Order.LeftRightLim
Monotone.le_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x ≤ y → f x ≤ Function.rightLim f y
-- Batteries.Data.Fin.Coding
Fin.decodePi.eq_def : ∀ {n : ℕ} (f : Fin n → ℕ) (x : Fin (Fin.prod f)),
  Fin.decodePi f x =
    match (motive := (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.prod f) → (i : Fin n) → Fin (f i)) n, f, x with
    | 0, x, x_1 => fun x_2 => nomatch x_2
    | n.succ, f, ⟨x, hx⟩ =>
      have h := ⋯;
      have this := ⋯;
      have t := Fin.decodePi (fun x => f x.succ) ⟨x / f 0, this⟩;
      fun x_1 =>
      match x_1 with
      | ⟨0, isLt⟩ => ⟨x % f 0, ⋯⟩
      | ⟨i.succ, hi⟩ => t ⟨i, ⋯⟩
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α], Set.Iio ⊤ = {⊤}ᶜ
-- Mathlib.Analysis.Normed.Group.Basic
/-- A group homomorphism from an `AddCommGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddCommGroup` structure on the domain.  -/
SeminormedAddCommGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : SeminormedAddGroup F] → [AddMonoidHomClass 𝓕 E F] → 𝓕 → SeminormedAddCommGroup E
-- Mathlib.Logic.Function.Basic
Function.Surjective.exists₃ : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
  Function.Surjective f → ∀ {p : β → β → β → Prop}, (∃ y₁ y₂ y₃, p y₁ y₂ y₃) ↔ ∃ x₁ x₂ x₃, p (f x₁) (f x₂) (f x₃)
-- Init.Data.String.Lemmas.Splits
/-- Given a position that splits `s` into `t₁` and `t₂ ++ t₃` with witness `h`, constructs a position
`h.rotateRight` that splits `s` into `t₁ ++ t₂` and `t₃`. Use `h.splits_rotateRight` for the witness
that `h.rotateRight` splits `s` as required.
 -/
String.Pos.Splits.rotateRight : {s : String} → {p : s.Pos} → {t₁ t₂ t₃ : String} → p.Splits t₁ (t₂ ++ t₃) → s.Pos
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The domain of the isomorphism  -/
CategoryTheory.WalkingIso.zero : CategoryTheory.WalkingIso
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of `Submodule.equivMapOfInjective`.
 -/
AffineSubspace.equivMapOfInjective : {𝕜 : Type u_1} →
  {V₁ : Type u_3} →
    {V₂ : Type u_5} →
      {P₁ : Type u_8} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V₁] →
              [inst_2 : NormedSpace 𝕜 V₁] →
                [inst_3 : PseudoMetricSpace P₁] →
                  [inst_4 : NormedAddTorsor V₁ P₁] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (E : AffineSubspace 𝕜 P₁) →
                              [inst_9 : Nonempty ↥E] →
                                (φ : P₁ →ᵃ[𝕜] P₂) → Function.Injective ⇑φ → ↥E ≃ᵃ[𝕜] ↥(AffineSubspace.map φ E)
-- Mathlib.Order.Category.Frm
Frm.instCategory : CategoryTheory.Category.{u, u + 1} Frm
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.preimage_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y),
  ⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)
-- Mathlib.Order.Atoms
instIsStronglyAtomicOfWellFoundedLT : ∀ {α : Type u_2} [inst : PartialOrder α] [WellFoundedLT α], IsStronglyAtomic α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_eq_self : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid N},
  S ≤ AddMonoidHom.mrange f → AddSubmonoid.map f (AddSubmonoid.comap f S) = S
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.single_apply : ∀ (R : Type u_1) [inst : Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] [inst_4 : DecidableEq ι] (i : ι),
  ⇑(ContinuousLinearMap.single R φ i) = Pi.single i
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.val.eq_1 : ∀ {M : Type u_1}, ArchimedeanOrder.val = Equiv.refl (ArchimedeanOrder M)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.postcompose`.

---

Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
 -/
CategoryTheory.Limits.Cones.postcompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (F ⟶ G) → CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_pow : ∀ (n : ℕ) (R θ : ℝ), circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)
-- Mathlib.Algebra.Order.Ring.Int
Nat.cast_natAbs : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ℤ), ↑n.natAbs = ↑|n|
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_inter : ∀ {α : Type u_1} (t s₁ s₂ s : Set α), t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
-- Mathlib.Algebra.Group.MinimalAxioms
Group.ofRightAxioms.eq_1 : ∀ {G : Type u} [inst : Mul G] [inst_1 : Inv G] [inst_2 : One G] (assoc : ∀ (a b c : G), a * b * c = a * (b * c))
  (mul_one : ∀ (a : G), a * 1 = a) (mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1),
  Group.ofRightAxioms assoc mul_one mul_inv_cancel =
    { toMul := inst, mul_assoc := assoc, toOne := inst_2, one_mul := ⋯, mul_one := mul_one, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, toInv := inst_1, div := DivInvMonoid.div', zpow := zpowRec, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₂' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (self : CategoryTheory.Abelian.SpectralObject C ι) (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2),
  (CategoryTheory.ComposableArrows.mk₂
      ((self.H n).map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Abelian.SpectralObject._proof_6
              CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_10
              CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_4).app
          D))
      ((self.H n).map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_8
              CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_6
              CategoryTheory.Abelian.SpectralObject._proof_4 CategoryTheory.Abelian.SpectralObject._proof_4).app
          D))).Exact
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_seven : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 7 → M), ∑ i, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6
-- Mathlib.Algebra.Lie.Killing
/-- **Alias** of `LieAlgebra.isKilling_of_equiv`.

---

Given a Killing Lie algebra `L`, if `L'` is isomorphic to `L`, then `L'` is Killing too.  -/
LieEquiv.isKilling : ∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L' : Type u_4}
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [LieAlgebra.IsKilling R L] (e : L ≃ₗ⁅R⁆ L'),
  LieAlgebra.IsKilling R L'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_fst : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (self : G.PullbackObjObj f₁ f₃),
  CategoryTheory.CategoryStruct.comp self.π self.fst = (G.map f₁.op).app X₃
-- Mathlib.Data.PSigma.Order
/-- The lexicographical linear order on a sigma type.  -/
PSigma.Lex.orderTop : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : OrderTop ι] → [inst_2 : (i : ι) → Preorder (α i)] → [OrderTop (α ⊤)] → OrderTop (Σₗ' (i : ι), α i)
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_fun_smul_eq_smul_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E]
  [BorelSpace E] {X : Ω → 𝕜} {Y : Ω → E},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ → ∫ (ω : Ω), X ω • Y ω ∂μ = (∫ (ω : Ω), X ω ∂μ) • ∫ (ω : Ω), Y ω ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).get! k = m₁.get! k
-- Mathlib.Tactic.Linter.UnusedTacticExtension
/-- `#show_kind tac` takes as input the syntax of a tactic and returns the `SyntaxNodeKind`
at the head of the tactic syntax tree.

The input syntax needs to parse, though it can be *extremely* elided.
For instance, to see the `SyntaxNodeKind` of the `refine` tactic, you could use
```lean
#show_kind refine _
```
The trailing underscore `_` makes the syntax valid, since `refine` expects something else.
 -/
Mathlib.Linter.UnusedTactic.«command#show_kind_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- The object part of the initial functor `ℕᵒᵖ ⥤ J`  -/
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj : (J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsCofiltered J] → ℕ → J
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_sub_const_fun : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (derivWithin fun x => f x - c) = derivWithin f
-- Mathlib.FieldTheory.Normal.Defs
/-- Restriction to a normal subfield as a group homomorphism  -/
AlgEquiv.restrictNormalHom : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      [inst_1 : Field K₁] →
        [inst_2 : Algebra F K₁] →
          (E : Type u_6) →
            [inst_3 : Field E] →
              [inst_4 : Algebra F E] →
                [inst_5 : Algebra E K₁] → [IsScalarTower F E K₁] → [Normal F E] → Gal(K₁/F) →* Gal(E/F)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_back!_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keysArray.back!
-- Mathlib.RingTheory.WittVector.Truncated
instInhabitedTruncatedWittVector : (p n : ℕ) → (R : Type u_2) → [Inhabited R] → Inhabited (TruncatedWittVector p n R)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The `MeasurableSpace α` instance on a `StandardBorelSpace` `α` is equal to
the Borel sets of `upgradeStandardBorel α`.  -/
eq_borel_upgradeStandardBorel : ∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α], inst = borel α
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  (s.toJordanDecomposition.posPart.singularPart μ).MutuallySingular (s.toJordanDecomposition.negPart.singularPart μ)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {w x : D} {y z : C} (f : w ⟶ x) (g : y ⟶ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x g)
        h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.zsmul_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f : X ⟶ G) (n : ℤ)
  (g : G ⟶ H) [CategoryTheory.IsAddMonHom g] {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (n • f) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (n • CategoryTheory.CategoryStruct.comp f g) h
-- Lean.Message
Lean.MessageSeverity.noConfusionType : Sort v✝ → Lean.MessageSeverity → Lean.MessageSeverity → Sort v✝
-- Aesop.Forward.State
Aesop.instBEqPatSubstSource.beq : Aesop.PatSubstSource → Aesop.PatSubstSource → Bool
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.index_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D)
  (I : S.shape.R), (S.index P).fst I = P.map I.r.g₁.op
-- Mathlib.GroupTheory.Order.Min
/-- The minimum order of a non-identity element. Also the minimum size of a nontrivial subgroup, see
`Monoid.le_minOrder_iff_forall_subgroup`. Returns `∞` if the monoid is torsion-free.  -/
Monoid.minOrder : (α : Type u_2) → [Monoid α] → ℕ∞
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_lt_toDFinsupp : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Multiset.toDFinsupp s < Multiset.toDFinsupp t ↔ s < t
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_add_erase : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (f : ι →₀ M), (fun₀ | a => f a) + Finsupp.erase a f = f
-- Mathlib.Analysis.Complex.Hadamard
/-- **Hadamard three-line theorem** (Variant in simpler terms): Let `f` be a
bounded function, continuous on the closed strip `re ⁻¹' [l, u]` and differentiable on open strip
`re ⁻¹' (l, u)`. If, for all `z.re = l`, `‖f z‖ ≤ a` for some `a ∈ ℝ` and, similarly, for all
`z.re = u`, `‖f z‖ ≤ b` for some `b ∈ ℝ` then for all `z` in the closed strip
`re ⁻¹' [l, u]` the inequality
`‖f(z)‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))`
holds.  -/
Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {z : ℂ} {a b l u : ℝ},
  l < u →
    z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u →
      DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip l u) →
        BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip l u) →
          (∀ z ∈ Complex.re ⁻¹' {l}, ‖f z‖ ≤ a) →
            (∀ z ∈ Complex.re ⁻¹' {u}, ‖f z‖ ≤ b) → ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
-- Mathlib.Data.Set.Function
Set.MapsTo.mono_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β}, Set.MapsTo f s t₁ → t₁ ⊆ t₂ → Set.MapsTo f s t₂
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_comap_eq_self_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Surjective ⇑f → ∀ (H : AddSubgroup N), AddSubgroup.map f (AddSubgroup.comap f H) = H
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.get! t.min! = t.min!
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Set.pairwise_pair_of_symm`. -/
Set.pairwise_pair_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} [Std.Symm r], {a, b}.Pairwise r ↔ a ≠ b → r a b
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
SemimoduleCat.Hom.Simps.hom : {R : Type u} → [inst : Semiring R] → (A B : SemimoduleCat R) → A.Hom B → ↑A →ₗ[R] ↑B
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_toLinearMap : ∀ {G : Type v} [inst : Monoid G] (X Y : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  (Representation.LinearizeMonoidal.μ X Y).toLinearMap = ↑(MonoidAlgebra.tensorEquiv k)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instMin.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  Submonoid.instMin = { min := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯, one_mem' := ⋯ } }
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mkCoconeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  (lift : (s : CategoryTheory.Limits.Cocone F) → t ⟶ s)
  (uniq : ∀ (s : CategoryTheory.Limits.Cocone F) (m : t ⟶ s), m = lift s),
  CategoryTheory.Limits.IsColimit.mkCoconeMorphism lift uniq = { desc := fun s => (lift s).hom, fac := ⋯, uniq := ⋯ }
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul'.eq_2 : ∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k_1 v p_2).mul' k = Int.Internal.Linear.Poly.add (k * k_1) v (p_2.mul' k)
-- Init.Data.Iterators.Consumers.Monadic.Total
/-- A wrapper around an iterator that provides strictly terminating consumers. See
`IterM.ensureTermination`.
 -/
Std.IterM.Total : {α : Type w} → (Type w → Type w') → Type w → Type w
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X') (F.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X' X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X' Y) h)
-- Lean.Elab.Match
/-- Generate equalities `h : discr = pattern` for discriminants annotated with `h :`.
We use these equalities to elaborate the right-hand-side of a `match` alternative.
 -/
Lean.Elab.Term.withEqs : {α : Type} →
  Array Lean.Elab.Term.Discr →
    List Lean.Meta.Match.Pattern → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.GroupTheory.OrderOfElement
/-- A nonempty idempotent subset of a finite cancellative additive monoid is a submonoid  -/
addSubmonoidOfIdempotent : {M : Type u_6} → [inst : AddLeftCancelMonoid M] → [Finite M] → (S : Set M) → S.Nonempty → S + S = S → AddSubmonoid M
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_isBase_iff : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A] {s : Set A},
  (AlgebraicIndependent.matroid R A).IsBase s ↔ IsTranscendenceBasis R Subtype.val
-- Mathlib.Analysis.Polynomial.CauchyBound
/-- Cauchy's bound on the roots of a given polynomial.
See `IsRoot.norm_lt_cauchyBound` for the proof that the roots satisfy this bound.
 -/
Polynomial.cauchyBound : {K : Type u_1} → [inst : NormedDivisionRing K] → Polynomial K → NNReal
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_inclusion : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) (a : ↥S),
  ↑((AddSubmonoid.inclusion h) a) = ↑a
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.dualProdIsometry_toFun : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] N) (a : Module.Dual R M × M),
  (QuadraticForm.dualProdIsometry f) a = (f.symm.dualMap.toAddEquiv.prodCongr f.toAddEquiv) a
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
/-- We say a root pairing is balanced if the root span and coroot span are perfectly
complementary.

All root systems are balanced and all finite root pairings over a field are balanced.  -/
RootPairing.IsBalanced : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : AddCommGroup M] →
          [inst_1 : AddCommGroup N] →
            [inst_2 : CommRing R] → [inst_3 : Module R M] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instSecondCountableTopology : SecondCountableTopology UpperHalfPlane