mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two sets coincide in a punctured neighborhood of `x`,
then the corresponding iterated derivatives are equal.

Note that we also allow to puncture the neighborhood of `x` at `y`.
If `y ≠ x`, then this is a no-op.  -/
iteratedFDerivWithin_congr_set' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f : E → F} {x y : E},
  s =ᶠ[nhdsWithin x {y}ᶜ] t → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Every structure groupoid contains the identity groupoid.  -/
instStructureGroupoidOrderBot : {H : Type u_1} → [inst : TopologicalSpace H] → OrderBot (StructureGroupoid H)
-- Lean.Parser.Command
Lean.Parser.Command.mutual.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Parser.Term
Lean.Parser.Term.typeOf.formatter : Lean.PrettyPrinter.Formatter
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.pure.sizeOf_spec : ∀ (h : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MCasesPat.pure h) = 1 + sizeOf h
-- Init.Data.Option.Lemmas
Option.filter_le : ∀ {α : Type u_1} [inst : LE α], (∀ (x : α), x ≤ x) → ∀ {o : Option α} {p : α → Bool}, Option.filter p o ≤ o
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose_iff₃ : ∀ {p q : Prop}, (¬p ↔ q) → (p ↔ ¬q)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The wideEqualizer built from `wideEqualizer.ι f` is limiting.  -/
CategoryTheory.Limits.wideEqualizerIsWideEqualizer : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        (f : J → (X ⟶ Y)) →
          [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] →
            [inst_2 : Nonempty J] →
              CategoryTheory.Limits.IsLimit
                (CategoryTheory.Limits.Trident.ofι (CategoryTheory.Limits.wideEqualizer.ι f) ⋯)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Padic.adicCompletionEquiv.eq_1 : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  [inst_4 : IsIntegralClosure R ℤ ℚ] (p : Nat.Primes),
  Padic.adicCompletionEquiv R p =
    (ContinuousAlgEquiv.cast ⋯).trans
      (Rat.HeightOneSpectrum.adicCompletion.padicEquiv (Rat.HeightOneSpectrum.primesEquiv.symm p)).symm
-- Mathlib.Algebra.Group.Prod
Prod.zero_mk_add_zero_mk : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : Add N] (b₁ b₂ : N), (0, b₁) + (0, b₂) = (0, b₁ + b₂)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- If `a` is in the `u, v`-compression but `v ≤ a`, then `a` must have been in the original
family.  -/
UV.mem_of_mem_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → v ≤ a → (v = ⊥ → u = ⊥) → a ∈ s
-- Std.Internal.Do.Order.Basic
/-- Top element of a complete lattice (supremum of all elements)  -/
Lean.Order.top : {α : Type u} → [Lean.Order.CompleteLattice α] → α
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
ModuleCat.projectiveDimension_eq_zero_of_projective : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R) [Nontrivial ↑M] [CategoryTheory.Projective M],
  CategoryTheory.projectiveDimension M = 0
