mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.integrable_indicator : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasurableSet s → MeasureTheory.Integrable (s.indicator f) μ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k : α} {f : β → β}
  {hc : (Std.DHashMap.Internal.Raw₀.Const.modify m k f).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k hc =
    f (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The kernel of `biproduct.toSubtype f p` is `⨁ Subtype.restrict pᶜ f`.  -/
CategoryTheory.Limits.kernelBiproductToSubtypeIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : Type} →
        [inst_2 : Finite K] →
          [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            (f : K → C) →
              (p : K → Prop) →
                CategoryTheory.Limits.kernel (CategoryTheory.Limits.biproduct.toSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ {f : α → E},
        (∀ (g : G) (x : α), f (g +ᵥ x) = f x) →
          (MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P ≈ Q → (W'.Nonsingular P ↔ W'.Nonsingular Q)
-- Mathlib.Analysis.Convex.Visible
/-- One cannot see any point in the interior of a set.  -/
IsVisible.eq_of_mem_interior : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] {s : Set V} {x y : V} [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V],
  IsVisible 𝕜 s x y → y ∈ interior s → x = y
-- Mathlib.Logic.Function.Basic
Function.instIsStrictTotalOrderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsStrictTotalOrder α r], IsStrictTotalOrder α (Function.swap r)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Associativity of the `L^p` product as an isometric equivalence.  -/
IsometryEquiv.withLpProdAssoc : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      (γ : Type u_4) →
        [hp : Fact (1 ≤ p)] →
          [inst : PseudoEMetricSpace α] →
            [inst_1 : PseudoEMetricSpace β] →
              [inst_2 : PseudoEMetricSpace γ] → WithLp p (WithLp p (α × β) × γ) ≃ᵢ WithLp p (α × WithLp p (β × γ))
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)]
  (g : CategoryTheory.CostructuredArrow L Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F) g) h.isoColimit.inv =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      ((CategoryTheory.StructuredArrow.right E).map g.hom)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Left unitor for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Lax.OplaxTrans.leftUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.var.inj : ∀ {i i_1 : Lean.Grind.CommRing.Var}, Lean.Grind.CommRing.Expr.var i = Lean.Grind.CommRing.Expr.var i_1 → i = i_1
-- Mathlib.Order.Filter.Prod
/-- If a function tends to a product `g ×ˢ h` of filters, then its second component tends to
`h`. See also `Filter.Tendsto.snd_nhds` for the special case of converging to a point in a
product of two topological spaces.  -/
Filter.Tendsto.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → β × γ},
  Filter.Tendsto m f (g ×ˢ h) → Filter.Tendsto (fun a => (m a).2) f h
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.instEpiCommRingCatToTotalQuotientPresheaf : ∀ {X : TopCat} (F : TopCat.Presheaf CommRingCat X), CategoryTheory.Epi F.toTotalQuotientPresheaf
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a right homology data for `S₁` induces a right homology data for `S₂` with
the same `Q` and `H` fields. This is obtained by dualising `LeftHomologyData.ofEpiOfIsIsoOfMono'`.
The inverse construction is `ofEpiOfIsIsoOfMono'`.  -/
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₁.RightHomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₂.RightHomologyData
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α]
  {l : List ((a : α) × β a)} {k : α} {v : β k} [EquivBEq α] [LawfulHashable α],
  m.WF → m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l
-- Mathlib.CategoryTheory.Action.Monoidal
Action.rightDual_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {H : Type u_3} [inst_2 : Group H] (X : Action V H) [inst_3 : CategoryTheory.RightRigidCategory V] (h : H),
  Xᘁ.ρ h = X.ρ h⁻¹ᘁ
