mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_congr : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M},
  G.LocalInvariantProp G' P → ChartedSpace.LiftPropOn P g s → (∀ y ∈ s, g' y = g y) → ChartedSpace.LiftPropOn P g' s
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The graded tensor product of two elements of graded rings.  -/
GradedTensorProduct.«term_ᵍ⊗ₜ[_]_» : Lean.TrailingParserDescr
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallTelescopeReducingAux : {α : Type} → Lean.Expr → Option ℕ → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Std.Data.HashMap.Raw
/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.HashMap.Raw.all : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → (α → β → Bool) → Bool
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.bialgEquivOfSubsingleton.eq_1 : ∀ {R : Type u_1} (M : Type u_8) [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Subsingleton M],
  AddMonoidAlgebra.bialgEquivOfSubsingleton M =
    { toCoalgHom := (Bialgebra.counitBialgHom R (AddMonoidAlgebra R M)).toCoalgHom,
      invFun := ⇑(algebraMap R (AddMonoidAlgebra R M)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.compl₁₂.eq_1 : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] [inst_13 : SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ)
  (g' : Qₗ' →ₗ[R₂] N), f.compl₁₂ g g' = (f ∘ₗ g).compl₂ g'
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.toFlat : {α : Type} →
  Lean.Meta.LazyDiscrTree.ImportData →
    Lean.Meta.LazyDiscrTree.PreDiscrTree α → BaseIO (Lean.Meta.LazyDiscrTree.InitResults α)
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findSyntheticFieldCompletion? : Lean.FileMap →
  String.Pos.Raw → Lean.Syntax → Lean.Elab.InfoTree → Option Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.Analysis.Complex.BranchLogRoot
/-- If `g : X → ℂ` defined on a locally path connected space
is continuous on an open simply connected set `U` and `0 ∉ g '' U`,
then for any `n ≠ 0`, there exists a continuous branch of `ⁿ√g` on `U`.
More precisely, there exists a function `f : X → ℂ` continuous on `U`
such that `(f x) ^ n = g x` for all `x`.  -/
Complex.exists_continuousOn_pow_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsSimplyConnected U →
    IsOpen U →
      ∀ {g : X → ℂ}, ContinuousOn g U → 0 ∉ g '' U → ∀ {n : ℕ}, n ≠ 0 → ∃ f, ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_mk : ∀ {α : Type u} {L : List (α × Bool)} {β : Type v} [inst : AddGroup β] {f : α → β},
  (FreeAddGroup.lift f) (FreeAddGroup.mk L) = (List.map (fun x => bif x.2 then f x.1 else -f x.1) L).sum
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerCongr_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N)
  (r : ↥(Subsemigroup.center M)), ↑((Submonoid.centerCongr e) r) = e ↑r
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.create.injEq : ∀ (a a_1 : Lean.Lsp.CreateFile), (Lean.Lsp.DocumentChange.create a = Lean.Lsp.DocumentChange.create a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Show the equalizing cocone is a colimit  -/
CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
      [inst_2 : CategoryTheory.Limits.HasPushouts C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
          CategoryTheory.Limits.IsColimit
            (CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone F)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isUniformEmbedding_coe : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding SetLike.coe
-- Mathlib.Analysis.SpecificLimits.FloorPow
mul_pow_le_nat_floor_pow : ∀ {c : ℝ}, 1 < c → ∀ (i : ℕ), (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_eq_liminf_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.bliminf u f p = Filter.liminf (u ∘ Subtype.val) (Filter.comap Subtype.val f)
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeffLinearEquiv.eq_1 : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S],
  MonoidAlgebra.coeffLinearEquiv R = Equiv.linearEquiv R MonoidAlgebra.coeffEquiv
-- Mathlib.Data.Matrix.Basic
Matrix.scalarAlgHom_apply : ∀ (n : Type u_3) (R : Type u_7) {α : Type u_11} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] (a : α), (Matrix.scalarAlgHom n R) a = (Matrix.scalar n) a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_tan : ∀ {x : ℝ}, -(Real.pi / 2) < x → x < Real.pi / 2 → Real.arctan (Real.tan x) = x
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α],
  AddOpposite.instAddCommMonoid = { toAddMonoid := AddOpposite.instAddMonoid, add_comm := ⋯ }
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instSMulWithZeroSubtypeMem : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : NonAssocSemiring R'] →
      {S' : Type u_5} →
        [inst_1 : SetLike S' R'] →
          [inst_2 : SubsemiringClass S' R'] → (s : S') → [inst_3 : Zero α] → [SMulWithZero R' α] → SMulWithZero (↥s) α
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) →
    derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x
