mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_mul_cancel : ∀ {R : Type u} [inst : CommRing R] (f g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  AlgebraicGeometry.StructureSheaf.const f g₁ U hu₁ * AlgebraicGeometry.StructureSheaf.const g₁ g₂ U hu₂ =
    AlgebraicGeometry.StructureSheaf.const f g₂ U hu₂
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {c : ℤ → ComplexShape κ} {r₀ : ℤ}
      (data data_1 : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀),
      data = data_1 →
        ∀ (r r_1 : ℤ) (e_r : r = r_1) (pq pq_1 : κ),
          pq = pq_1 →
            ∀ (hr : r₀ ≤ r),
              CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq hr =
                CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X_1 data_1 r_1 pq_1 ⋯
-- Init.Data.Array.Basic
Array.size.eq_1 : ∀ {α : Type u} (a : Array α), a.size = a.toList.length
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} {s : Set α} [inst_1 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    MeasureTheory.AEStronglyMeasurable f (μ.restrict s) →
      MeasureTheory.AEStronglyMeasurable g (μ.restrict sᶜ) → MeasureTheory.AEStronglyMeasurable (s.piecewise f g) μ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulMono_iff_posMulReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α], PosMulMono α ↔ PosMulReflectLT α
-- Lean.Server.References
Lean.Server.Ilean.mk.injEq : ∀ (version : ℕ) (module : Lean.Name) (directImports : Array Lean.Lsp.ImportInfo) (references : Lean.Lsp.ModuleRefs)
  (decls : Lean.Lsp.Decls) (version_1 : ℕ) (module_1 : Lean.Name) (directImports_1 : Array Lean.Lsp.ImportInfo)
  (references_1 : Lean.Lsp.ModuleRefs) (decls_1 : Lean.Lsp.Decls),
  ({ version := version, module := module, directImports := directImports, references := references, decls := decls } =
      { version := version_1, module := module_1, directImports := directImports_1, references := references_1,
        decls := decls_1 }) =
    (version = version_1 ∧
      module = module_1 ∧ directImports = directImports_1 ∧ references = references_1 ∧ decls = decls_1)
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instStrictForwardPatternForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.StrictForwardPattern p
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃ : ∀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.i₃ r pq hr = WithBotTop.coe (↑pq.2 + r - 1)
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.herglotzLogIntegrand.eq_1 : ∀ (w ρ : ℂ), herglotzLogIntegrand✝ w ρ = Complex.re ∘ herglotzRieszKernel 0 w • fun x => Real.log ‖x - ρ‖
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.toFn_zero : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (Polynomial.toFn n) 0 = 0
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_5.splitter : (motive : ℕ → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → Sort u_1) →
  (x : ℕ) →
    (x_1 : Bool) →
      (x_2 : List Lean.MVarId) →
        (x_3 : List (List Lean.MVarId)) →
          (x_4 : Array Lean.MVarId) →
            ((x : ℕ) → (p : Bool) → (acc : Array Lean.MVarId) → motive x p [] [] acc) →
              ((n : ℕ) →
                  (p : Bool) →
                    (goals : List Lean.MVarId) →
                      (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p [] (goals :: stk) acc) →
                ((n : ℕ) →
                    (p : Bool) →
                      (g : Lean.MVarId) →
                        (goals : List Lean.MVarId) →
                          (stk : List (List Lean.MVarId)) →
                            (acc : Array Lean.MVarId) → motive n p (g :: goals) stk acc) →
                  motive x x_1 x_2 x_3 x_4
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.mk.injEq : ∀ (map : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (set : Lean.PHashSet Lean.Meta.Sym.AlphaKey)
  (map_1 : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (set_1 : Lean.PHashSet Lean.Meta.Sym.AlphaKey),
  ({ map := map, set := set } = { map := map_1, set := set_1 }) = (map = map_1 ∧ set = set_1)
-- Lean.Server.References
Lean.Server.ModuleImport.mk.inj : ∀ {module : Lean.Name} {uri : Lean.Lsp.DocumentUri} {isAll isPrivate : Bool} {metaKind : Lean.Lsp.LeanImportMetaKind}
  {module_1 : Lean.Name} {uri_1 : Lean.Lsp.DocumentUri} {isAll_1 isPrivate_1 : Bool}
  {metaKind_1 : Lean.Lsp.LeanImportMetaKind},
  { module := module, uri := uri, isAll := isAll, isPrivate := isPrivate, metaKind := metaKind } =
      { module := module_1, uri := uri_1, isAll := isAll_1, isPrivate := isPrivate_1, metaKind := metaKind_1 } →
    module = module_1 ∧ uri = uri_1 ∧ isAll = isAll_1 ∧ isPrivate = isPrivate_1 ∧ metaKind = metaKind_1
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.symm_toRatAlgEquiv : ∀ {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), f.toRatAlgEquiv.symm = f.symm.toRatAlgEquiv
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in no variables
and the ground ring.  -/
MvPolynomial.isEmptyAlgEquiv : (R : Type u) → (σ : Type u_1) → [inst : CommSemiring R] → [IsEmpty σ] → MvPolynomial σ R ≃ₐ[R] R
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.eq_2 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw) (i : ℕ), x.nextn i.succ x_1 = x.nextn i (x.next x_1)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int16.intCast : IntCast Int16
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_monotone_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P.op ≤ Q.op ↔ P ≤ Q
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.toKStar : {α : Type u_5} → [self : KleeneAlgebra α] → KStar α
-- Mathlib.Tactic.Core
/-- Repeats a tactic until it fails. Always succeeds.  -/
Lean.Elab.Tactic.iterateUntilFailure : {m : Type → Type u} → [Monad m] → [MonadExcept Lean.Exception m] → m Unit → m Unit
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- The derivative of a $C^{k + (α)}$ function is a $C^{l + (α)}$ function, if `l < k`.  -/
ContDiffPointwiseHolderAt.fderiv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k l : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → l < k → ContDiffPointwiseHolderAt l α (fderiv ℝ f) a
-- Init.Data.String.OrderInstances
String.Pos.toInt_eq : ∀ {s : String} {p : s.Pos}, ↑p = ↑p.offset.byteIdx
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.right_of_add_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.MemLp f p (μ + ν) → MeasureTheory.MemLp f p ν
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instCompl : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Compl (L.DefinableSet A α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).getD k fallback = fallback
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mono : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {l' : Filter ι},
  IsAddFoelner G μ l F → l' ≤ l → IsAddFoelner G μ l' F
-- Mathlib.CategoryTheory.Localization.Construction
/-- underlying object  -/
CategoryTheory.Localization.Construction.LocQuiver.obj : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} → CategoryTheory.Localization.Construction.LocQuiver W → C
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.faithfulSMul : ∀ (G : Type u_10) (B : Type u_12) (L : Type u_14) [inst : Group G] [inst_1 : CommRing B]
  [inst_2 : MulSemiringAction G B] [inst_3 : Field L] [inst_4 : Algebra B L] [IsFractionRing B L]
  [inst_6 : MulSemiringAction G L] [SMulDistribClass G B L] [FaithfulSMul G B], FaithfulSMul G L
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- Lower exponential growth of a sequence of extended nonnegative real numbers.  -/
ExpGrowth.expGrowthInf : (ℕ → ENNReal) → EReal
-- Init.Data.List.Range
List.range'_append_1 : ∀ {s m n : ℕ}, List.range' s m ++ List.range' (s + m) n = List.range' s (m + n)
-- Mathlib.Order.RelSeries
RelSeries.head_take : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.take i).head = p.head
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_map : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {S : Type u_1} [inst_1 : CommSemiring S] {φ : R →+* S}
  {f : MvPolynomial σ R} {i : σ},
  (MvPolynomial.pderiv i) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((MvPolynomial.pderiv i) f)
-- Batteries.Data.List.Lemmas
List.lt_add_of_mem_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, ∀ y ∈ List.findIdxs p xs s, y < xs.length + s
-- Lean.Syntax
Lean.Syntax.MonadTraverser.mk : {m : Type → Type} → MonadState Lean.Syntax.Traverser m → Lean.Syntax.MonadTraverser m
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_inf : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (S T : Submodule R E), ↑(S ⊓ T) = ↑S ⊓ ↑T
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_add : ∀ {d : ℤ} (z w : ℤ√d), (z + w).re = z.re + w.re
-- Init.Data.Option.Lemmas
Option.none_lt_some : ∀ {α : Type u_1} [inst : LT α] {a : α}, none < some a
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_nnreal : ∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ↑ε}
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The morphism `X ⟶ Subcomplex.range f` induced by `f : X ⟶ Y`.  -/
SSet.Subcomplex.toRange : {X Y : SSet} → (f : X ⟶ Y) → X ⟶ (SSet.Subcomplex.range f).toSSet
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- A finite number of random variables are independent if and only if their joint characteristic
function is equal to the product of the characteristic functions.
This is `iIndepFun_iff_charFunDual_pi` for `WithLp`. See `iIndepFun_iff_charFun_pi` for the
Hilbert space version.  -/
ProbabilityTheory.iIndepFun_iff_charFunDual_pi' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (p : ENNReal) [inst : Fact (1 ≤ p)]
  {ι : Type u_2} [inst_1 : Fintype ι] [MeasureTheory.IsProbabilityMeasure P] {E : ι → Type u_3}
  {mE : (i : ι) → MeasurableSpace (E i)} [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)]
  [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i}
  [inst_7 : (i : ι) → NormedSpace ℝ (E i)] [inst_8 : DecidableEq ι],
  (∀ (i : ι), AEMeasurable (X i) P) →
    (ProbabilityTheory.iIndepFun X P ↔
      ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => WithLp.toLp p fun x => X x ω) P) L =
          ∏ i,
            MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
              (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i))
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasGenEigenvector_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ} {x : M}, f.HasGenEigenvector μ k x ↔ x ∈ (f.genEigenspace μ) ↑k ∧ x ≠ 0
-- Mathlib.GroupTheory.Torsion
CommGroup.torsion_prod : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H],
  CommGroup.torsion (G × H) = (CommGroup.torsion G).prod (CommGroup.torsion H)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft_obj_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D'),
  (CategoryTheory.Functor.whiskeringLeft C D' E).obj (F.comp G) =
    ((CategoryTheory.Functor.whiskeringLeft D D' E).obj G).comp ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
-- Mathlib.Tactic.Cases
_private.Mathlib.Tactic.Cases.0.Mathlib.Tactic.getAltNumFields : Lean.Meta.ElimInfo → Lean.Name → Lean.Elab.TermElabM ℕ
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.coe_comp : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Pi.abs.match_1.eq_1 : ∀ {n : ℕ} {A : Type u_1} (F : A → TypeVec.{u_1} n → Type u_1) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u_1} n⦄
  (motive : ↑(MvQPF.Pi.P F) α → Sort u_2) (a : (MvQPF.Pi.P F).A) (f : ((MvQPF.Pi.P F).B a).Arrow α)
  (h_1 : (a : (MvQPF.Pi.P F).A) → (f : ((MvQPF.Pi.P F).B a).Arrow α) → motive ⟨a, f⟩),
  (match ⟨a, f⟩ with
    | ⟨a, f⟩ => h_1 a f) =
    h_1 a f
-- Mathlib.Data.Seq.Basic
Stream'.Seq.toList.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates), s.toList h = Stream'.Seq.take (s.length h) s
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] {f g : SupBotHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Init.Grind.Util
Lean.Grind.eqMatchUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerAux_sModEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  (x : Perfection (R ⧸ I) p) (m : ℕ), x.teichmullerAux m ≡ x.teichmullerAux (m + 1) [SMOD I ^ m]
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- If `a ≤ b`, `b ≠ 0`, then `x^b = O(x^a)` as `x → 0`, `x ≥ 0`.  -/
Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le : ∀ {a b : ℝ}, a ≤ b → b ≠ 0 → (fun x => x ^ b) =O[nhdsWithin 0 (Set.Ici 0)] fun x => x ^ a
-- Mathlib.Algebra.Polynomial.Module.TensorProduct
/-- The `R[X]`-linear equivalence `(R[X] ⊗[R] M) ≃ₗ[R[X]] (PolynomialModule R M)`.  -/
PolynomialModule.polynomialTensorProductLEquivPolynomialModule : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → TensorProduct R (Polynomial R) M ≃ₗ[Polynomial R] PolynomialModule R M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.filterMap! : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → Option (γ a)},
          (Std.DTreeMap.Internal.Impl.filterMap! f t₁).Equiv (Std.DTreeMap.Internal.Impl.filterMap! f t₂)
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a b : R),
  ↑(a * b) = ↑a * ↑b
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i))
  (T : CategoryTheory.Limits.FormalCoproduct C)
  (s : { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }) (i : T.I),
  ↑(((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T).symm s).f i) = ((↑s).1.f i, (↑s).2.f i)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_inv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Law of cosines** (cosine rule), angle-at-point form.  -/
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P),
  dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ -
      2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {s : Set α} (h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)),
  ∀ᵐ (x : α) ∂μ, x ∈ s → f x = MeasureTheory.AEStronglyMeasurable.mk f h x
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_one_X : ∀ {R : Type u_1} [inst : Semiring R], (PowerSeries.trunc 1) PowerSeries.X = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_mul_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A trident on `f : J → (X ⟶ Y)` is determined by the morphism `ι : P ⟶ X` satisfying
`∀ j₁ j₂, ι ≫ f j₁ = ι ≫ f j₂`.
 -/
