mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.equivQuotMaximalIdealPow_symm_apply_mk_mul : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (n : ℕ) (x : R)
  (s : ↥p.primeCompl),
  (IsLocalization.AtPrime.equivQuotMaximalIdealPow p Rₚ n).symm
        ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ ^ n)) (IsLocalization.mk' Rₚ x s)) *
      (Ideal.Quotient.mk (p ^ n)) ↑s =
    (Ideal.Quotient.mk (p ^ n)) x
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- Free `R`-modules over discrete types are flat.  -/
Module.FaithfullyFlat.finsupp : ∀ (R : Type u) [inst : CommRing R] (ι : Type v) [Nonempty ι], Module.FaithfullyFlat R (ι →₀ R)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.Full
-- Mathlib.Data.Setoid.Basic
/-- The quotient of `α` by the kernel of a function `f`
bijects with the image of `f` lifted to the quotient.  -/
Setoid.quotientKerEquivRangeKerLift : {α : Type u_1} → {β : Type u_2} → (f : α → β) → Quotient (Setoid.ker f) ≃ ↑(Set.range (Setoid.kerLift f))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.consₗ.sizeOf_spec : sizeOf Turing.PartrecToTM2.Γ'.consₗ = 1
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.pi_apply : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x : (i : ι) → Mᵢ i),
  (QuadraticMap.pi Q) x = ∑ i, (Q i) (x i)
-- Mathlib.Analysis.Convex.Segment
mem_segment_sub_add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [Invertible 2] (x y : E), x ∈ segment 𝕜 (x - y) (x + y)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `LinearIsometryEquivClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.

This is an abbreviation for `SemilinearIsometryEquivClass F (RingHom.id R) E E₂`.
 -/
LinearIsometryEquivClass : (𝓕 : Type u_11) →
  (R : outParam (Type u_12)) →
    (E : outParam (Type u_13)) →
      (E₂ : outParam (Type u_14)) →
        [inst : Semiring R] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R E₂] → [EquivLike 𝓕 E E₂] → Prop
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_normalizer : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), (Subgroup.normalizer ↑H).op = Subgroup.normalizer ↑H.op
-- Mathlib.Topology.NhdsWithin
preimage_nhdsWithin_coinduced' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α},
  a ∈ t → s ∈ nhds (X a) → X ⁻¹' s ∈ nhdsWithin a t
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.comp_apply : ∀ {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Init.Data.SInt.Lemmas
Int64.add_zero : ∀ (a : Int64), a + 0 = a
-- Mathlib.Analysis.Fourier.Notation
/-- The notation typeclass for the inverse Fourier transform.

While the inverse Fourier transform is a linear operator, the notation is for the function `E → F`
without any additional properties. This makes it possible to use the notation for functions where
integrability is an issue.
Moreover, including a scalar multiplication causes problems for inferring the notation type class.
 -/
FourierTransformInv : Type u → outParam (Type v) → Type (max u v)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimMap_epi' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] (α : F ⟶ G)
  [CategoryTheory.Epi α], CategoryTheory.Epi (CategoryTheory.Limits.colimMap α)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_zpow_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Group Z] [inst_4 : IsTopologicalGroup Z] (f : C(X × Y, Z)) (n : ℤ) (x : X),
  (f ^ n).curry x = f.curry x ^ n
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_biSup_of_l_u_eq_self : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α),
  (∀ (i : ι) (hi : p i), l (u (f i hi)) = f i hi) → u (⨆ i, ⨆ (hi : p i), f i hi) = ⨆ i, ⨆ (hi : p i), u (f i hi)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- **Alias** of `MeasureTheory.MemLp.of_le`. -/
MeasureTheory.MemLp.mono : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.MemLp f p μ
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`HashSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
the variant {lean}`it.ensureTermination.toHashSet` always terminates after finitely many steps.
 -/
Std.IterM.toHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      {m : Type w → Type w'} →
        [Monad m] → [inst_3 : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → m (Std.HashSet β)
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Sites with a terminal object admit a global sections functor.  -/
CategoryTheory.hasGlobalSectionsFunctor_of_hasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [CategoryTheory.Limits.HasTerminal C], CategoryTheory.HasGlobalSectionsFunctor J A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) g
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K],
  IsIntegrallyClosed ↥(FunctionField.ringOfIntegers F K)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Natural inclusion `B¹(G, A) →ₗ[k] Z¹(G, A)`.  -/
groupCohomology.coboundariesToCocycles₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{max u u_1, u, u} k G) → ↥(groupCohomology.coboundaries₁ A) →ₗ[k] ↥(groupCohomology.cocycles₁ A)
-- Mathlib.Logic.Encodable.Lattice
Encodable.iUnion_decode₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] (f : β → Set α), ⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b = ⋃ b, f b
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulStrictMono.to_covariantClass_pos_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulStrictMono α],
  CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.inv_length : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial), List.length m.inv = List.length m
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toArray_iter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β}, m.iter.toArray = m.toArray
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is both purely inseparable and separable, then `algebraMap F E` is bijective.  -/
IsPurelyInseparable.bijective_algebraMap_of_isSeparable : ∀ (F : Type u_1) (E : Type u_2) [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] [Nontrivial E] [IsDomain F]
  [Module.IsTorsionFree F E] [IsPurelyInseparable F E] [Algebra.IsSeparable F E], Function.Bijective ⇑(algebraMap F E)
