mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_realPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] (f : ℂ → ℂ)
  (a : A),
  autoParam (ContinuousOn f (quasispectrum ℂ ↑(realPart a))) cfcₙ_realPart._auto_1 →
    autoParam (f 0 = 0) cfcₙ_realPart._auto_3 →
      autoParam (IsStarNormal a) cfcₙ_realPart._auto_5 → cfcₙ f ↑(realPart a) = cfcₙ (fun x => f ↑x.re) a
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.isProbabilityMeasure_bind : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {m : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure m] {f : α → MeasureTheory.Measure β},
  AEMeasurable f m →
    (∀ᵐ (μ : α) ∂m, MeasureTheory.IsProbabilityMeasure (f μ)) → MeasureTheory.IsProbabilityMeasure (m.bind f)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_extend_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : β → γ}, Function.Injective g → (Summable (Function.extend g f 0) ↔ Summable f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The product of the composition of functions `f` and `g`, is the product over `b ∈ s.image g` of
`f b` to the power of the cardinality of the fibre of `b`. See also `Finset.prod_image`.  -/
Finset.prod_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] [inst_1 : DecidableEq κ] (f : κ → M)
  (g : ι → κ), ∏ a ∈ s, f (g a) = ∏ b ∈ Finset.image g s, f b ^ {a ∈ s | g a = b}.card
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.mem_himp_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR.loop.eq_def : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i : ℕ) (a : i ≤ n),
  Nat.allTR.loop✝ n f i a =
    match i, a with
    | 0, h => true
    | m.succ, h => f (n - m.succ) ⋯ && Nat.allTR.loop✝ n f m ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.instStar : {R : Type u_3} → [inst : CommRing R] → Star (Quaternion R)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.one_apply : ∀ {A : Type u_1} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A] (a : A), 1 a = a
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integrable_zero : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l (fun x => 0) vol
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_algEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2}
  [inst_5 : Ring U] [inst_6 : Algebra R U] (h'' : IsAdjoinRoot U f) (x : S),
  (h'.algEquiv h'') ((h.algEquiv h') x) = (h.algEquiv h'') x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instIsLocalHomAlgHomToAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), IsLocalHom ↑e
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  ¬μ.HaveLebesgueDecomposition ν → μ.rnDeriv ν = 0
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_rankInfinite_iff : ∀ {α : Type u_1} (M : Matroid α), ¬M.RankInfinite ↔ M.RankFinite
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.lift_apply : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {B : Type w'} [inst_4 : Semiring B]
  [inst_5 : Algebra R B] (maps : {i : I} → A i →ₐ[R] B),
  (LinearAlgebra.FreeProduct.lift R A) maps =
    (LinearAlgebra.FreeProduct.ringCon R A).liftₐ
      ((TensorAlgebra.lift R) (DirectSum.toModule R I B fun x => maps.toLinearMap)) ⋯
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_iInf_ge_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) (k : ℕ),
  ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i
-- Mathlib.RingTheory.Ideal.Basis
Ideal.basisSpanSingleton.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (b : Module.Basis ι R S) {x : S} (hx : x ≠ 0),
  Ideal.basisSpanSingleton b hx =
    b.map
      (((LinearEquiv.ofInjective (LinearMap.mulLeft R x) ⋯).trans
            (LinearEquiv.ofEq (LinearMap.mulLeft R x).range (Submodule.restrictScalars R (Ideal.span {x})) ⋯)).trans
        (LinearEquiv.restrictScalars R (Submodule.restrictScalarsEquiv R S S (Ideal.span {x}))))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (fallback : β k),
  t.getD k fallback =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => fallback
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match h : compare k k' with
      | Ordering.lt => l.getD k fallback
      | Ordering.gt => r.getD k fallback
      | Ordering.eq => cast ⋯ v'
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkNotation : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_sub : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [inst_1 : AddCommGroup M]
  [inst_2 : SubtractionCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m₁ m₂ : M) (s : ↥S),
  IsLocalizedModule.mk' f (m₁ - m₂) s = IsLocalizedModule.mk' f m₁ s - IsLocalizedModule.mk' f m₂ s
-- Init.Data.List.Lemmas
List.foldl_eq_apply_foldr : ∀ {α : Type u_1} {init x : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulRightIdentity f init],
  List.foldl f x xs = f x (List.foldr f init xs)
