mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
tprod_one_add_ne_zero_of_summable : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R]
  [NormMulClass R], (∀ (i : ι), 1 + f i ≠ 0) → (Summable fun x => ‖f x‖) → ∏' (i : ι), (1 + f i) ≠ 0
-- Mathlib.Analysis.Complex.HasPrimitives
/-- A function `f` `IsConservativeOn` in `U` if, for any rectangle contained in `U`
the integral of `f` over the rectangle is zero.  -/
Complex.IsConservativeOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → Set ℂ → Prop
-- Init.Data.List.Zip
List.zip_map_right : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {l₁ : List α} {l₂ : List β},
  l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_ric : ∀ {n : ℕ}, (*...=n).toList.toArray = (*...=n).toArray
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.mem_nhds_zero : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) {U : Set G}, U ∈ B → U ∈ nhds 0
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.instEquivLike : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → EquivLike (P₁ ≃ᴬ[k] P₂) P₁ P₂
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Continuous linear map from Schwartz functions to `L^p`.  -/
SchwartzMap.toLpCLM : (𝕜 : Type u_2) →
  {E : Type u_5} →
    (F : Type u_6) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : MeasurableSpace E] →
                [OpensMeasurableSpace E] →
                  [inst_6 : NormedField 𝕜] →
                    [inst_7 : NormedSpace 𝕜 F] →
                      [inst_8 : SMulCommClass ℝ 𝕜 F] →
                        [SecondCountableTopologyEither E F] →
                          (p : ENNReal) →
                            [inst_10 : Fact (1 ≤ p)] →
                              (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toLpCLM._auto_1) →
                                [hμ : μ.HasTemperateGrowth] → SchwartzMap E F →L[𝕜] ↥(MeasureTheory.Lp F p μ)
-- Mathlib.Topology.Defs.Filter
CompactSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsCompact Set.univ → CompactSpace X
-- Std.Sync.StreamMap
/-- Get a specific stream selector by name
 -/
Std.StreamMap.get? : {α β : Type} → [BEq α] → Std.StreamMap α β → α → Option (Std.Async.Selector β)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.trans_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : α), (h₁.trans h₂) x = h₂ (h₁ x)
-- Init.Data.Ord.Basic
/-- Inverts the order of an `Ord` instance.

The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
 -/
Ord.opposite : {α : Type u_1} → Ord α → Ord α
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub'` sometimes doesn't work.  -/
dist_eq_norm_vsub' : ∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y : P), dist x y = ‖y -ᵥ x‖
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- A `MorphismProperty C` is a class of morphisms between objects in `C`.  -/
CategoryTheory.MorphismProperty : (C : Type u) → [CategoryTheory.CategoryStruct.{v, u} C] → Type (max u v)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- A collection of comparisons.  -/
Mathlib.Tactic.Linarith.PCompSet : Type
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a convolution of measures
is the product of the respective characteristic functions.  -/
MeasureTheory.charFun_conv : ∀ {E : Type u_3} [inst : MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (t : E),
  MeasureTheory.charFun (μ.conv ν) t = MeasureTheory.charFun μ t * MeasureTheory.charFun ν t
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
/-- The boundary `∂Δ[n]` of the `n`-th standard simplex consists of
all `m`-simplices of `stdSimplex n` that are not surjective
(when viewed as monotone function `m → n`).  -/
SSet.boundary : (n : ℕ) → (SSet.stdSimplex.obj { len := n }).Subcomplex
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.one_le_inv_iff_le_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : Aˣ},
  0 ≤ ↑a → (1 ≤ ↑a⁻¹ ↔ a ≤ 1)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.subgroupCongr_symm_apply : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H = K) (x : ↥K), ↑((MulEquiv.subgroupCongr h).symm x) = ↑x
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRightIso.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor C A)
  (L : CategoryTheory.Functor A T),
  CategoryTheory.Comma.preRightIso R F L =
    CategoryTheory.NatIso.ofComponents'
      (fun X =>
        CategoryTheory.Comma.isoMk._to_dual_1
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight R F L).obj X).right)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight R F L).obj X).left) ⋯)
      ⋯
-- Init.Data.SInt.Lemmas
Int16.toInt_bmod_4294967296 : ∀ (x : Int16), x.toInt.bmod 4294967296 = x.toInt
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.mk.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (head head_1 : M i),
  head = head_1 →
    ∀ (tail tail_1 : Monoid.CoprodI.Word M) (e_tail : tail = tail_1) (fstIdx_ne : tail.fstIdx ≠ some i),
      { head := head, tail := tail, fstIdx_ne := fstIdx_ne } = { head := head_1, tail := tail_1, fstIdx_ne := ⋯ }
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instIntCast : {R : Type u_1} → [IntCast R] → IntCast Rᵒᵈ
-- Std.Data.DTreeMap.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.DTreeMap.contains : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-- See also `continuousAt_cpow` and `Complex.continuousAt_cpow_of_re_pos`.  -/
Complex.continuousAt_cpow_zero_of_re_pos : ∀ {z : ℂ}, 0 < z.re → ContinuousAt (fun x => x.1 ^ x.2) (0, z)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.opcyclesMapIso iso i).hom = HomologicalComplex.opcyclesMap iso.hom i
-- Mathlib.Order.Hom.Lattice
InfHom.bot_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Bot β] (a : α), ⊥ a = ⊥
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_cons' : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s)
  (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun AddCommute f)),
  (Finset.cons a s ha).noncommSum f comm = s.noncommSum f ⋯ + f a
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `deriv_const_smul_field`.

