mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.liftOnAddUnits_mk : ∀ {M : Type u_1} {α : Type u_4} [inst : AddMonoid M] {c : AddCon M} (f : (x y : M) → c (x + y) 0 → c (y + x) 0 → α)
  (Hf :
    ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0) (hyx' : c (y' + x') 0),
      c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx')
  (x y : M) (hxy : ↑x + ↑y = 0) (hyx : ↑y + ↑x = 0),
  AddCon.liftOnAddUnits { val := ↑x, neg := ↑y, val_neg := hxy, neg_val := hyx } f Hf = f x y ⋯ ⋯
-- Mathlib.RingTheory.HopfAlgebra.TensorProduct
TensorProduct.instHopfAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : HopfAlgebra R A] →
                    [inst_6 : HopfAlgebra S B] →
                      [inst_7 : Algebra R B] → [IsScalarTower R S B] → HopfAlgebra S (TensorProduct R B A)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- **Alias** of `AlgebraicGeometry.Flat.flat_appLE`. -/
AlgebraicGeometry.Scheme.Hom.flat_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Flat f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.n : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {combined : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined → ℕ
-- Init.Data.List.Nat.TakeDrop
List.reverse_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1},
  l.length = l'.length → (List.zipWith f l l').reverse = List.zipWith f l.reverse l'.reverse
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_of_le_of_le : ∀ {n : ℕ} {i j k : Fin n}, i ≤ k → k ≤ j → ∀ [inst : NeZero n], (i.cycleIcc j) k = if k = j then i else k + 1
-- Mathlib.Topology.Algebra.Ring.Ideal
Ideal.coe_closure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsTopologicalRing R] (I : Ideal R),
  ↑I.closure = closure ↑I
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact ↔ CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Up to pre-composing with an equivalence of categories, `Sigma.functor` is isomorphic
to `colim`.  -/
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim : (α : Type w₂) →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] →
        (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim ≅
          CategoryTheory.Limits.Sigma.functor α
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_norm_left`. -/
Asymptotics.IsLittleO.of_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =o[l] g → f' =o[l] g
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (motive : Std.DTreeMap.Internal.RxoIterator α β → Sort u_3) →
        (x : Std.DTreeMap.Internal.RxoIterator α β) →
          ((upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }) →
            ((k : α) →
                (v : β k) →
                  (t : Std.DTreeMap.Internal.Impl α β) →
                    (it : Std.DTreeMap.Internal.Zipper α β) →
                      (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }) →
              motive x
-- Init.Data.Fin.Basic
_private.Init.Data.Fin.Basic.0.Fin.modn.match_1.splitter : {n : ℕ} →
  (motive : Fin n → ℕ → Sort u_1) →
    (x : Fin n) → (x_1 : ℕ) → ((a : ℕ) → (h : a < n) → (m : ℕ) → motive ⟨a, h⟩ m) → motive x x_1
-- Mathlib.RingTheory.PowerSeries.Exp
/-- A power series with derivative equal to itself and constant term 1 must be `exp`.

The proof uses induction on coefficients: if `f' = f` and `f(0) = 1`, then
`coeff (n+1) f * (n+1) = coeff n f`, which determines all coefficients uniquely.  -/
PowerSeries.exp_unique_of_derivative_eq_self : ∀ {A : Type u_3} [inst : CommRing A] [inst_1 : Algebra ℚ A] [IsAddTorsionFree A] {f : PowerSeries A},
  (PowerSeries.derivative A) f = f → PowerSeries.constantCoeff f = 1 → f = PowerSeries.exp A
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_obj_X₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₂ = K.X j
-- Init.Data.UInt.IntToBitVec
UInt16.toBitVec64_toUSize : ∀ (n : UInt16) (h : System.Platform.numBits = 64), n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec
-- Init.Core
DoResultPRBC.continue.inj : ∀ {α β σ : Type u} {a a_1 : σ}, DoResultPRBC.continue a = DoResultPRBC.continue a_1 → a = a_1
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
HasStrictDerivAt.to_localInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜}
  (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0),
  HasStrictDerivAt (HasStrictDerivAt.localInverse f f' a hf hf') f'⁻¹ (f a)
-- Init.Data.BitVec.Lemmas
BitVec.concat.eq_1 : ∀ {n : ℕ} (msbs : BitVec n) (lsb : Bool), msbs.concat lsb = msbs ++ BitVec.ofBool lsb
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey?_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (Std.Internal.List.Const.modifyKey k f l) =
      if Std.Internal.List.containsKey k l = true then some k else none