CategoryTheory.Limits.Trident.ofι : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {P : C} →
              (ι : P ⟶ X) →
                (∀ (j₁ j₂ : J),
                    CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) →
                  CategoryTheory.Limits.Trident f
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The underlying predicate should be invariant under restriction  -/
TopCat.PrelocalPredicate.res : ∀ {X : TopCat} {T : ↑X → Type u_1} (self : TopCat.PrelocalPredicate T) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V)
  (f : (x : ↥V) → T ↑x), self.pred f → self.pred fun x => f (i x)
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The induced `G`-action on the target of `J : SingleObj G ⥤ Type u`.  -/
CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar : {M : Type v} →
  [inst : Monoid M] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) →
      MulAction M (J.obj (CategoryTheory.SingleObj.star M))
-- Mathlib.Algebra.Quaternion
Quaternion.coe_sub : ∀ {R : Type u_3} [inst : CommRing R] (x y : R), ↑(x - y) = ↑x - ↑y
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_id_comp_assoc : ∀ {R₁ R₂ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] (f₁₂ : R₁ →+* R₂)
  {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : ModuleCat.extendScalars f₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id R₁) f₁₂).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R₁).hom (ModuleCat.extendScalars f₁₂))
        (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalars f₁₂).leftUnitor.hom h)) =
    h
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
/-- Pull back a pseudometric space structure by a uniform inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `UniformSpace`
structure.  -/
IsUniformInducing.comapPseudoMetricSpace : {α : Type u_3} →
  {β : Type u_4} →
    [inst : UniformSpace α] → [m : PseudoMetricSpace β] → (f : α → β) → IsUniformInducing f → PseudoMetricSpace α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_top : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], ↑⊤ = ⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_sub_mul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α},
  r.toArray = (Std.Rcc.Internal.iter r).toArray
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image2_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, Set.image2 (fun x1 x2 => x1 • x2) s t = s • t
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isoOfHomeo_inv : ∀ {X Y : TopCat} (f : ↑X ≃ₜ ↑Y), (TopCat.isoOfHomeo f).inv = TopCat.ofHom ↑f.symm
-- Init.Data.UInt.Basic
instNegUInt16 : Neg UInt16
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J × D.J),
  (D.diagramIso F).hom.app (CategoryTheory.Limits.WalkingMultispan.left i) =
    CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.left i))
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_gt_two : 2 < Real.exp 1