-- Mathlib.Data.ZMod.QuotientRing
/-- `ℤ` modulo the ideal generated by `a : ℤ` is `ZMod a.natAbs`.  -/
Int.quotientSpanEquivZMod : (a : ℤ) → ℤ ⧸ Ideal.span {a} ≃+* ZMod a.natAbs
-- Mathlib.Order.Lattice
Ne.lt_sup_or_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≠ b → a < a ⊔ b ∨ b < a ⊔ b
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toStrictlyUnitaryPseudofunctor : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor.map f)
            (toStrictlyUnitaryPseudofunctor.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam)
  (mapComp_eq_eqToIso :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam)
  (toStrictlyUnitaryPseudofunctor_1 : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (map_comp_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor_1.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor_1.map f)
            (toStrictlyUnitaryPseudofunctor_1.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam)
  (mapComp_eq_eqToIso_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor_1.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam),
  ({ toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor, map_comp := map_comp,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso } =
      { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor_1, map_comp := map_comp_1,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso_1 }) =
    (toStrictlyUnitaryPseudofunctor = toStrictlyUnitaryPseudofunctor_1)
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- The length of a path in a manifold is invariant under a monotone reparametrization.  -/
Manifold.pathELength_comp_of_monotoneOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)]
  {f : ℝ → ℝ},
  a ≤ b →
    MonotoneOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Icc a b) →
        MDiff[Set.Icc (f a) (f b)] γ → Manifold.pathELength I (γ ∘ f) a b = Manifold.pathELength I γ (f a) (f b)
-- Init.Data.String.Basic
String.Pos.ofToSlice_le_iff : ∀ {s : String} {p : s.toSlice.Pos} {q : s.Pos}, String.Pos.ofToSlice p ≤ q ↔ p ≤ q.toSlice
-- Mathlib.Control.Fold
Monoid.Foldl.ofFreeMonoid_apply : ∀ {α β : Type u} (f : β → α → β) (xs : FreeMonoid α),
  (Monoid.Foldl.ofFreeMonoid f) xs = MulOpposite.op (TypeCat.ofHom (flip (List.foldl f) (FreeMonoid.toList xs)))
-- Mathlib.Data.Real.Embedding
Archimedean.embedReal_apply : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : One M]
  [inst_4 : ZeroLEOneClass M] [inst_5 : NeZero 1] [inst_6 : Archimedean M] (a : M),
  (Archimedean.embedReal M) a = Archimedean.embedRealFun a
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkGate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkGate
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.ofIso_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (s : S₁.Splitting) (e : S₁ ≅ S₂),
  (s.ofIso e).s = CategoryTheory.CategoryStruct.comp e.inv.τ₃ (CategoryTheory.CategoryStruct.comp s.s e.hom.τ₂)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_veq_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x x' y y' : R}, x =ᵥ y → x' =ᵥ y' → x * x' =ᵥ y * y'
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableAt_iff_target : ∀ {𝕜 : 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 : M → M'} {x : M},
  MDiffAt f x ↔ ContinuousAt f x ∧ MDiffAt (↑(extChartAt I' (f x)) ∘ f) x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.explore_eq_applyPartition : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] {k : α → Ordering} (init : δ)
  (l : Std.DTreeMap.Internal.Impl α β) (f : δ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → δ),
  (∀ {k_1 : α} {hk : k k_1 = Ordering.lt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Std.DTreeMap.Internal.Cell α β k}
      {rr r : List ((a : α) × β a)} {init : δ},
      f (f init (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k_1 hk v r))
          (Std.DTreeMap.Internal.Impl.ExplorationStep.eq ll c rr) =
        f init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq ll c (rr ++ ⟨k_1, v⟩ :: r))) →
    (∀ {k_1 : α} {hk : k k_1 = Ordering.gt} {v : β k_1} {ll : List ((a : α) × β a)}
        {c : Std.DTreeMap.Internal.Cell α β k} {rr l : List ((a : α) × β a)} {init : δ},
        f (f init (Std.DTreeMap.Internal.Impl.ExplorationStep.gt l k_1 hk v))
            (Std.DTreeMap.Internal.Impl.ExplorationStep.eq ll c rr) =
          f init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq (l ++ ⟨k_1, v⟩ :: ll) c rr)) →
      Std.DTreeMap.Internal.Impl.explore k init f l =
        Std.DTreeMap.Internal.Impl.applyPartition k l fun l_1 c x r =>
          f init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq l_1 c r)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_top_of_bound : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.MemLp f ⊤ μ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The bicone constructed in `binaryBiconeOfIsSplitEpiOfKernel` is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.  -/
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [inst_2 : CategoryTheory.IsSplitEpi f] →
            {c : CategoryTheory.Limits.KernelFork f} →
              (i : CategoryTheory.Limits.IsLimit c) →
                (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.embedding_map : ∀ (R : Type u_1) [inst : CommRing R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] {x x_1 : C} (f : x ⟶ x_1),
  (CategoryTheory.Free.embedding R C).map f = fun₀ | f => 1
-- Aesop.Stats.Basic
Aesop.Stats.total : Aesop.Stats → Aesop.Nanos
-- Mathlib.NumberTheory.Divisors
Nat.mem_divisorsAntidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_eq_zero' : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R),
  (∀ d ∈ φ.support, Finsupp.degree d ≠ n) → (MvPolynomial.homogeneousComponent n) φ = 0
-- Lean.Meta.HaveTelescope
/-- Auxiliary structure used to represent the return value of `simpHaveTelescopeAux`.
See `simpHaveTelescope` for an overview and `HaveTelescopeInfo` for an example.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult : Type
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_sConvexComb : ∀ {R : Type u_1} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  (f : Convexity.StdSimplex R (Convexity.StdSimplex R I)),
  (Convexity.sConvexComb f).weights = f.weights.sum fun d r => r • d.weights
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofIntTruncate : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.monObjAsOverPullback_one : ∀ {M S T : AlgebraicGeometry.Scheme} [inst : M.Over S] {f : T ⟶ S} [inst_1 : CategoryTheory.MonObj (M.asOver S)],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback f))
      ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.one)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Subgroup.IsFinitelyNormallyGenerated.of_FG : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [N.Normal] [h : Group.FG ↥N], N.IsFinitelyNormallyGenerated