-- Mathlib.Analysis.Normed.Group.Basic
norm_isUnit_zsmul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) {n : ℤ}, IsUnit n → ‖n • a‖ = ‖a‖
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality_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] {d d' : D} (f : d ⟶ d') {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d'
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').inv h)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V},
  (∀ (p : G.Walk v w), s(v, w) ∈ p.edges) →
    ∀ (c : G.Walk u u), c.IsTrail → ∀ (he : s(v, w) ∈ c.edges), w ∈ (c.takeUntil v ⋯).support → False
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.abs_ofNat : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Lattice R] [IsOrderedRing R] (n : ℕ) [inst_3 : n.AtLeastTwo],
  |OfNat.ofNat n| = OfNat.ofNat n
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_commute : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], Commute (↑r) a
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- A regular argument.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular : Lean.Term → Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.Topology.Algebra.Monoid
continuousMul_of_indiscreteTopology : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Mul N] [IndiscreteTopology N], ContinuousMul N
-- Mathlib.Analysis.Convex.Extreme
image_extremePoints : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {L : Type u_6} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [IsOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F]
  [inst_7 : EquivLike L E F] [LinearEquivClass L 𝕜 E F] (f : L) (s : Set E),
  ⇑f '' Set.extremePoints 𝕜 s = Set.extremePoints 𝕜 (⇑f '' s)
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on the upper half plane in complex space  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromUpperHalfPlane : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Batteries.Data.List.Basic
List.IsChain.below.singleton : ∀ {α : Type u_1} {R : α → α → Prop} {motive : (a : List α) → List.IsChain R a → Prop} (a : α), List.IsChain.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.whiskerEquiv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C}
  (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [inst_1 : CategoryTheory.Limits.HasProduct f]
  [inst_2 : CategoryTheory.Limits.HasProduct g],
  (CategoryTheory.Limits.Pi.whiskerEquiv e w).hom =
    CategoryTheory.Limits.Pi.map' ⇑e.symm fun k =>
      CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.insert_toList_zoom_nil : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {p : RBTree.RBNode.Path α} {v : α}
  {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (RBTree.RBNode.nil, p) → (RBTree.RBNode.insert cmp t v).toList = p.withList [v]
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.prod_swap : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β), (μ.prod ν).map Prod.swap = ν.prod μ
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.resolution_quasiIso : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) → QuasiIso (Rep.FiniteCyclicGroup.resolution.π k g)
-- Mathlib.Order.RelClasses
/-- **Alias** of `superset_antisymm`.

---