-- Init.Data.SInt.Basic
/-- Truncating division for 32-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int32.div 10 3 = 3`
* `Int32.div 10 (-3) = (-3)`
* `Int32.div (-10) (-3) = 3`
* `Int32.div (-10) 3 = (-3)`
* `Int32.div 10 0 = 0`
 -/
Int32.div : Int32 → Int32 → Int32
-- Mathlib.Computability.Primrec.Basic
Primrec₂.pair : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec₂ Prod.mk
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.map_open' : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : α →CO β),
  IsOpenMap self.toFun
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.equiv_symm_eq_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X}
  [inst_5 : CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : CategoryTheory.Meq P S) (I : S.Arrow),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I))
      ((CategoryTheory.Meq.equiv P S).symm x) =
    ↑x I
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_one : NNReal.sqrt 1 = 1
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.preimage_image_coe : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G),
  QuotientGroup.mk ⁻¹' QuotientGroup.mk '' s = ↑N * s
-- Init.Data.Int.Order
Int.max_def : ∀ (n m : ℤ), max n m = if n ≤ m then m else n
-- Init.Data.Nat.Basic
Nat.add_le_add_iff_left : ∀ {m k n : ℕ}, n + m ≤ n + k ↔ m ≤ k
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- The determinant of a matrix given by the Leibniz formula.  -/
Matrix.det : {n : Type u_2} → [DecidableEq n] → [Fintype n] → {R : Type v} → [CommRing R] → Matrix n n R → R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.termX : Lean.ParserDescr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piEquivSucc.eq_1 : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι] [inst_1 : SuccOrder ι]
  (equiv : (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j) (e : F (Order.succ i) ≃ F i × X i) (hi : ¬IsMax i),
  InverseSystem.piEquivSucc equiv e hi =
    InverseSystem.piSplitLE
      (fun j => equiv ⟨↑j, ⋯⟩,
        e.trans
          (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (InverseSystem.piSplitLE.trans (Equiv.piCongrSet ⋯))))
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    [inst : BEq α] →
      (a : α) →
        (motive :
            (x : Std.DHashMap.Internal.AssocList α β) →
              Std.DHashMap.Internal.AssocList.contains a x = true → Sort u_3) →
          (x : Std.DHashMap.Internal.AssocList α β) →
            (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true) →
              ((k : α) →
                  (v : β k) →
                    (es : Std.DHashMap.Internal.AssocList α β) →
                      (h :
                          Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) =
                            true) →
                        motive (Std.DHashMap.Internal.AssocList.cons k v es) h) →
                motive x x_1
-- Init.System.IOError
IO.Error.hardwareFault.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.hardwareFault osCode details = IO.Error.hardwareFault osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.sub_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) (x : P),
  (f - g) x = f x - g x
-- Std.Data.DTreeMap.Internal.Model
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGE?ₘ' : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveHypothesisBundle.mk.inj : ∀ {names : Array String} {fvarIds : Array Lean.FVarId} {type : Lean.Widget.CodeWithInfos}
  {val? : Option Lean.Widget.CodeWithInfos} {isInstance? isType? isInserted? isRemoved? : Option Bool}
  {names_1 : Array String} {fvarIds_1 : Array Lean.FVarId} {type_1 : Lean.Widget.CodeWithInfos}
  {val?_1 : Option Lean.Widget.CodeWithInfos} {isInstance?_1 isType?_1 isInserted?_1 isRemoved?_1 : Option Bool},
  { names := names, fvarIds := fvarIds, type := type, val? := val?, isInstance? := isInstance?, isType? := isType?,
        isInserted? := isInserted?, isRemoved? := isRemoved? } =
      { names := names_1, fvarIds := fvarIds_1, type := type_1, val? := val?_1, isInstance? := isInstance?_1,
        isType? := isType?_1, isInserted? := isInserted?_1, isRemoved? := isRemoved?_1 } →
    names = names_1 ∧
      fvarIds = fvarIds_1 ∧
        type = type_1 ∧
          val? = val?_1 ∧
            isInstance? = isInstance?_1 ∧ isType? = isType?_1 ∧ isInserted? = isInserted?_1 ∧ isRemoved? = isRemoved?_1
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.toRatAlgEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃+* S) (a : R), f.toRatAlgEquiv a = f a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.Nil.tail : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.Nil → p.tail.Nil
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] (M : Type v)
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [inst_6 : IsScalarTower R₀ R M]
  [IsSemisimpleModule R M] [Module.Finite R M],
  ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i)))
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R] {p : Polynomial R}, p.IsPrimitive → p ≠ 0
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.Slice.toList_split_char : ∀ {s : String.Slice} {c : Char},
  List.map String.Slice.copy (s.split c).toList = List.map String.ofList (List.splitOn c s.copy.toList)
-- Mathlib.Order.Heyting.Basic
le_himp_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ (a ⇨ b) ⇨ b
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mk : Lean.Expr →
  Lean.Expr →
    Lean.MetavarContext → Array Lean.Meta.SynthInstance.Instance → ℕ → Bool → Lean.Meta.SynthInstance.GeneratorNode
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Type u_2} [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (f : C(X, NNReal)),
  φ.realContinuousMapOfNNReal ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe }.comp f) = φ f
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁ : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {Y : CategoryTheory.Abelian.SpectralObject C EInt} [self : Y.IsThirdQuadrant] (i j : EInt) (hij : i ≤ j),
  WithBotTop.coe 0 < i →
    ∀ (n : ℤ),
      CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `S`-algebra structure on the underlying completion.  -/
IsDedekindDomain.HeightOneSpectrum.instAlgebraCompletion : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        {S : Type u_3} →
          [inst_2 : Field K] →
            [inst_3 : CommSemiring S] →
              [inst_4 : Algebra R K] →
                [inst_5 : IsFractionRing R K] →
                  (v : IsDedekindDomain.HeightOneSpectrum R) →
                    [Algebra S K] → Algebra S (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Init.Data.UInt.Bitwise
UInt32.ofFin_shiftRight_mod : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a >>> (b % 32)) = UInt32.ofFin a >>> UInt32.ofFin b
-- Init.Data.BitVec.Lemmas
BitVec.append.eq_1 : ∀ {n m : ℕ} (msbs : BitVec n) (lsbs : BitVec m),
  msbs.append lsbs = msbs.shiftLeftZeroExtend m ||| BitVec.setWidth' ⋯ lsbs
-- Mathlib.Algebra.Homology.Homotopy
/-- Being homotopy equivalent is a symmetric relation.  -/
HomotopyEquiv.symm : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → HomotopyEquiv C D → HomotopyEquiv D C
-- Mathlib.Algebra.Category.ModuleCat.Semi
_private.Mathlib.Algebra.Category.ModuleCat.Semi.0.SemimoduleCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : Semiring R] [inst_1 : SizeOf R] (carrier : Type v) [isAddCommMonoid : AddCommMonoid carrier]
  [isModule : Module R carrier],
  sizeOf { carrier := carrier, isAddCommMonoid := isAddCommMonoid, isModule := isModule } =
    1 + sizeOf carrier + sizeOf isAddCommMonoid + sizeOf isModule
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.hasPullback_of_left_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f],
  CategoryTheory.Limits.HasPullback f g
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.forget₂_addGrp_map_ofHom : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] (f : X →+ Y),
  (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).map (AddCommGrpCat.ofHom f) = AddGrpCat.ofHom f
-- Mathlib.Topology.Hom.Open
ContinuousOpenMapClass.toContinuousMapClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : TopologicalSpace α}
  {inst_1 : TopologicalSpace β} {inst_2 : FunLike F α β} [self : ContinuousOpenMapClass F α β], ContinuousMapClass F α β
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.mul` -/
MeasureTheory.AEStronglyMeasurable.fun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Mul β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i * g i) μ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (n : ℕ),
  NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm K n =
    Trans.trans
      (Trans.trans ((NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv K).subtypeEquiv ⋯)
        Equiv.prodSubtypeFstEquivSubtypeProd)
      (Equiv.prodCongrLeft fun x =>
        Equiv.subtypeSubtypeEquivSubtypeInter (fun I => Submodule.IsPrincipal ↑I) fun I => Ideal.absNorm ↑I = n)
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of `Topology.IsEmbedding.induced`. -/
Function.Injective.isEmbedding_induced : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [t : TopologicalSpace Y], Function.Injective f → Topology.IsEmbedding f
-- Init.Data.NeZero
instNeZeroNatHAdd : ∀ {n m : ℕ} [h : NeZero n], NeZero (n + m)
-- Mathlib.Algebra.Group.Defs
/-- Addition is associative  -/
AddSemigroup.add_assoc : ∀ {G : Type u} [self : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.deriv_sigmoid : deriv Real.sigmoid = fun x => x.sigmoid * (1 - x.sigmoid)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atTop_of_degree_gt' : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    0 < P.leadingCoeff / Q.leadingCoeff →
      Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.Integrable.prodLp_fst : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => (f x).fst) μ
