mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The function that sends `x` to the `y`-derivative of `f (x, y)` at `g (x)` is `C^m` at `x₀`,
where the derivative is taken as a continuous linear map.
We have to assume that `f` is `C^n` at `(x₀, g(x₀))` for `n ≥ m + 1` and `g` is `C^m` at `x₀`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
Version within a set.
 -/
ContMDiffWithinAt.mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  [Js : IsManifold J 1 N] [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M'] {x₀ : N} {f : N → M → M'} {g : N → M}
  {t : Set N} {u : Set M},
  ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (x₀, g x₀) →
    ContMDiffWithinAt J I m g t x₀ →
      x₀ ∈ t →
        Set.MapsTo g t u →
          m + 1 ≤ n →
            UniqueMDiff[u] →
              ContMDiffWithinAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m
                (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv[u] (f x) (g x)) x₀) t x₀
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift_apply_inr : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r)
  (m : M), (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inr m) = g m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_lt' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  [SecondCountableTopology α] [OrderClosedTopology α], MeasurableSet {p | p.1 < p.2}
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.mk.injEq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (bilin : M →ₗ[R] M →ₗ[R] A)
  (contract : ∀ (m : M), (bilin m) m = (algebraMap R A) (Q m))
  (contract_mid : ∀ (m₁ m₂ m₃ : M), (bilin m₁) m₂ * (bilin m₂) m₃ = Q m₂ • (bilin m₁) m₃) (bilin_1 : M →ₗ[R] M →ₗ[R] A)
  (contract_1 : ∀ (m : M), (bilin_1 m) m = (algebraMap R A) (Q m))
  (contract_mid_1 : ∀ (m₁ m₂ m₃ : M), (bilin_1 m₁) m₂ * (bilin_1 m₂) m₃ = Q m₂ • (bilin_1 m₁) m₃),
  ({ bilin := bilin, contract := contract, contract_mid := contract_mid } =
      { bilin := bilin_1, contract := contract_1, contract_mid := contract_mid_1 }) =
    (bilin = bilin_1)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.mem_nsmul_of_ne_zero : ∀ {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ}, n ≠ 0 → (a ∈ n • s ↔ a ∈ s)
-- Init.Data.Array.Erase
Array.eraseP_empty : ∀ {α : Type u_1} {p : α → Bool}, #[].eraseP p = #[]
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.visit : Lean.Expr → Lean.Meta.AbstractNestedProofs.M Lean.Expr
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_erase : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n i : ℕ),
  (SkewPolynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_le_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n i : ι} {ω : Ω} [WellFoundedLT ι], MeasureTheory.hittingAfter u s n ω ≤ ↑i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of `bot_lt_of_lt`. -/
LT.lt.bot_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, b < a → ⊥ < a
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_inverse_obj : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  (x : Cᵒᵖ × Dᵒᵖ), (CategoryTheory.prodOpEquiv C).inverse.obj x = Opposite.op (Opposite.unop x.1, Opposite.unop x.2)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Frequently.le_linearGrowthSup : ∀ {u : ℕ → EReal} {a : EReal}, (∃ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n) → a ≤ LinearGrowth.linearGrowthSup u
-- Mathlib.Order.Hom.Basic
OrderHom.orderHom_eq_id : ∀ {α : Type u_2} [inst : Preorder α] [Subsingleton α] (g : α →o α), g = OrderHom.id
-- Init.Data.Option.Instances
Option.eq_none_of_isNone : ∀ {α : Type u} {o : Option α}, o.isNone = true → o = none
-- Mathlib.Logic.Basic
/-- **Alias** of `or_congr`. -/
Iff.or : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.isTrail : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCircuit → p.IsTrail
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.curry_apply_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (c : CharacterModule (TensorProduct R A B)) (x : A),
  (CharacterModule.curry c) x = AddMonoidHom.comp c ↑((TensorProduct.mk R A B) x)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