-- Mathlib.Data.Set.Function
Set.bijOn_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α), Set.BijOn f s s
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.nextCoeff_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).nextCoeff = f p.nextCoeff
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mono' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (self : StieltjesFunction R), Monotone ↑self
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.equivOp.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_eq_zero : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {x : AddMonoid.Coprod M N},
  (AddMonoid.Coprod.swap M N) x = 0 ↔ x = 0
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankD_set : ∀ {arr : Array Batteries.UFNode} {x : ℕ} {v : Batteries.UFNode} {i : ℕ} {h : x < arr.size},
  Batteries.UnionFind.rankD (arr.set x v h) i = if x = i then v.rank else Batteries.UnionFind.rankD arr i
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.erase_monomial : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} {a : R}, SkewPolynomial.erase n ((SkewPolynomial.monomial n) a) = 0
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.snd` is continuous at `(x, y)`  -/
ContinuousAt.snd' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : Y → Z} {x : X} {y : Y}, ContinuousAt f y → ContinuousAt (fun x => f x.2) (x, y)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The isomorphism of functors `toOver (𝟙_ C)` and `toOverUnit C`.  -/
CategoryTheory.toOverIsoToOverUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.toOver (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.toOverUnit C
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.irreducible_pow_sup_of_ge`. -/
irreducible_pow_sup_of_ge : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ → Irreducible J → ∀ (n : ℕ), emultiplicity J I ≤ ↑n → J ^ n ⊔ I = J ^ multiplicity J I
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a morphism `f` has an image.  -/
CategoryTheory.Limits.ImageFactorisation : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- If `a : ℂ` has norm greater than one, then `circleAverage (log ‖· - a‖) 0 1` equals `log ‖a‖`.
 -/
circleAverage_log_norm_sub_const₂ : ∀ {a : ℂ}, 1 < ‖a‖ → Real.circleAverage (fun x => Real.log ‖x - a‖) 0 1 = Real.log ‖a‖
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The regular wreath product of groups `Q` and `D`. It is the product `(Q → D) × Q` with the group
operation `⟨a₁, a₂⟩ * ⟨b₁, b₂⟩ = ⟨a₁ * (fun x ↦ b₁ (a₂⁻¹ * x)), a₂ * b₂⟩`.  -/
RegularWreathProduct : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of `MeasurableSet.setOfPred_infinite`. -/
MeasurableSet.setOf_infinite : ∀ {α : Type u_1} [Countable α], MeasurableSet {s | s.Infinite}
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Given a match-application `e` with `MatcherInfo` `info`, return `some result`
if at least of one of the discriminants has been simplified.
 -/
Lean.Meta.Simp.simpMatchDiscrs? : Lean.Meta.MatcherInfo → Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.Order.RelSeries
SetRel.finiteDimensional_iff : ∀ {α : Type u_1} (r : SetRel α α), r.FiniteDimensional ↔ ∃ x, ∀ (y : RelSeries r), y.length ≤ x.length
-- Mathlib.Data.Multiset.Count
Multiset.countP_False : ∀ {α : Type u_1} {s : Multiset α}, Multiset.countP (fun x => False) s = 0
-- Mathlib.Order.WellFoundedSet
Set.IsWF.mono : ∀ {α : Type u_2} [inst : LT α] {s t : Set α}, t.IsWF → s ⊆ t → s.IsWF
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.C_smul_derivation_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R) (f : Polynomial R),
  Polynomial.C a • D f = a • D f