-- Mathlib.GroupTheory.PresentedGroup
/-- `of` is the canonical map from `α` to a presented group with generators `x : α`. The term `x` is
mapped to the equivalence class of the image of `x` in `FreeGroup α`.  -/
PresentedGroup.of : {α : Type u_1} → {rels : Set (FreeGroup α)} → α → PresentedGroup rels
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) t.toList
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.mk : {aig : Std.Sat.AIG ℕ} →
  {cnf : Std.Sat.CNF ℕ} →
    (marks : Array Bool) →
      (hmarks : marks.size = aig.decls.size) →
        Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks hmarks → Std.Sat.AIG.toCNF.Cache✝ aig cnf
-- Mathlib.RepresentationTheory.Coinvariants
Rep.finsuppToCoinvariantsTensorFree_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {α : Type u} [inst_2 : DecidableEq α]
  (i : α) (x : ↑A),
  ((A.finsuppToCoinvariantsTensorFree α) fun₀ | i => x) =
    (Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α)))
      (x ⊗ₜ[k] fun₀ | i => MonoidAlgebra.single 1 1)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Given affine opens `x ∈ V ⊆ f⁻¹(U)`, the stalk map of `f` at `x` is isomorphic to
`Localization.localRingHom` of `f.appLE U V`.  -/
AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    {x : ↥X} →
      (U : Y.Opens) →
        (hU : AlgebraicGeometry.IsAffineOpen U) →
          (V : X.Opens) →
            (hV : AlgebraicGeometry.IsAffineOpen V) →
              (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) →
                (hx : x ∈ V) →
                  CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f x) ≅
                    CategoryTheory.Arrow.mk
                      (CommRingCat.ofHom
                        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
                          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)) ⋯))
