mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toSubring_subtype : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A),
  NonUnitalSubringClass.subtype S = ↑(NonUnitalStarSubalgebraClass.subtype S)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKeyD_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.Const.modifyKey k f l).isEmpty = false →
        ∀ {fallback : α},
          Std.Internal.List.maxKeyD (Std.Internal.List.Const.modifyKey k f l) fallback =
            if (Std.Internal.List.maxKeyD l fallback == k) = true then k else Std.Internal.List.maxKeyD l fallback
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.isLocalHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → IsLocalHomeomorph f
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- In the alternating group, the stabilizer of a set acts
primitively on that set if the complement is nontrivial.  -/
alternatingGroup.stabilizer_isPreprimitive : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  sᶜ.Nontrivial → MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥(alternatingGroup α)) s) ↑s
-- Init.Data.String.Basic
/-- Constructs a valid position on `t` from a valid position on `s` and a proof that
`s.copy = t.copy`.  -/
String.Slice.Pos.cast : {s t : String.Slice} → s.Pos → s.copy = t.copy → t.Pos
-- Mathlib.Data.EReal.Basic
instAddMonoidEReal : AddMonoid EReal
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.isAtom_smul_finset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G} {a : G},
  Finset.IsAtom✝ K S (a • A) ↔ Finset.IsAtom✝ K S A
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.card_finsuppAntidiag_nat_eq_choose : ∀ {ι : Type u_1} [inst : DecidableEq ι] {s : Finset ι} (n : ℕ), (s.finsuppAntidiag n).card = (s.card + n - 1).choose n
-- Lean.Elab.Tactic.Ext
/-- Applies a single extensionality theorem, using `pats` to introduce variables in the result.
Runs continuation `k` on each subgoal.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.withExt1 : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.Elab.TermElabM m] →
      Lean.MVarId → List (Lean.TSyntax `rcasesPat) → (Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m ℕ) → m ℕ
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_tsum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Type u_4} {f : ι → α → ENNReal},
  (∀ (i : ι), LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop : ∀ {n : Type u} (R : CommRingCat),
  AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.SpecIso n R).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom
      (CommRingCat.ofHom
        (MvPolynomial.eval₂Hom
          (CommRingCat.Hom.hom
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
              (AlgebraicGeometry.Scheme.Hom.appTop
                (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R))))
          (AlgebraicGeometry.AffineSpace.coord (AlgebraicGeometry.Spec R))))
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i},
  HasFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasFDerivAt (φ i) (φ' i) x
-- Mathlib.Analysis.Complex.LocallyUniformLimit
/-- A locally uniform limit of holomorphic functions on an open domain of the complex plane is
holomorphic (the derivatives converge locally uniformly to that of the limit, which is proved
as `TendstoLocallyUniformlyOn.deriv`).  -/
TendstoLocallyUniformlyOn.differentiableOn : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {φ : Filter ι}
  {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E] [φ.NeBot],
  TendstoLocallyUniformlyOn F f φ U → (∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) → IsOpen U → DifferentiableOn ℂ f U
-- Mathlib.Topology.Order.Basic
tendsto_nhds_top_mono : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Preorder β] [inst_2 : OrderTop β] [OrderTopology β]
  {l : Filter α} {f g : α → β}, Filter.Tendsto f l (nhds ⊤) → f ≤ᶠ[l] g → Filter.Tendsto g l (nhds ⊤)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.iUnion : ∀ {R : Type u_1} {X : Type u_2} {ι : Sort u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : ι → Set X},
  (∀ (i : ι), Convexity.IsStarConvexSet R x (s i)) → Convexity.IsStarConvexSet R x (⋃ i, s i)
-- Mathlib.Algebra.Group.Int.Defs
Int.nsmul_eq_mul : ∀ (n : ℕ) (a : ℤ), n • a = ↑n * a
-- Mathlib.Order.Filter.Subsingleton
/-- A subsingleton filter on a nonempty type is less than or equal to `pure a` for some `a`.  -/
Filter.Subsingleton.exists_le_pure : ∀ {α : Type u_1} {l : Filter α} [Nonempty α], l.Subsingleton → ∃ a, l ≤ pure a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpowMonoidHom_apply : ∀ (r : ℝ) (x : NNReal), (NNReal.rpowMonoidHom r) x = x ^ r
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.image_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} {ι : Type u_1}
  (G : ι → CategoryTheory.Subfunctor F) (f : F ⟶ F'), (⨆ i, G i).image f = ⨆ i, (G i).image f
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x → derivWithin (c * d) s x = derivWithin c s x * d x + c x * derivWithin d s x
-- Init.System.IO
IO.instInhabitedTaskState.default : IO.TaskState
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_comp_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : E) (y z : F) (w : G),
  ((InnerProductSpace.rankOne 𝕜) x) y ∘SL ((InnerProductSpace.rankOne 𝕜) z) w =
    inner 𝕜 y z • ((InnerProductSpace.rankOne 𝕜) x) w
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabReduceConfig : Lean.Syntax →
  optParam Lean.Meta.Command.ReduceConfig { } →
    optParam Bool true → Lean.Elab.Command.CommandElabM Lean.Meta.Command.ReduceConfig
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.inverse.eq_1 : ∀ {A : Type u_10} {B : Type u_11} [inst : Monoid A] [inst_1 : Monoid B] (f : A →* B) (g : B → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f),
  f.inverse g h₁ h₂ = { toFun := g, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
continuous functions when `p < ∞`, version in terms of `eLpNorm`.  -/
MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular],
  p ≠ ⊤ →
    ∀ {f : α → E},
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ENNReal},
          ε ≠ 0 →
            ∃ g, HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g p μ
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_mul_ord`. -/
Ordinal.principal_mul_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) c.ord
-- Init.Data.Range.Polymorphic.Basic
Std.Rci.lower_le_of_mem : ∀ {α : Type u} {r : Std.Rci α} {a : α} [inst : LE α], a ∈ r → r.lower ≤ a
-- Lean.PrettyPrinter.Formatter
/-- Whether the generated format begins with the result of an ungrouped category formatter.  -/
Lean.PrettyPrinter.Formatter.State.isUngrouped : Lean.PrettyPrinter.Formatter.State → Bool
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator ≤ LinearMap.ker P.CorootForm
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' R'' : Φ.RightResolution X₂} (φ : R.Hom R') (ψ : R'.Hom R''),
  (φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Naturality of the lax naturality constraint.  -/
CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g)
  {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (F.map g) (self.app b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (CategoryTheory.CategoryStruct.comp (self.naturality g) h)
-- Init.Data.Rat.Lemmas
Rat.den_divInt : ∀ (a b : ℤ), (Rat.divInt a b).den = if b = 0 then 1 else b.natAbs / b.gcd a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.id_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (x : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.CategoryStruct.id x).fst = CategoryTheory.CategoryStruct.id x.fst
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` and `⊥` to the domain and codomain of a `LatticeHom`.  -/
LatticeHom.withTopWithBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] → LatticeHom α β → BoundedLatticeHom (WithTop (WithBot α)) (WithTop (WithBot β))
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.HasLimit.lift_hom_apply : ∀ {R : Type u} [inst : Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J),
  (ModuleCat.Hom.hom (ModuleCat.HasLimit.lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f : Y ⟶ X) {Z : D} (h : e.functor.obj (e.inverse.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app Y)
      (CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app X) h)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.instNonnegHomClassReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NonnegHomClass (NumberField.FinitePlace K) K ℝ
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.checkModifiers : Lean.Elab.Modifiers → Lean.Elab.Modifiers → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_center_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a : A},
  a ∈ Subalgebra.center R A ↔ ∀ (b : A), b * a = a * b
-- Mathlib.Analysis.LocallyConvex.Polar
/-- The (absolute) polar of `s : Set E` is given by the set of all `y : F` such that `‖B x y‖ ≤ 1`
for all `x ∈ s`.  -/
LinearMap.polar : {𝕜 : 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] → (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Set E → Set F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).inl = b.ι CategoryTheory.Limits.WalkingPair.left
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- When a function is `C^n`, it admits `ftaylorSeries 𝕜 f` as a Taylor series up
to order `n` in `s`.  -/
ContDiff.ftaylorSeries : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f)
-- Init.Data.Order.Lemmas
Std.le_total : ∀ {α : Type u} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] {a b : α}, a ≤ b ∨ b ≤ a
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Group.IsFinitelyPresented.out : ∀ {G : Type u_5} {inst : Group G} [self : Group.IsFinitelyPresented G],
  ∃ n φ, Function.Surjective ⇑φ ∧ φ.ker.IsFinitelyNormallyGenerated
-- Mathlib.Algebra.Group.Subgroup.Basic
MulAut.characteristic_apply_symm_apply_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Characteristic] (φ : MulAut G) (h : ↥H),
  ↑((MulEquiv.symm ((MulAut.characteristic H) φ)) h) = (MulEquiv.symm φ) ↑h
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(1)`). Append two `DList α`.  -/
Batteries.DList.append : {α : Type u} → Batteries.DList α → Batteries.DList α → Batteries.DList α
-- Mathlib.Analysis.Distribution.TestFunction
/-- The natural inclusion `𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F)` when `K ⊆ Ω`.  -/
TestFunction.ofSupportedIn : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {n : ℕ∞} →
                {K : TopologicalSpace.Compacts E} → ↑K ⊆ ↑Ω → ContDiffMapSupportedIn E F n K → TestFunction Ω F n
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.Subcomplex.coe_mk' : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) [inst_1 : Topology.CWComplex C] (E : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E)
  (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E),
  ↑(Topology.CWComplex.Subcomplex.mk' C E I closedCell_subset union) = E
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.two_le_iff : ∀ {α : Type u}, 2 ≤ Cardinal.mk α ↔ ∃ x y, x ≠ y
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.range : Lean.DeclarationRanges → Lean.DeclarationRange
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfcₙ` is continuous in the variable `a : A` when `s : Set 𝕜` is compact and `a` varies over
elements whose quasispectrum is contained in `s`, all of which satisfy the predicate `p`, and the
function `f` is continuous `s` and `f 0 = 0`.  -/
Continuous.cfcₙ' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A},
      Continuous a →
        (∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s) →
          autoParam (ContinuousOn f s) Continuous.cfcₙ'._auto_1 →
            autoParam (f 0 = 0) Continuous.cfcₙ'._auto_3 →
              autoParam (∀ (x : X), p (a x)) Continuous.cfcₙ'._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `S / R` and `S' / R'` are algebras, `i : R →+* R'` is a surjective ring homomorphism,
`j : S →+* S'` is an injective ring homomorphism, such that `R → R' → S'` and `R → S → S'` commute,
then the rank of `S / R` is smaller than or equal to the rank of `S' / R'`.  -/
Algebra.lift_rank_le_of_surjective_injective : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  {S' : Type v'} [inst_3 : CommSemiring R'] [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R →+* R')
  (j : S →+* S'),
  Function.Surjective ⇑i →
    Function.Injective ⇑j →
      (algebraMap R' S').comp i = j.comp (algebraMap R S) →
        Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `a : X → A` tends to `a₀ : A` along a
filter `l` (such that eventually `a x` satisfies the predicate `p` associated to `𝕜` and has
spectrum contained in `s`, as does `a₀`), then `fun x ↦ cfc f (a x)` tends to `cfc f a₀`.  -/
Filter.Tendsto.cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {a₀ : A} {l : Filter X},
      Filter.Tendsto a l (nhds a₀) →
        (∀ᶠ (x : X) in l, spectrum 𝕜 (a x) ⊆ s) →
          (∀ᶠ (x : X) in l, p (a x)) →
            spectrum 𝕜 a₀ ⊆ s →
              p a₀ →
                autoParam (ContinuousOn f s) Filter.Tendsto.cfc._auto_1 →
                  Filter.Tendsto (fun x => cfc f (a x)) l (nhds (cfc f a₀))
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a.inj : ∀ {n : ℕ} {a a_1 : ZMod (2 * n)}, QuaternionGroup.a a = QuaternionGroup.a a_1 → a = a_1
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.isRightCancelMulZero_iff : ∀ {R : Type u_1} [inst : Semiring R], IsRightCancelMulZero (Polynomial R) ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isSuccLimit_of_isPrincipal_add`. -/
Ordinal.isSuccLimit_of_principal_add : ∀ {o : Ordinal.{u}}, 1 < o → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o → Order.IsSuccLimit o
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_inter_Icc_of_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {x y : α}, Set.Ioo x y ⊆ s → (s ∩ Set.Icc x y).OrdConnected
-- Mathlib.Combinatorics.Compactness
/-- Given a (dependent) function `g s : (a : s) → β a` for each finite set `s` of `α`, provided that
each `β a` is finite, we can find another function `χ : (a : α) → β a` such that on every `s`,
there is some larger `t` such that `χ` agrees with `g t` on `s`.
Informally, we are stitching together the local functions `g s` into a global `χ` such that on
each `s`, `χ` can be expressed in terms of one of the `g`.
 -/
Set.Finite.rado_selection_subtype : ∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Set α) → s.Finite → (a : ↑s) → β ↑a),
  ∃ χ, ∀ (s : Set α), s.Finite → ∃ t, ∃ (ht : t.Finite) (hst : s ⊆ t), ∀ (x : ↑s), χ ↑x = g t ht (Set.inclusion hst x)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeftEquiv_trans : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddZeroClass M₃] [inst_3 : AddMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃),
  (e₁₂.trans e₂₃).addMonoidHomCongrLeftEquiv = e₁₂.addMonoidHomCongrLeftEquiv.trans e₂₃.addMonoidHomCongrLeftEquiv
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkNatCast : ℕ → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Lean.Expr
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_induction₂ : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A}
  {p : (x y : A) → x ∈ StarAlgebra.adjoin R s → y ∈ StarAlgebra.adjoin R s → Prop},
  (∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) →
      (∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) →
        (∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) →
          (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
              (hz : z ∈ StarAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
            (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                (hz : z ∈ StarAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
              (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                  (hz : z ∈ StarAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                    (hz : z ∈ StarAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                  (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
                      p x y hx hy → p (star x) y ⋯ hy) →
                    (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
                        p x y hx hy → p x (star y) hx ⋯) →
                      ∀ {a b : A} (ha : a ∈ StarAlgebra.adjoin R s) (hb : b ∈ StarAlgebra.adjoin R s), p a b ha hb
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Over a division ring, `dilatransvections` correspond to linear
equivalences `e` such that the linear map `e - id` has rank at most 1.

See also `LinearEquiv.mem_dilatransvections_iff_finrank`.  -/
LinearEquiv.mem_dilatransvections_iff_rank : ∀ {V : Type u_2} [inst : AddCommGroup V] {K : Type u_3} [inst_1 : DivisionRing K] [inst_2 : Module K V] {e : V ≃ₗ[K] V},
  e ∈ LinearEquiv.dilatransvections K V ↔ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1