-- Mathlib.FieldTheory.NormalizedTrace
/-- If all the coefficients of `minpoly E a` are in `F`, then the normalized trace of `a` from `K`
to `E` equals the normalized trace of `a` from `K` to `F`.  -/
Algebra.normalizedTrace_algebraMap_of_lifts : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F K] [inst_8 : CharZero F] [inst_9 : CharZero E] [inst_10 : Algebra.IsIntegral E K]
  (a : K),
  minpoly E a ∈ Polynomial.lifts (algebraMap F E) →
    (algebraMap F E) ((Algebra.normalizedTrace F K) a) = (Algebra.normalizedTrace E K) a
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.irreducible_toPolynomialAdjoinImageCompl : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  Irreducible F → ∀ (i : ι), (AlgebraicIndependent k fun x => a ↑x) → Irreducible (F.toPolynomialAdjoinImageCompl a i)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedDivisionRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'},
  MDiffAt[s] p z → MDiffAt[s] q z → q z ≠ 0 → MDiffAt[s] (p / q) z
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
NumberField.coe_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(NumberField.discr K) = Algebra.discr ℚ ⇑(NumberField.integralBasis K)
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.instMulAction : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction M αᵐᵒᵖ
-- Init.Data.SInt.Bitwise
Int16.shiftRight_and : ∀ {a b c : Int16}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- The identity of `ℝ` as a Stieltjes function, used to construct Lebesgue measure.  -/
StieltjesFunction.id : StieltjesFunction ℝ
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_false_of_not_eq_true' : ∀ {a : Bool}, ¬a = true → a = false
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the sphere of radius `r`
around zero `{x | v.restrict x = r}` is open in the valuative topology.  -/
Valuation.isOpen_sphere : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsOpen {x | v.restrict x = r}
-- Lean.Expr
Lean.Nat.mkInstLE : Lean.Expr
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (r : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) →
          (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)) →
        ((a : RBTree.RBNode α) →
            (y : α) →
              (b : RBTree.RBNode α) →
                (z : α) →
                  (c : RBTree.RBNode α) →
                    motive
                      (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c)) →
          ((r : RBTree.RBNode α) →
              (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
                  r = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
                (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
                    r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c →
                      False) →
                  motive r) →
            motive r
-- Init.Data.Int.DivMod.Bootstrap
Int.add_mul_ediv_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), b ≠ 0 → (a + b * c) / b = a / b + c
-- Mathlib.Tactic.Linter.Whitespace
/-- The distance to the end of the source string, as number of characters  -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.srcNat : Mathlib.Linter.FormatError✝ → ℕ
-- Mathlib.Algebra.Category.Ring.Under.Property
/-- If `Q` is stable under finite products and equalizers, the inclusion from the subcategory of
`Under R` defined by `Q` creates finite limits.  -/
CommRingCat.Under.createsFiniteLimitsForget : {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} →
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
        (R : CommRingCat) →
          CategoryTheory.Limits.CreatesFiniteLimits
            (CategoryTheory.MorphismProperty.Under.forget
              (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one_assoc : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {X₂ : C₂} {X₃ : C₃}
  (f₁ : X₁ ⟶ Y₁) (g : (F.obj Y₁).obj X₂ ⟶ X₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj₂.homEquiv (CategoryTheory.CategoryStruct.comp ((F.map f₁).app X₂) g)) h =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv g) (CategoryTheory.CategoryStruct.comp ((G.map f₁.op).app X₃) h)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtNormed.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f f_1 : ι → E),
  f = f_1 →
    ∀ (n n_1 : ι), n = n_1 → InnerProductSpace.gramSchmidtNormed 𝕜 f n = InnerProductSpace.gramSchmidtNormed 𝕜 f_1 n_1
-- Mathlib.CategoryTheory.Equivalence
/-- Recover a natural transformation between `e.functor` and `f.functor` from the data of
a morphism `e ⟶ f`.  -/
CategoryTheory.Equivalence.asNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {e f : C ≌ D} → (e ⟶ f) → (e.functor ⟶ f.functor)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictDvd_def : ∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F} [inst_1 : Decidable (q = 0)] (hpq : p ∣ q),
  Polynomial.Gal.restrictDvd hpq = if hq : q = 0 then 1 else Polynomial.Gal.restrict p q.SplittingField
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsElliptic.bc_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsOrderedRing R] {m : Matrix (Fin 2) (Fin 2) R},
  m.IsElliptic → m 0 1 * m 1 0 ≠ 0
-- Mathlib.Algebra.Group.Units.Defs
isUnit_of_mul_isUnit_left : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {x y : M}, IsUnit (x * y) → IsUnit x
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Definition of a prefibered category.

See SGA 1 VI.6.1.  -/
CategoryTheory.Functor.IsPreFibered : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] → CategoryTheory.Functor 𝒳 𝒮 → Prop
-- Lean.Meta.Match.Basic
/-- Alternative patterns.
 -/
Lean.Meta.Match.Alt.patterns : Lean.Meta.Match.Alt → List Lean.Meta.Match.Pattern
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
fderivWithin_fderivWithin_eq_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E},
  s ∈ nhds x → fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderiv 𝕜 (fderiv 𝕜 f) x
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact : ∀ (α : Type u_2) [inst : CompleteLattice α], WellFoundedGT α ↔ CompleteLattice.IsSupFiniteCompact α
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
/-- The binomial distribution with parameter `p` on simple graphs with vertices `V`.  -/
SimpleGraph.binomialRandom : (V : Type u_1) → ↑unitInterval → MeasureTheory.Measure (SimpleGraph V)
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- For `1 < s.re`, the sum over primes of `-log (1 - χ p * p ^ (-s))` — the logarithm of the Euler
product — equals the `L`-series of `n ↦ χ n * Λ n / Real.log n`.
 -/
DirichletCharacter.eulerProduct_log_eq_LSeries : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re →
    ∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) =
      LSeries (fun n => χ ↑n * ↑(ArithmeticFunction.vonMangoldt n) / ↑(Real.log ↑n)) s
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_sUnion : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)},
  (∀ s ∈ S, IsClopen s) → IsClopen (⋃₀ S)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_same_else : ∀ (c t e : Bool), ((bif c then t else e) == e) = (!c || t == e)
-- Init.Data.Fin.Iterate
_private.Init.Data.Fin.Iterate.0.Fin.hIterateFrom.eq_def : ∀ (P : ℕ → Sort u_1) {n : ℕ} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (i : ℕ) (ubnd : i ≤ n) (a : P i),
  Fin.hIterateFrom P f i ubnd a =
    if g : i < n then Fin.hIterateFrom P f (i + 1) g (f ⟨i, g⟩ a)
    else
      have p := ⋯;
      cast ⋯ a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.filterMap_eq_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, Std.ExtTreeMap.filterMap (fun k v => some (f k v)) t = Std.ExtTreeMap.map f t
-- Mathlib.Data.Multiset.AddSub
Multiset.le_sub_add : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ s - t + t
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivOp_eq_lineDerivCLM : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F] {v : E} {T : Distribution Ω F ⊤},
  LineDeriv.lineDerivOp v T = (Distribution.lineDerivCLM v) T
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_sub_sinh : ∀ (x : ℂ), Complex.cosh x - Complex.sinh x = Complex.exp (-x)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a (min b c)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.AddGrp.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_le_of_lt`.  -/
Left.mul_lt_one_of_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, a ≤ 1 → b < 1 → a * b < 1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- Adding a bottom element to a conditionally complete lattice
gives a conditionally complete lattice  -/
WithBot.conditionallyCompleteLattice : {α : Type u_5} → [ConditionallyCompleteLattice α] → ConditionallyCompleteLattice (WithBot α)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_subset_support_append_right : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), q.support ⊆ (p.append q).support
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_self_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ y₁ : F}
  {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ =
    WeierstrassCurve.Affine.Point.some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.addY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁)) ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_toDual : ∀ {E : Type u_2} [inst : NNNorm E] (x : E), ‖OrderDual.toDual x‖₊ = ‖x‖₊
-- Mathlib.NumberTheory.LSeries.ZetaZeros
mem_riemannZetaZeros : ∀ {z : ℂ}, z ∈ riemannZetaZeros ↔ riemannZeta z = 0
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap'_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' (φ + φ') h₁ h₂ =
    CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_sub_smul : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : Module.End R M) (μ : R),
  LinearMap.charpoly (f - μ • 1) = (LinearMap.charpoly f).comp (Polynomial.X + Polynomial.C μ)
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- Given a neighborhood `U` of the identity, one may find a neighborhood `V` of the identity which
is closed, symmetric, and satisfies `V * V ⊆ U`.  -/
exists_closed_nhds_one_inv_eq_mul_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {U : Set G},
  U ∈ nhds 1 → ∃ V ∈ nhds 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
-- Mathlib.Data.Nat.Prime.Defs
Nat.fact_prime_three : Fact (Nat.Prime 3)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.neg : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.instFintypeOne.eq_1 : ∀ {α : Type u_2} [inst : One α], Set.instFintypeOne = Set.fintypeSingleton 1
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.isOpen_mono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] {H₁ H₂ : Subgroup G},
  H₁ ≤ H₂ → IsOpen ↑H₁ → IsOpen ↑H₂
-- Mathlib.Analysis.Seminorm
Seminorm.finset_sup_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E),
  (s.sup p) x = ↑(s.sup fun i => NNReal.mk ((p i) x) ⋯)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.right_of_add_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f (μ + ν) → MeasureTheory.HasFiniteIntegral f ν
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W.map f).polynomialX = Polynomial.map (Polynomial.mapRingHom f) W.polynomialX