-- Mathlib.Data.Multiset.Sum
Multiset.inl_mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {a : α}, Sum.inl a ∈ s.disjSum t ↔ a ∈ s
-- Lean.Util.Diff
/-- Given two `Subarray`s, find their common prefix and return their differing suffixes  -/
Lean.Diff.matchPrefix : {α : Type u_1} → [BEq α] → Subarray α → Subarray α → Array α × Subarray α × Subarray α
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.neg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn (-f) U ↔ MeromorphicOn f U
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffWithinAt_prod_iff : ∀ {𝕜 : 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] {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_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} {x : M} {n : WithTop ℕ∞} (f : M → M' × N'),
  ContMDiffWithinAt I (I'.prod J') n f s x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) s x
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_eq_self_of_isOpen`. -/
gauge_lt_one_eq_self_of_isOpen : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → IsOpen s → {x | gauge s x < 1} = s
-- Mathlib.Order.Partition.Basic
/-- Every partition of `s : Set α` induces a transitive, symmetric binary relation on `α`
whose equivalence classes are the parts of `P`. The relation is irreflexive outside `s`.  -/
Partition.Rel : {α : Type u_1} → {s : Set α} → Partition s → α → α → Prop
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGT.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (lowerBound : α) (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMapGT Std.DTreeMap.Internal.Impl.leaf lowerBound it = it
-- Mathlib.Data.Nat.Pairing
Nat.left_le_pair : ∀ (a b : ℕ), a ≤ Nat.pair a b
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.symm_bijective : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B],
  Function.Bijective StarMulEquiv.symm
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_mul : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ} {f g : MvPolynomial σ R},
  (MvPolynomial.pderiv i) (f * g) = (MvPolynomial.pderiv i) f * g + f * (MvPolynomial.pderiv i) g
-- Mathlib.CategoryTheory.Category.ULift
/-- `AsSmall C` is a small category equivalent to `C`.
More specifically, if `C : Type u` is endowed with `Category.{v} C`, then
`AsSmall.{w} C : Type (max w v u)` is endowed with an instance of a small category.

The objects and morphisms of `AsSmall C` are defined by applying `ULift` to the
objects and morphisms of `C`.

Note: We require a category instance for this definition in order to have direct
access to the universe level `v`.
 -/
CategoryTheory.AsSmall : (D : Type u) → [CategoryTheory.Category.{v, u} D] → Type (max u w v)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE'.congr_simp : ∀ {α : Type u_1} {m : MeasurableSpace α} (s s_1 : MeasureTheory.SignedMeasure α) (e_s : s = s_1) (i i_1 : Set α)
  (e_i : i = i_1) (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i)
  (j j_1 : Set α) (e_j : j = j_1) (hj : MeasurableSet j),
  s.toMeasureOfZeroLE' i hi j hj = s_1.toMeasureOfZeroLE' i_1 ⋯ j_1 ⋯
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** using little-o notation.  -/
taylor_isLittleO : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      ContDiffOn ℝ (↑n) f s → (fun x => f x - taylorWithinEval f n s x₀ x) =o[nhdsWithin x₀ s] fun x => (x - x₀) ^ n
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.eq_gcd_cert.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (g : ℤ)
  (h_1 :
    (k : ℤ) →
      (v : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k v p))
  (h_2 : (g : ℤ) → motive (Lean.Grind.CommRing.Poly.num g)),
  (match Lean.Grind.CommRing.Poly.num g with
    | Lean.Grind.CommRing.Poly.add k v p => h_1 k v p
    | Lean.Grind.CommRing.Poly.num g => h_2 g) =
    h_2 g
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.mapClusterPt_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {x : X} {l : Filter X}, MapClusterPt (f x) l f ↔ ClusterPt x l
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consCollision.congr_simp : ∀ {α : Type u} {β : Type v} (keys keys_1 : Subarray α) (e_keys : keys = keys_1) (vals vals_1 : Subarray β)
  (e_vals : vals = vals_1) (a : Std.Slice.size keys = Std.Slice.size vals)
  (a_1 a_2 : Lean.PersistentHashMap.Zipper α β),
  a_1 = a_2 →
    Lean.PersistentHashMap.Zipper.consCollision keys vals a a_1 =
      Lean.PersistentHashMap.Zipper.consCollision keys_1 vals_1 ⋯ a_2
-- Mathlib.Data.Part
Part.get_eq_iff_eq_some : ∀ {α : Type u_1} {a : Part α} {ha : a.Dom} {b : α}, a.get ha = b ↔ a = Part.some b
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions.mk.sizeOf_spec : ∀ (id? : Option String), sizeOf { id? := id? } = 1 + sizeOf id?
-- Mathlib.Order.Lattice
/-- Pointwise maximum of two monotone functions is a monotone function.  -/
MonotoneOn.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => max (f x) (g x)) s
-- Init.Data.Int.DivMod.Basic
/-- Division of two divisible integers. Division by `0` returns `0`.

This operation uses an optimized implementation, specialized for two divisible integers.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `Int.divExact 21 3 (by decide) = 7`
 * `Int.divExact 21 (-3) (by decide) = -7`
 * `Int.divExact (-15) 5 (by decide) = -3`
 * `Int.divExact 0 22 (by decide) = 0`
 * `Int.divExact 0 0 (by decide) = 0`
 -/
Int.divExact : (x y : ℤ) → y ∣ x → ℤ
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instHashableAuxLemmaKey.hash : Lean.Meta.AuxLemmaKey → UInt64
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The projection `π : K.cylinder ⟶ K`.  -/
HomologicalComplex.cylinder.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → K.cylinder ⟶ K
-- Mathlib.Analysis.Distribution.Support
Distribution.mem_dsupport_iff_frequently : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {x : α},
  x ∈ Distribution.dsupport f ↔ ∃ᶠ (u : Set α) in (nhds x).smallSets, ¬Distribution.IsVanishingOn f u
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.boundaryLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {k' : ι'} {j : ι},
  c'.Rel (e.f j) k' → (∀ (i : ι), e.f i ≠ k') → e.BoundaryLE j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_iso_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.CommSq fst snd f g →
    ∀ [inst_1 : CategoryTheory.Limits.HasPullback f g] (i : P ≅ CategoryTheory.Limits.pullback f g),
      CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.pullback.fst f g) = fst →
        CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.pullback.snd f g) = snd →
          CategoryTheory.IsPullback fst snd f g
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ico_add_one_add_one_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ico (a + 1) (b + 1) = Set.Ioc a b
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), B.polar {0} = Set.univ
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_singleton_eq_one_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.eRk {e} = 1 ↔ M.IsNonloop e
-- Mathlib.Data.Multiset.Basic
Multiset.choose_property : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a),
  p (Multiset.choose p l hp)
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousOn.eq_1 : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α)
  (S : Set X), EquicontinuousOn F S = ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.inflate.eq_1 : ∀ {α : Type v} [small : Std.Internal.Small α] (x : Std.Internal.USquash α),
  x.inflate = Std.Internal.ComputableSmall.inflate x.inner
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleType_cycleRange : ∀ {n : ℕ} {i : Fin n} [inst : NeZero n], i ≠ 0 → i.cycleRange.cycleType = {↑i + 1}
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The domain of the partial equivalence.  -/
PartialEquiv.source : {α : Type u_5} → {β : Type u_6} → PartialEquiv α β → Set α
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_finsetInf : ∀ {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] {ι : Type u_4} (s : Finset ι) (K : ι → Ideal S),
  Ideal.comap f (s.inf K) = s.inf fun i => Ideal.comap f (K i)
-- Init.Data.UInt.Lemmas
UInt32.lt_trans : ∀ {a b c : UInt32}, a < b → b < c → a < c
-- Mathlib.Analysis.SpecificLimits.Normed
/-- For `k ≠ 0` and a constant `r` the function `r / n ^ k` tends to zero.  -/
tendsto_const_div_pow : ∀ (r : ℝ) (k : ℕ), k ≠ 0 → Filter.Tendsto (fun n => r / ↑n ^ k) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsGδ.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  IsGδ s → MeasurableSet s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp f g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskeringLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u_1) →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            [inst_3 : CategoryTheory.MonoidalCategory E] →
              (F : CategoryTheory.Functor C D) → ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).Monoidal
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnInfo.mk.sizeOf_spec : ∀ (numArgs coercee : ℕ) (type : Lean.Meta.CoeFnType),
  sizeOf { numArgs := numArgs, coercee := coercee, type := type } = 1 + sizeOf numArgs + sizeOf coercee + sizeOf type
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Subgroup.smulInvariantMeasure : ∀ {G : Type u_3} {α : Type u_4} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (H : Subgroup G),
  MeasureTheory.SMulInvariantMeasure (↥H) α μ
-- Mathlib.Order.SymmDiff
inf_symmDiff_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff (a ⊓ b) (symmDiff a b) = a ⊔ b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpCompIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal],
  CategoryTheory.Functor.mapGrpCompIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Grp.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapGrp.obj X).X) ⋯ ⋯) ⋯
-- Mathlib.Analysis.Calculus.DSlope
ContinuousWithinAt.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜},
  ContinuousWithinAt (dslope f a) s b → ContinuousWithinAt f s b
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.hasForgetToBialgebra : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (HopfAlgCat R) (BialgCat R)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_left_inj : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit c → (a - c = b - c ↔ a = b)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_add_two_pi : ∀ (x : ℝ), Circle.exp (x + 2 * Real.pi) = Circle.exp x
-- Std.Http.Internal.LowerCase
String.toLower.eq_1 : ∀ (s : String), s.toLower = String.map Char.toLower s
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_symm_apply : ∀ {α : Type u_3} {s : Set α} [inst : DecidablePred fun x => x ∈ s] (x : ↑s), (Equiv.Set.sumCompl s).symm ↑x = Sum.inl x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey?.isSome = true