-- Lean.Declaration
Lean.RecursorRule.mk.injEq : ∀ (ctor : Lean.Name) (nfields : ℕ) (rhs : Lean.Expr) (ctor_1 : Lean.Name) (nfields_1 : ℕ) (rhs_1 : Lean.Expr),
  ({ ctor := ctor, nfields := nfields, rhs := rhs } = { ctor := ctor_1, nfields := nfields_1, rhs := rhs_1 }) =
    (ctor = ctor_1 ∧ nfields = nfields_1 ∧ rhs = rhs_1)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.mem_supp_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedAddCommMonoidWithTop Γ₀] [inst_1 : CommRing R]
  (v : AddValuation R Γ₀) (x : R), x ∈ v.supp ↔ v x = ⊤
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorAdd'_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ)
  (a₁ a₂ a₃ : A) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : B) (h₁ : b₁ = φ a₁) (h₂ : b₂ = φ a₂) (h₃ : b₃ = φ a₃),
  (CategoryTheory.shiftFunctorAdd' (CategoryTheory.PullbackShift C φ) a₁ a₂ a₃ h).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a₂).map
        ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).hom.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).hom.app ((CategoryTheory.shiftFunctor C b₁).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app X)
          ((CategoryTheory.pullbackShiftIso C φ a₃ b₃ h₃).inv.app X)))
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.inclusionOfMooreComplexMap_f : ∀ {A : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) (n : ℕ),
  (AlgebraicTopology.inclusionOfMooreComplexMap X).f n = (AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_right_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : CategoryTheory.Over Y),
  ((CategoryTheory.ChosenPullbacksAlong.pullback f.inv).obj Z).right.as = PUnit.unit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (t.insertMany l).size = t.size + l.length
-- Mathlib.Data.List.Permutation
List.get_permutations'Aux : ∀ {α : Type u_1} (s : List α) (x : α) (n : ℕ) (hn : n < (List.permutations'Aux x s).length),
  (List.permutations'Aux x s).get ⟨n, hn⟩ = s.insertIdx n x
-- Mathlib.RingTheory.Ideal.Basic
Ideal.pow_multiset_sum_mem_span_pow : ∀ {α : Type u_2} [inst : CommSemiring α] [inst_1 : DecidableEq α] (s : Multiset α) (n : ℕ),
  s.sum ^ (s.card * n + 1) ∈ Ideal.span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
-- Mathlib.Topology.Compactness.Paracompact
/-- **Dieudonné's theorem**: a paracompact R₁ space is normal.
Formalization is based on the proof
at [ncatlab](https://ncatlab.org/nlab/show/paracompact+Hausdorff+spaces+are+normal).  -/
NormalSpace.of_paracompactSpace_r1Space : ∀ {X : Type v} [inst : TopologicalSpace X] [R1Space X] [ParacompactSpace X], NormalSpace X
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `pi` construction for affine maps. From a family of affine maps it produces an affine
map into a family of affine spaces.

This is the affine version of `LinearMap.pi`.
 -/
AffineMap.pi : {k : Type u_2} →
  {V1 : Type u_3} →
    {P1 : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] →
          [inst_2 : AddTorsor V1 P1] →
            [inst_3 : Module k V1] →
              {ι : Type u_9} →
                {φv : ι → Type u_10} →
                  {φp : ι → Type u_11} →
                    [inst_4 : (i : ι) → AddCommGroup (φv i)] →
                      [inst_5 : (i : ι) → Module k (φv i)] →
                        [inst_6 : (i : ι) → AddTorsor (φv i) (φp i)] →
                          ((i : ι) → P1 →ᵃ[k] φp i) → P1 →ᵃ[k] (i : ι) → φp i
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_eval₂_eq_zero_of_commute : ∀ {R : Type u} [inst : Semiring R] {A : Type u_1} [inst_1 : Semiring A] {p : Polynomial R} (f : R →+* A) {z : A},
  Polynomial.eval₂ f z p = 0 →
    Commute (f p.leadingCoeff) z →
      (∀ {r r' : R}, Commute (f r) (f r')) →
        (∀ (x : R), f x = 0 → x = 0) → Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insert k v).minKey ⋯ = k
-- Mathlib.Order.BourbakiWitt
/-- An admissible set for given `x : α` and `f : α → α` has `x`, the base point, as a least element
and is closed under applying `f` and `cSup`.  -/
ChainCompletePartialOrder.IsAdmissible : {α : Type u_1} → [ChainCompletePartialOrder α] → α → (α → α) → Set α → Prop
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- Given an element `a : A` of an `S`-algebra, where `S` is itself an `R`-algebra, we say that
the spectrum of `a` restricts via a function `f : S → R` if `f` is a left inverse of
`algebraMap R S`, and `f` is a right inverse of `algebraMap R S` on `spectrum S a`.

For example, when `f = Complex.re` (so `S := ℂ` and `R := ℝ`), `SpectrumRestricts a f` means that
the `ℂ`-spectrum of `a` is contained within `ℝ`. This arises naturally when `a` is selfadjoint
and `A` is a C⋆-algebra.

This is the property allows us to restrict a continuous functional calculus over `S` to a
continuous functional calculus over `R`.  -/
QuasispectrumRestricts : {R : Type u_3} →
  {S : Type u_4} →
    {A : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : NonUnitalRing A] → [Module R A] → [Module S A] → [Algebra R S] → A → (S → R) → Prop
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mvars.levels : Lean.Option Bool
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Order.Sublattice
Sublattice.mem_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Lattice α] {a : α} {f : ι → Sublattice α}, a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.sub_mem_ker_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {x y : M}, x - y ∈ f.ker ↔ f x = f y
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_compLinearMap_lsingle : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p))
  (p : (i : ι) → κ i),
  ((MultilinearMap.dfinsuppFamily f).compLinearMap fun i => DFinsupp.lsingle (p i)) =
    (DFinsupp.lsingle p).compMultilinearMap (f p)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Auxiliary simp lemma for the `coherence` tactic:
this move brackets to the left in order to expose a maximal prefix
built out of unitors and associators.
 -/
Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂ : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b}
  [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g]
  [inst_3 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] (η : f ⟶ g) (θ : g ⟶ h) (ι : h ⟶ i)
  [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ θ],
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.mk : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {X : C} →
                {data : F.OneHypercoverDenseData J₀ J X} →
                  {X₀ : C₀} →
                    {f : F.obj X₀ ⟶ X} →
                      {Y₀ : C₀} →
                        {g : Y₀ ⟶ X₀} →
                          (i₀ : data.I₀) →
                            (q : F.obj Y₀ ⟶ F.obj (data.X i₀)) →
                              autoParam
                                  (CategoryTheory.CategoryStruct.comp q (data.f i₀) =
                                    CategoryTheory.CategoryStruct.comp (F.map g) f)
                                  CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam →
                                data.SieveStruct f g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is not zero or `π` if and only if the three points are affinely
independent.  -/
EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 ∧ EuclideanGeometry.oangle p₁ p₂ p₃ ≠ ↑Real.pi ↔
    AffineIndependent ℝ ![p₁, p₂, p₃]
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instAdd : {E : Type u_3} → [inst : AddGroup E] → Add (AddGroupNorm E)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.integral_inducedMeasure : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B] (f : CompactlySupportedContinuousMap B ℝ),
  ∫ (b : B), f b ∂H.inducedMeasure μA μC = (H.integrate μA μC) f
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `U` is a family of open sets that covers `X`, then `X.restrict U` forms an `X.open_cover`.  -/
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover : {s : Type u_1} → (X : AlgebraicGeometry.Scheme) → (U : s → X.Opens) → TopologicalSpace.IsOpenCover U → X.OpenCover
-- Mathlib.Algebra.Group.Hom.Basic
/-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
monoids.  -/
powMonoidHom : {α : Type u_1} → [inst : CommMonoid α] → ℕ → α →* α