-- Batteries.Data.List.Perm
List.Subperm.antisymm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₂.Subperm l₁ → l₁.Perm l₂
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.adjunction.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D]
  [inst_4 : J.HasSheafCompose F] (adj : G ⊣ F),
  CategoryTheory.Sheaf.adjunction J adj =
    ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).comp
          (CategoryTheory.sheafificationAdjunction J D)).restrictFullyFaithful
      (CategoryTheory.fullyFaithfulSheafToPresheaf J E)
      (CategoryTheory.Functor.FullyFaithful.id (CategoryTheory.Sheaf J D))
      (CategoryTheory.Iso.refl
        ((CategoryTheory.sheafToPresheaf J E).comp
          (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ E D).obj G).comp (CategoryTheory.presheafToSheaf J D))))
      (CategoryTheory.Iso.refl
        ((CategoryTheory.Functor.id (CategoryTheory.Sheaf J D)).comp
          ((CategoryTheory.sheafToPresheaf J D).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F))))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Ici_sub_Ici' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.Ici a) μ →
    MeasureTheory.IntegrableOn f (Set.Ici b) μ →
      ∫ (x : ℝ) in Set.Ici a, f x ∂μ - ∫ (x : ℝ) in Set.Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Order.Interval.Set.Fin
Fin.image_cast_fun : ∀ {m n : ℕ} (h : m = n), Set.image (Fin.cast h) = Set.preimage (Fin.cast ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.lift_ι_assoc : ∀ {X Y : SSet} (f : X ⟶ Y) {B : Y.Subcomplex} (hf : SSet.Subcomplex.range f ≤ B) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.lift f hf) (CategoryTheory.CategoryStruct.comp B.ι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.EReal.Operations
EReal.top_mul_coe_ennreal : ∀ {x : ENNReal}, x ≠ 0 → ⊤ * ↑x = ⊤
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion : ∀ (K : Type u_1) [inst : Field K], Nonempty ↥(NumberField.Units.torsion K)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.Discharge : Type
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than or equal to the given key.
 -/
Std.ExtDTreeMap.getKeyGE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Mathlib.Algebra.Group.Defs
IsAddTorsionFree.nsmul_right_injective : ∀ {M : Type u_2} {inst : AddMonoid M} [self : IsAddTorsionFree M] ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => n • a
-- Init.Data.List.Attach
List.pmap.eq_def : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (x : List α) (x_1 : ∀ a ∈ x, P a),
  List.pmap f x x_1 =
    match x, x_1 with
    | [], x => []
    | a :: l, H => f a ⋯ :: List.pmap f l ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_descCochain_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n)
  (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r) {Z : C} (h_1 : M.X r ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.descCochain φ α β h).v q r hr) h_1) =
    CategoryTheory.CategoryStruct.comp (β.v p r ⋯) h_1