-- Mathlib.Order.Filter.CountableInter
eventually_countable_ball : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {p : α → (i : ι) → i ∈ S → Prop},
      (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instInhabited : (R : Type u_1) →
  {V : Type u_2} →
    {W : Type u_3} →
      (P : Type u_4) →
        {Q : Type u_5} →
          [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 Q] → [inst_8 : AddTorsor W Q] → Inhabited (P →ᴬ[R] Q)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.re_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b), (star z).re = z.re + b * z.im
-- Init.System.IOError
IO.Error.resourceExhausted.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.resourceExhausted filename osCode details = IO.Error.resourceExhausted filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C).obj X₁).obj X₂).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₁) X₃
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.mk : (toTop : TopCat) → [is_compactly_generated : UCompactlyGeneratedSpace ↑toTop] → CompactlyGenerated
-- Mathlib.Data.Seq.Defs
Stream'.Seq.destruct_nil : ∀ {α : Type u}, Stream'.Seq.nil.destruct = none
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.unitClosedBall_eq_univ_of_discrete : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜], Metric.closedBall 0 1 = Set.univ
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.tensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Center C → CategoryTheory.Center C → CategoryTheory.Center C
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Two compositions (possibly of different integers) coincide if and only if they have the
same sequence of blocks.  -/
Composition.sigma_eq_iff_blocks_eq : ∀ {c c' : (n : ℕ) × Composition n}, c = c' ↔ c.snd.blocks = c'.snd.blocks
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal],
  F.mapAddMon =
    { obj := fun A => { X := F.obj A.X, addMon := CategoryTheory.Functor.addMonObjObj A.X },
      map := fun {X Y} f => { hom := F.map f.hom, isAddMonHom_hom := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.RingTheory.WittVector.Basic
/-- `WittVector.map f` is the ring homomorphism `𝕎 R →+* 𝕎 S` naturally induced
by a ring homomorphism `f : R →+* S`. It acts coefficientwise.  -/
WittVector.map : {p : ℕ} →
  {R : Type u_1} →
    {S : Type u_2} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Fact (Nat.Prime p)] → (R →+* S) → WittVector p R →+* WittVector p S
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_right : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] (f : F) {f' : F'},
  UpperHalfPlane.IsZeroAtImInfty ⇑f' → UpperHalfPlane.IsZeroAtImInfty (UpperHalfPlane.petersson k ⇑f ⇑f')
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.pointwise_smul_le_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S T : AddSubmonoid A}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.mk_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b),
  (CategoryTheory.Limits.WidePullbackCone.mk b π h).base = b
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- If `fs i → f` in `L1`, then `setToL1 hT (fs i) → setToL1 hT f`.  -/
MeasureTheory.L1.tendsto_setToL1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : ↥(MeasureTheory.Lp E 1 μ)) {ι : Type u_7} (fs : ι → ↥(MeasureTheory.Lp E 1 μ)) {l : Filter ι},
  Filter.Tendsto fs l (nhds f) →
    Filter.Tendsto (fun i => (MeasureTheory.L1.setToL1 hT) (fs i)) l (nhds ((MeasureTheory.L1.setToL1 hT) f))
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.image_source_inter_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Constructor for functors from `FreeRefl`.  -/
CategoryTheory.Cat.FreeRefl.lift_spec : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (F : V ⥤rq D), CategoryTheory.Cat.toFreeRefl V ⋙rq (CategoryTheory.Cat.FreeRefl.lift F).toReflPrefunctor = F
-- Mathlib.Util.Notation3
Mathlib.Notation3.BoundValueType.normal.sizeOf_spec : sizeOf Mathlib.Notation3.BoundValueType.normal = 1
-- Mathlib.Algebra.Group.Prod
Prod.instCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : CancelMonoid M] [inst_1 : CancelMonoid N],
  Prod.instCancelMonoid = { toLeftCancelMonoid := Prod.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.ExceptT.run_bind.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((x : α) → motive (Except.ok x)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.star_mem_nonZeroDivisors_iff : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  star z ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- If `C` holds for the `algebraMap` of `r : R` into `CliffordAlgebra Q`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `CliffordAlgebra Q`.

See also the stronger `CliffordAlgebra.left_induction` and `CliffordAlgebra.right_induction`.
 -/
CliffordAlgebra.induction : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {C : CliffordAlgebra Q → Prop},
  (∀ (r : R), C ((algebraMap R (CliffordAlgebra Q)) r)) →
    (∀ (x : M), C ((CliffordAlgebra.ι Q) x)) →
      (∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)) →
        (∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)) → ∀ (a : CliffordAlgebra Q), C a