Set notation form of `ge_antisymm` -/
HasSubset.Subset.antisymm' : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → a ⊆ b → a = b
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.eval_integral_piLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E} [inst_3 : (i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)],
  (∀ (i : ι), MeasureTheory.Integrable (fun x => (f x).ofLp i) μ) →
    ∀ (i : ι), (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.simpMatch : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Polynomial.Derivative
/-- Chain rule for formal derivative of polynomials.  -/
Polynomial.derivative_eval₂_C : ∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R),
  Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) =
    Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_le_re_and_le_im : ∀ (a b : ℝ), frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.aeEq_iff : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {f g : α → β}, f =ᵐ[μ] g ↔ μ {x | f x ≠ g x} = 0
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Set.pairwise_union_of_symm`. -/
Set.pairwise_union_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α} [Std.Symm r],
  (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.hom.inj_on_objects : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), Function.Injective S.hom.obj
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α],
  Topology.IsEmbedding TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.monic_scaleRoots_iff : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} (s : R), (p.scaleRoots s).Monic ↔ p.Monic
-- Mathlib.Data.Seq.Computation
Computation.Bind.f.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → Computation β) (cb : Computation β),
  Computation.Bind.f f (Sum.inr cb) = Computation.Bind.g cb.destruct
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.instBotWideSubquiver : {V : Type u_1} → [inst : Quiver V] → Bot (WideSubquiver V)
-- Mathlib.Order.SupClosed
isSublattice_univ : ∀ {α : Type u_3} [inst : Lattice α], IsSublattice Set.univ
-- Mathlib.Order.Completion
DedekindCut.factorEmbedding_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : PartialOrder β] (f : β ↪o α) (A : DedekindCut β),
  (DedekindCut.factorEmbedding f) A = sSup (⇑f '' A.left)
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.structuredArrowEquiv_apply : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  (W : CategoryTheory.MorphismProperty C) (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  [inst_3 : L.IsLocalization W] [inst_4 : L'.IsLocalization W] {X : C} (f : CategoryTheory.StructuredArrow (L.obj X) L),
  (CategoryTheory.Localization.structuredArrowEquiv W L L') f =
    CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L L') f.hom)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.IsCofibrant ((HomotopicalAlgebra.CofibrantObject.localizerMorphism C).functor.obj X)
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.instInhabitedMethod.default : Aesop.ScriptGenerated.Method
-- Mathlib.Algebra.Lie.EngelSubalgebra
/-- A Lie-subalgebra of an Artinian Lie algebra is self-normalizing
if it contains an Engel subalgebra.
See `LieSubalgebra.normalizer_engel` for a proof that Engel subalgebras are self-normalizing,
avoiding the Artinian condition.  -/
LieSubalgebra.normalizer_eq_self_of_engel_le : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsArtinian R L]
  (H : LieSubalgebra R L) (x : L), LieSubalgebra.engel R x ≤ H → H.normalizer = H
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofPNatList.eq_1 : ∀ (l : List ℕ+) (h : ∀ p ∈ l, p.Prime), PrimeMultiset.ofPNatList l h = PrimeMultiset.ofPNatMultiset (↑l) h
-- Mathlib.Analysis.Calculus.MeanValue
/-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
bounded by `C` satisfies `‖f 1 - f 0‖ ≤ C`, `derivWithin` version.  -/
norm_image_sub_le_of_norm_deriv_le_segment_01 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {C : ℝ},
  DifferentiableOn ℝ f (Set.Icc 0 1) → (∀ x ∈ Set.Ico 0 1, ‖derivWithin f (Set.Icc 0 1) x‖ ≤ C) → ‖f 1 - f 0‖ ≤ C
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for directional derivatives.

Version for a Schwartz function with values in continuous linear maps.  -/
SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left : ∀ {𝕜 : Type u_2} {D : Type u_4} {V : Type u_7} {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup D] [inst_5 : NormedSpace ℝ D]
  [inst_6 : MeasurableSpace D] {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure]
  [inst_10 : RCLike 𝕜] [inst_11 : NormedSpace 𝕜 F] [inst_12 : NormedSpace 𝕜 V] (f : SchwartzMap D (F →L[𝕜] V))
  (g : SchwartzMap D F) (v : D),
  ∫ (x : D), (f x) ((LineDeriv.lineDerivOp v g) x) ∂μ = -∫ (x : D), ((LineDeriv.lineDerivOp v f) x) (g x) ∂μ
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- An arbitrarily chosen projective resolution of an object.  -/
CategoryTheory.projectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Z : C) →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.HasProjectiveResolution Z] → CategoryTheory.ProjectiveResolution Z
-- Init.Data.Vector.Lemmas
Vector.forall_mem_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {P : β → Prop},
  (∀ i ∈ Vector.map f xs, P i) ↔ ∀ j ∈ xs, P (f j)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (X : C) (X_1 : CategoryTheory.Sheaf (J.over X) A)
  (X_2 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackId A X).hom.app X_1).hom.app X_2 =
    X_1.obj.map ((CategoryTheory.Over.mapId X).inv.app (Opposite.unop X_2)).op
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.coePolynomial.eq_1 : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (P : Polynomial K),
  ↑P = (algebraMap (Polynomial K) (RatFunc K)) P
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (A : C)
  [CategoryTheory.Closed A], (CategoryTheory.Limits.prod.functor.obj A).IsLeftAdjoint
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_toNonUnitalSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} {x : A}, x ∈ S.toNonUnitalSubring ↔ x ∈ S
-- Init.Core
/-- A reasoning principle that allows proofs about squashed types to assume that all values are
constructed with `Squash.mk`.
 -/
Squash.ind : ∀ {α : Sort u} {motive : Squash α → Prop}, (∀ (a : α), motive (Squash.mk a)) → ∀ (q : Squash α), motive q
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.monoidalComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} [inst_1 : CategoryTheory.MonoidalCoherence X Y]
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.monoidalComp f g =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCoherence.iso.hom g)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))))
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)),
  ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet
        (NumberField.mixedEmbedding.fundamentalCone.idealSetMap K J a)) ∈
    ↑↑J
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯ =
    (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫
      CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b₁).symm
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.compactSpace_of_isAffine : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X], CompactSpace ↥X
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C),
  CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.bwd : Bool → Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated],
  P.trW.IsCompatibleWithTriangulation
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_mul : ∀ {a b : UInt64}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). True if the trees have the same elements, ignoring structural differences.

```
Equiv {1, 2, 4} {2, 1, 1, 4} = true
Equiv {1, 2, 4} {1, 2, 3} = false
```  -/
Ordnode.Equiv : {α : Type u_1} → Ordnode α → Ordnode α → Prop
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel.  -/
CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.IsIdempotentComplete C ↔
    ∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → CategoryTheory.Limits.HasKernel p
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNat' : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNat n).toUInt64 = UInt64.ofNat n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_eq_toList_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], r.toList = (Std.PRange.UpwardEnumerable.least...=r.upper).toList