---

A variant of `deriv_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
deriv_const_smul' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), deriv (c • f) x = c • deriv f x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE? k = Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k none
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
ArithmeticFunction.liouville_ne_zero : ∀ {n : ℕ}, n ≠ 0 → ArithmeticFunction.liouville n ≠ 0
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L)
  [inst_5 : SMulCommClass G K L], F ≤ FixedPoints.intermediateField ↥H ↔ H ≤ fixingSubgroup G ↑F
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Given proofs
- that `a` is a natural number `na`;
- that `b` is a nonnegative rational number `nb / db`;

returns a tuple of
- a natural number `r` (result);
- the same number, as an expression;
- a proof that `a ^ b = r`.

Fails if `na` is not a `db`th power of a natural number.
 -/
Mathlib.Meta.NormNum.proveIsNatRPowIsNNRat : (a : Q(ℝ)) →
  (na : Q(ℕ)) →
    Q(Mathlib.Meta.NormNum.IsNat «$a» «$na») →
      (b : Q(ℝ)) →
        (nb db : Q(ℕ)) →
          Q(Mathlib.Meta.NormNum.IsNNRat «$b» «$nb» «$db») →
            Lean.MetaM (ℕ × (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» ^ «$b») «$r»))
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.prod.snd
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_smul_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {r : R} {f : MvPolynomial σ R},
  m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)
-- Mathlib.Algebra.Module.ULift
ULift.mulAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M],
  ULift.mulAction = { toSMul := ULift.smulLeft, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isoOfHomeo_hom : ∀ {X Y : TopCat} (f : ↑X ≃ₜ ↑Y), (TopCat.isoOfHomeo f).hom = TopCat.ofHom ↑f
-- Mathlib.Order.Heyting.Basic
sdiff_sup_cancel : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a → a \ b ⊔ b = a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_pow_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, Polynomial.X ^ n * p = p * Polynomial.X ^ n
-- Mathlib.GroupTheory.Torsion
IsAddTorsion.eq_1 : ∀ (G : Type u_1) [inst : AddMonoid G], IsAddTorsion G = ∀ (g : G), IsOfFinAddOrder g
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv (t.truncLEι a) = t.truncLTι b
-- Std.Data.DTreeMap.Internal.Balancing
/-- Slower version of `balanceR` which can be used in the complete absence of balancing information
but still assumes that the preconditions of `balanceR` or `balanceRErase` are satisfied
(otherwise panics).
 -/
Std.DTreeMap.Internal.Impl.balanceR! : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α}, ∅.getKey? a = none
-- Init.Core
/-- Places an element of a type into the quotient that equates terms according to an equivalence
relation.

The setoid instance is provided explicitly. `Quotient.mk'` uses instance synthesis instead.