MonotoneOn.nnnorm_cfcₙ : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A),
  MonotoneOn f (quasispectrum NNReal a) →
    autoParam (ContinuousOn f (quasispectrum NNReal a)) MonotoneOn.nnnorm_cfcₙ._auto_1 →
      autoParam (f 0 = 0) MonotoneOn.nnnorm_cfcₙ._auto_3 →
        autoParam (0 ≤ a) MonotoneOn.nnnorm_cfcₙ._auto_5 → ‖cfcₙ f a‖₊ = f ‖a‖₊
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In an ordered additive commutative monoid, if each summand `f i` of one finite sum is less than
or equal to the corresponding summand `g i` of another finite sum, then
`∑ i ∈ s, f i ≤ ∑ i ∈ s, g i`.  -/
Finset.sum_le_sum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f g : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, f i ≤ g i) → ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.sup_eq_closure_add : ∀ {M : Type u_3} [inst : AddMonoid M] (H K : AddSubmonoid M), H ⊔ K = AddSubmonoid.closure (↑H + ↑K)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f pf x → HasFPowerSeriesAt (-f) (-pf) x
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable.  -/
ConditionallyCompleteLinearOrder.toDecidableLE : {α : Type u_5} → [self : ConditionallyCompleteLinearOrder α] → DecidableLE α
-- Mathlib.Topology.ShrinkingLemma
/-- Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk"
to a new open cover so that the closure of each new open set is contained in the corresponding
original open set.  -/
exists_iUnion_eq_closure_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} [NormalSpace X],
  (∀ (i : ι), IsOpen (u i)) →
    (∀ (x : X), {i | x ∈ u i}.Finite) →
      ⋃ i, u i = Set.univ → ∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.pairing.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore),
  h.pairing = { I := h.I, II := h.II, inter := ⋯, union := ⋯, p := h.equivII.symm.trans h.equivI }
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instSecondCountableTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [SecondCountableTopology α],
  SecondCountableTopology (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.HasFiniteWidePullbacks.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type) [Finite J], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C) →
    CategoryTheory.Limits.HasFiniteWidePullbacks C
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.topologicalAddGroup : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι}, WithSeminorms p → IsTopologicalAddGroup E
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis_apply_self : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (i j : ι),
  (b.dualBasis i) (b j) = if j = i then 1 else 0
-- Mathlib.Order.Category.Preord
/-- The underlying `OrderHom`.  -/
Preord.Hom.hom' : {X Y : Preord} → X.Hom Y → ↑X →o ↑Y
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (value : Dynamic), sizeOf { stx := stx, value := value } = 1 + sizeOf stx + sizeOf value
-- Mathlib.Data.List.Basic
List.reverse_injective : ∀ {α : Type u}, Function.Injective List.reverse
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α},
  ∅.getKey! a = default
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.div.eq_2 : ∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.div k (Int.Internal.Linear.Poly.add k_1 v p_1) =
    Int.Internal.Linear.Poly.add (k_1 / k) v (Int.Internal.Linear.Poly.div k p_1)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_coe : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (I : Ideal R), Ideal.map (↑f) I = Ideal.map f I
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0),
  x.orderTop = ↑(⋯.min ⋯)
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonShowMessageParams.fromJson : Lean.Json → Except String Lean.Lsp.ShowMessageParams
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y},
  CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst =
      CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst →
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd →
      f = g
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.fourierPowSMulRight.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (n : ℕ),
  VectorFourier.fourierPowSMulRight L f v n =
    (-(2 * ↑Real.pi * Complex.I)) ^ n •
      (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (f v)).compContinuousLinearMap fun x => L v
-- Batteries.Recycling.RBTree.Basic
/-- `path.insertNew v` inserts element `v` into the tree, assuming that `path` is zoomed in
on a `nil` node such that inserting a new element at this position is valid.
 -/
RBTree.RBNode.Path.insertNew : {α : Type u_1} → RBTree.RBNode.Path α → α → RBTree.RBNode α
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Linear equivalence between a curried and uncurried function.
Differs from `TensorProduct.curry`.  -/
LinearEquiv.curry : (R : Type u_1) →
  (M : Type u_5) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (V : Type u_9) → (V₂ : Type u_10) → (V × V₂ → M) ≃ₗ[R] V → V₂ → M
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul_right_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ {q : Polynomial R}, p * q = 0 ↔ q = 0
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The **Cauchy-Davenport Theorem**. If `s`, `t` are nonempty sets in `ℤ/pℤ`, then the size of
`s + t` is lower-bounded by `|s| + |t| - 1`, unless this quantity is greater than `p`.  -/
ZMod.cauchy_davenport : ∀ {p : ℕ}, Nat.Prime p → ∀ {s t : Finset (ZMod p)}, s.Nonempty → t.Nonempty → min p (s.card + t.card - 1) ≤ (s + t).card
-- Mathlib.Tactic.Sat.FromLRAT
/-- A single clause as a formula.  -/
Sat.Fmla.one : Sat.Clause → Sat.Fmla
-- Mathlib.Algebra.Category.ModuleCat.Descent
/-- Extension of scalars along faithfully flat ring maps reflects isomorphisms.  -/
ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat : ∀ {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.FaithfullyFlat → (ModuleCat.extendScalars f).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Given a functor from `C` to `D`, this is the corresponding profunctor from `C` to `D`.  -/
CategoryTheory.Functor.toProfunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Profunctor.{v₂, v₁, v₂, u₁, u₂} C D
-- Mathlib.Order.Antichain
IsAntichain.bot_mem_iff : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : OrderBot α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (⊥ ∈ s ↔ s = {⊥})
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.add_tensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f g : W ⟶ X)
  (h : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (f + g) h =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f h + CategoryTheory.MonoidalCategoryStruct.tensorHom g h
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem** for a disk: if `f : ℂ → E` is continuous on a closed disk
`{z | ‖z - c‖ ≤ R}` and is complex differentiable at all but countably many points of its interior,
then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero.  -/
Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ},
  0 ≤ R →
    ∀ {f : ℂ → E} {c : ℂ} {s : Set ℂ},
      s.Countable →
        ContinuousOn f (Metric.closedBall c R) →
          (∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) → ∮ (z : ℂ) in C(c, R), f z = 0