Given `v : α`, `Quotient.mk s v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.
 -/
Quotient.mk : {α : Sort u} → (s : Setoid α) → α → Quotient s
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_toSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), CategoryTheory.Presheaf.IsLocallyInjective J (J.toSheafify P)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0`, then for any `t : ℝ`, the function
`t ↦ ∫ x in 0..t, g x` is bounded below by `t ↦ X + ⌊t/T⌋ • Y` for appropriate constants `X` and
`Y`.  -/
Function.Periodic.sInf_add_zsmul_le_integral_of_pos : ∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      0 < T →
        ∀ (t : ℝ),
          sInf ((fun t => ∫ (x : ℝ) in 0..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x ≤
            ∫ (x : ℝ) in 0..t, g x
-- Lean.Elab.Do.Basic
/-- Throw an error if a declaration of the given name would shadow a `mut` variable.  -/
Lean.Elab.Do.checkMutVarsForShadowingOne : Lean.Ident → Lean.Elab.Do.DoElabM Unit
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The second theorem that characterises the function `reduce`: the maximal
reduction of a word only reduces to itself.  -/
FreeAddGroup.reduce.min : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂ → FreeAddGroup.reduce L₁ = L₂
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The leading coefficient of a sum of polynomials with the same degree is
the sum of the leading coefficients, provided that this sum is nonzero.
 -/
Polynomial.leadingCoeff_sum_of_degree_eq : ∀ {ι : Type w} {S : Type u_1} [inst : Semiring S] {f : ι → Polynomial S} {s : Finset ι} {d : WithBot ℕ},
  (∀ k ∈ s, (f k).degree = d) →
    ∑ k ∈ s, (f k).leadingCoeff ≠ 0 → (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getD_leftInvSeq_mul_wordProd : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  (cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₁ ≃ᵃ[k] P₂
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous at `x₀ : X`* if, for all entourages `U ∈ 𝓤 α`, there is a neighborhood `V` of `x₀`
such that, for all `x ∈ V` and for all `i : ι`, `F i x` is `U`-close to `F i x₀`.  -/
EquicontinuousAt : {ι : Type u_1} →
  {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → (ι → X → α) → X → Prop
-- Mathlib.Tactic.Sat.FromLRAT
/-- The reification of a positive literal `¬⟦a⟧_v ≡ ¬a`.  -/
Sat.Literal.reify_pos : ∀ {v : Sat.Valuation} {a : Prop} {n : ℕ}, (v n ↔ a) → Sat.Literal.reify v (Sat.Literal.pos n) ¬a
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.eq_1 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw), x.nextn 0 x_1 = x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- Given `f : X ⟶ S` and `h : ChosenPullback f f`, this is the type of
morphisms `l : X ⟶ h.pullback` that are equal to the diagonal map.  -/
CategoryTheory.Limits.ChosenPullback.Diagonal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X S : C} → {f : X ⟶ S} → CategoryTheory.Limits.ChosenPullback f f → Type v
-- Lean.Data.AssocList
Lean.AssocList.forIn : {α : Type u} →
  {β : Type v} →
    {δ : Type w} → {m : Type w → Type w'} → [Monad m] → Lean.AssocList α β → δ → (α × β → δ → m (ForInStep δ)) → m δ
-- Mathlib.Order.Bounds.Defs
IsLUB.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsLUB s = IsLeast (upperBounds s)
-- Mathlib.Data.NNReal.Defs
Real.ofNat_le_toNNReal : ∀ {n : ℕ} {r : ℝ} [inst : n.AtLeastTwo], OfNat.ofNat n ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivWithinAt_abs_neg : ∀ (s : Set ℝ) {x : ℝ}, x < 0 → HasDerivWithinAt (fun x => |x|) (-1) s x
-- Mathlib.Algebra.Homology.Single
/-- The object in degree `i` of `(single V c h).obj A` is just `A` when `i = j`.  -/
HomologicalComplex.singleObjXIsoOfEq : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) →
              (j : ι) → (A : V) → (i : ι) → i = j → (((HomologicalComplex.single V c j).obj A).X i ≅ A)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.isCentralScalar : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (P : Submodule R M) [inst_6 : SMul Sᵐᵒᵖ R]
  [inst_7 : SMul Sᵐᵒᵖ M] [inst_8 : IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M], IsCentralScalar S (M ⧸ P)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.prodAddUnits.eq_1 : ∀ {α : Type u} {β : Type v} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid β]
  [inst_3 : TopologicalSpace β],
  Homeomorph.prodAddUnits = { toEquiv := AddEquiv.prodAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Analysis.Seminorm
/-- Closed seminorm-balls at the origin are balanced.  -/
Seminorm.balanced_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.closedBall 0 r)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.π_arrow_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) {Z : C}
  (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j)
      (CategoryTheory.CategoryStruct.comp (arrows j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base arrows) h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → t.minKey?.isSome = true
-- Init.System.Platform
System.Platform.numBits_le : System.Platform.numBits ≤ 64
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_mod_256 : ∀ (n : UInt8), n.toUInt64 % 256 = n.toUInt64
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_mono_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s.addEnergy t₁ ≤ s.addEnergy t₂
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.pushforward_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {S : CategoryTheory.Sheaf K RingCat} [inst_4 : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
  [inst_5 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_6 : ∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C)
  [inst_7 : G.IsContinuous K J] [inst_8 : G.IsCocontinuous K J]
  (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R)
  (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S)
  [inst_9 : ∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))]
  (h :
    ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
      CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂,
          max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
        (SheafOfModules.pushforward
          (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ)))
  {M : SheafOfModules R} (P : M.QuasicoherentData) (i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)),
  (SheafOfModules.QuasicoherentData.pushforward G φ η h P).X i = i.fst
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.infinite : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  [Mi : Infinite M], L.ElementarilyEquivalent M N → Infinite N
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DTreeMap.Raw.Const.toList t ↔ t.getKey? k = some k ∧ Std.DTreeMap.Raw.Const.get? t k = some v
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- Exterior derivative within a set commutes with pullback.  -/
extDerivWithin_pullback : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} {r : WithTop ℕ∞} {s : Set E} {x : E}
  {ω : F → F [⋀^Fin n]→L[𝕜] G} {f : E → F} {t : Set F},
  DifferentiableWithinAt 𝕜 ω t (f x) →
    ContDiffWithinAt 𝕜 r f s x →
      minSmoothness 𝕜 2 ≤ r →
        UniqueDiffOn 𝕜 s →
          x ∈ closure (interior s) →
            x ∈ s →
              Set.MapsTo f s t →
                extDerivWithin (fun x => (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)) s x =
                  (extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)