-- Lean.Parser.Command
Lean.Parser.Command.printAxioms.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- The **Plünnecke-Ruzsa inequality**. Addition version. Note that this is genuinely
harder than the subtraction version because we cannot use a double counting argument.  -/
Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (m n : ℕ), ↑(m • B - n • B).card ≤ (↑(A + B).card / ↑A.card) ^ (m + n) * ↑A.card
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C} [P.IsMultiplicative]
  [Q.IsMultiplicative], (P ⊓ Q).IsMultiplicative
-- Init.Data.UInt.Lemmas
UInt16.mul_succ : ∀ {a b : UInt16}, a * (b + 1) = a * b + a
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.suppressInsideQuot : Lean.Parser.CacheableParserContext → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.MeasureTheory.Group.Measure
/-- The measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`.  -/
MeasureTheory.Measure.neg : {G : Type u_1} → [inst : MeasurableSpace G] → [Neg G] → MeasureTheory.Measure G → MeasureTheory.Measure G
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {U V : TopologicalSpace.Opens M} (hUV : U ≤ V) (f : ↥V → M') (x : ↥U),
      ChartedSpace.LiftPropAt P f (Set.inclusion hUV x) ↔ ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- `mvfderiv I J f x` is the `mfderiv` of a vector-valued function `f` on `M` at `x`,
but taking values in the target normed space directly.
The difference to `mfderiv` is explained in the module-docstring for
`Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean`.

Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/
mvfderiv : {𝕜 : 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] →
                      {F : Type u_8} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] → (M → F) → (x : M) → TangentSpace I x →L[𝕜] F
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.id_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra),
  (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_le_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
-- Init.Prelude
/-- An unsupported syntax exception. We keep this separate because it is
used for control flow: if one macro does not support a syntax then we try
the next one.  -/
Lean.Macro.Exception.unsupportedSyntax : Lean.Macro.Exception
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J),
  c.toStructuredArrowCompToUnderCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.Set.Lattice
Set.biUnion_gt_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [NoMinOrder α] {s : α → Set β}, ⋃ n, ⋃ m, ⋃ (_ : m > n), s m = ⋃ n, s n
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.map.match_1.splitter : {α : Type u_1} →
  (motive : Computation α → Sort u_2) →
    (x : Computation α) →
      ((s : Stream' (Option α)) → (al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a) → motive ⟨s, al⟩) →
        motive x
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.mk : ∀ {G : Type u_1} [inst : AddGroup G], Nat.card G = 4 → AddMonoid.exponent G = 2 → IsAddKleinFour G
-- Mathlib.Algebra.Category.ModuleCat.AB
ModuleCat.isSeparator : ∀ (R : Type u) [inst : Ring R] [inst_1 : Small.{v, u} R], CategoryTheory.IsSeparator (ModuleCat.of R (Shrink.{v, u} R))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Unit part of the monomial.  -/
Tactic.ComputeAsymptotics.Monomial.unit : Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.UnitMonomial
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_sdiff_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α),
  (s.sup fun b => a \ f b) = a \ s.inf f
-- Mathlib.Order.WellFoundedSet
/-- If `α` is a linear order with well-founded `<`, then any set in it is a partially well-ordered set.
Note this does not hold without the linearity assumption.
 -/
Set.IsPWO.of_linearOrder : ∀ {α : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] (s : Set α), s.IsPWO
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, and any family of
`R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
also `R`-linearly independent.  -/
Submodule.LinearDisjoint.linearIndependent_mul_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    Module.Flat R ↥M ∨ Module.Flat R ↥N →
      ∀ {κ : Type u_1} {ι : Type u_2} {m : κ → ↥M} {n : ι → ↥N},
        LinearIndependent R m → LinearIndependent R n → LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.map_relNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (I : Ideal S)
  {T : Type u_4} [inst_11 : Semiring T] (f : R →+* T),
  Ideal.map f ((Ideal.relNorm R) I) = Ideal.span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {𝓨 : Type u_3} {m𝓨 : MeasurableSpace 𝓨}
  {ν : MeasureTheory.Measure 𝓨} {Y : 𝓧 → 𝓨},
  ProbabilityTheory.HasLaw Y ν μ → ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.HasLaw (Y ∘ X) ν P
-- Mathlib.Topology.Maps.Basic
Topology.isCoinducing_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f ↔ ∀ (s : Set Y), IsClosed (f ⁻¹' s) ↔ IsClosed s
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isFibrant_iff_of_isTerminal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y)
  (hY : CategoryTheory.Limits.IsTerminal Y), HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration p