mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.le_order_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → ∀ (f : MvPowerSeries σ R), (⨅ i, (a i).order) * f.order ≤ (MvPowerSeries.subst a f).order
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Helper definition for the seminorms of the Schwartz space.  -/
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → ℕ → ℕ → SchwartzMap E F → ℝ
-- Lean.Language.Basic
/-- Applies the current `SnapshotTreeTransform` to a `SnapshotTree` and recursively to its children.  -/
Lean.Language.SnapshotTree.transform : Lean.Language.SnapshotTree → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree
-- Init.Data.Array.Lemmas
Array.flatten_map_toArray_toArray : ∀ {α : Type u_1} {L : List (List α)}, (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
-- Init.Data.Iterators.Basic
Std.Iter.toIter_comp_toIterM : ∀ {α β : Type w}, Std.IterM.toIter ∘ Std.Iter.toIterM = id
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a}, p.IsHamiltonianCycle → p.IsCycle
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAnti_dual_iff`. -/
StrictAnti.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.disconnect_le : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), S.disconnect ≤ S
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_mrange_le : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
  (f : (i : ι) → M i →* N) {s : Submonoid N},
  MonoidHom.mrange (Monoid.CoprodI.lift f) ≤ s ↔ ∀ (i : ι), MonoidHom.mrange (f i) ≤ s
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_pow : ∀ {a b : ℝ} (n : ℕ) {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  IntervalIntegrable (fun x => x ^ n) μ a b
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_of_inter_support_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s t : Set α},
  MeasurableSet s → MeasurableSet t → s ∩ p.support = t ∩ p.support → p.toMeasure s = p.toMeasure t
-- Mathlib.Topology.Basic
IsClosed.not : ∀ {X : Type u} {p : X → Prop} [inst : TopologicalSpace X], IsClosed {a | p a} → IsOpen {a | ¬p a}
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.prod_dp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  {s : Finset ι} {n : ι → ℕ} {m : M},
  ∏ i ∈ s, DividedPowerAlgebra.dp R (n i) m = ↑(Nat.multinomial s n) * DividedPowerAlgebra.dp R (s.sum n) m
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_ge_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {l : Filter β}
  {u : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l fun x => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Auxiliary definition used to define `liftOfRightInverse`  -/
AddMonoidHom.liftOfRightInverseAux : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : AddGroup G₁] →
        [inst_1 : AddGroup G₂] →
          [inst_2 : AddGroup G₃] →
            (f : G₁ →+ G₂) →
              (f_neg : G₂ → G₁) → Function.RightInverse f_neg ⇑f → (g : G₁ →+ G₃) → f.ker ≤ g.ker → G₂ →+ G₃
-- Batteries.Data.UnionFind.Basic
/-- Parent of union-find node  -/
Batteries.UnionFind.parent : Batteries.UnionFind → ℕ → ℕ
-- Mathlib.NumberTheory.Real.Irrational
instDecidableIrrationalSqrtCastReal_2 : (q : ℚ) → Decidable (Irrational √↑q)
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.scale.eq_1 : ∀ {E : Type u_1} (f : ℂ → E) (l u : ℝ) (z : ℂ), Complex.HadamardThreeLines.scale f l u z = f (↑l + z • (↑u - ↑l))
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`.  -/
closure_Ioo : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.Ioo a b) = Set.Icc a b
-- Init.Data.SInt.Lemmas
Int64.lt_or_lt_of_ne : ∀ {a b : Int64}, a ≠ b → a < b ∨ b < a
-- Mathlib.Topology.Compactification.StoneCech
stoneCechExtend_extends : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β] {g : α → β}
  (hg : Continuous g) [inst_3 : CompactSpace β], stoneCechExtend hg ∘ stoneCechUnit = g
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_mul_Ici_eq : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] [MulRightMono α] {a b : α},
  Set.Ici a * Set.Ici b = Set.Ici (a * b)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The source of a 1-simplex in a path is identified with the source vertex.  -/
SSet.Path.arrow_src : ∀ {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) (f.arrow i) = f.vertex i.castSucc
-- Mathlib.Algebra.Homology.Augment
CochainComplex.cochainComplex_d_succ_succ_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) (i : ℕ), C.d 0 (i + 2) = 0
-- Init.Data.Array.Lemmas
Array.append_eq_empty_iff : ∀ {α : Type u_1} {xs ys : Array α}, xs ++ ys = #[] ↔ xs = #[] ∧ ys = #[]
-- Mathlib.Algebra.Group.Hom.Defs
/-- `MonoidHomClass F M N` states that `F` is a type of `Monoid`-preserving homomorphisms.
You should also extend this typeclass when you extend `MonoidHom`.  -/
MonoidHomClass : (F : Type u_10) →
  (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [MulOne M] → [MulOne N] → [FunLike F M N] → Prop
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_conjTranspose : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] [inst_2 : StarAddMonoid R]
  (A : Matrix n n R), A.conjTranspose.trace = star A.trace
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.helperLemmaNames : Array Lean.Name
-- Std.Async.ContextAsync
/-- Checks if the current context is cancelled. Returns `true` if the context (or any ancestor) has been cancelled.
Long-running operations should periodically check this and exit gracefully when cancelled.
 -/
Std.Async.ContextAsync.isCancelled : Std.Async.ContextAsync Bool
-- Lean.Parser.Command
Lean.Parser.Command.structure.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_const : ∀ {b : EReal}, b ≠ ⊥ → b ≠ ⊤ → (LinearGrowth.linearGrowthSup fun x => b) = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_apply : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] {c a : A},
  (CFC.conjSqrt c) a = CFC.sqrt c * a * CFC.sqrt c
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_central_scalar : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R]
  [inst_3 : MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R], IsCentralScalar M (Subring R)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.DHashMap.Const.insertMany m l},
            Std.DHashMap.Const.get (Std.DHashMap.Const.insertMany m l) k' h = v
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
finite_integral_rpow_sub_one_pow_aux : ∀ {r : ℝ} (n : ℕ), ↑n < r → ∫⁻ (x : ℝ) in Set.Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
-- Init.Data.UInt.Lemmas
UInt8.toFin_mod : ∀ (a b : UInt8), (a % b).toFin = a.toFin % b.toFin
-- Mathlib.Util.AtomM
/-- The list of atoms-up-to-defeq encountered thus far, used for atom sorting.  -/
Mathlib.Tactic.AtomM.State.atoms : Mathlib.Tactic.AtomM.State → Array Lean.Expr
-- Mathlib.CategoryTheory.Limits.Cones
/-- For `F : J ⥤ C`, given a cone `c : Cone F`, and a natural isomorphism `α : H ≅ H'` for functors
`H H' : C ⥤ D`, the postcomposition of the cone `H.mapCone` using the isomorphism `α` is
isomorphic to the cone `H'.mapCone`.
 -/
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J C} →
              {H H' : CategoryTheory.Functor C D} →
                (α : H ≅ H') →
                  (c : CategoryTheory.Limits.Cone F) →
                    (CategoryTheory.Limits.Cone.postcompose (F.whiskerLeft α.hom)).obj (H.mapCone c) ≅ H'.mapCone c
-- Mathlib.RingTheory.IntegralDomain
/-- Every finite domain is a division ring. More generally, they are fields; this can be found in
`Mathlib/RingTheory/LittleWedderburn.lean`.  -/
Fintype.divisionRingOfIsDomain : (R : Type u_3) → [inst : Ring R] → [IsDomain R] → [DecidableEq R] → [Fintype R] → DivisionRing R
-- Std.Sync.CancellationToken
Std.CancellationToken.mk : Std.Mutex Std.CancellationToken.State → Std.CancellationToken
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.arrowCongrEquivₛₗ_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  {M₄ : Type u_7} [inst_12 : TopologicalSpace M₄] [inst_13 : AddCommMonoid M₄] [inst_14 : Module R₁ M₁]
  [inst_15 : Module R₂ M₂] [inst_16 : Module R₃ M₃] {R₄ : Type u_8} [inst_17 : Semiring R₄] [inst_18 : Module R₄ M₄]
  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [inst_19 : RingHomInvPair σ₃₄ σ₄₃] [inst_20 : RingHomInvPair σ₄₃ σ₃₄]
  {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [inst_21 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
  [inst_22 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_23 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_24 : SMulCommClass R₃ R₃ M₃]
  [inst_25 : SMulCommClass R₄ R₄ M₄] [inst_26 : ContinuousAdd M₃] [inst_27 : ContinuousConstSMul R₃ M₃]
  [inst_28 : ContinuousAdd M₄] [inst_29 : ContinuousConstSMul R₄ M₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃)
  (a : M₁ →SL[σ₁₄] M₄), ⋯ a = ⋯.toFun a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β},
  compare (Std.ExtDTreeMap.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.Order.Atoms
OrderIso.isCoatomic_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] (f : α ≃o β), IsCoatomic α ↔ IsCoatomic β
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeGroupOfNonempty : ∀ (α : Type u) [Nonempty α], Infinite (FreeGroup α)
-- Lean.Data.PersistentArray
Lean.PersistentArray.filter : {α : Type u} → Lean.PersistentArray α → (α → Bool) → Lean.PersistentArray α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cones_obj_map : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  ((CategoryTheory.cones J C).obj F).map f =
    TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.unop) g
-- Lean.Server.GoTo
Lean.Server.GoToContext.infoTree? : Lean.Server.GoToContext → Option Lean.Elab.InfoTree
-- Init.Data.SInt.Bitwise
Int16.toISize_or : ∀ (a b : Int16), (a ||| b).toISize = a.toISize ||| b.toISize
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_le : ∀ {G : Type u_1} [inst : AddGroup G] {s t : Set G}, s ⊆ t → AddSubgroup.centralizer t ≤ AddSubgroup.centralizer s
-- Mathlib.Topology.Order
coinduced_mono : ∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {f : α → β},
  t₁ ≤ t₂ → TopologicalSpace.coinduced f t₁ ≤ TopologicalSpace.coinduced f t₂
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The restriction of scalars operation is functorial. For any `f : R →+* S` a ring homomorphism,
* an `S`-module `M` can be considered as `R`-module by `r • m = f r • m`
* an `S`-linear map is also `R`-linear
 -/
ModuleCat.restrictScalars : {R : Type u₁} →
  {S : Type u₂} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → CategoryTheory.Functor (ModuleCat S) (ModuleCat R)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_eq' : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (b : α),
  Multiset.filter (fun x => x = b) s = Multiset.replicate (Multiset.count b s) b
-- Mathlib.RingTheory.Teichmuller
Perfection.liftMonoidHom.congr_simp : ∀ (p : ℕ) (M : Type u_2) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (N : Type u_3) [inst_2 : CommMonoid N],
  Perfection.liftMonoidHom p M N = Perfection.liftMonoidHom p M N
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.mk.inj : ∀ {start «end» start_1 end_1 : ℕ},
  { start := start, «end» := «end» } = { start := start_1, «end» := end_1 } → start = start_1 ∧ «end» = end_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodAssoc_apply : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) (P₃ : Type u_4) {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃] (p : (P₁ × P₂) × P₃),
  (AffineEquiv.prodAssoc k P₁ P₂ P₃) p = (p.1.1, p.1.2, p.2)
-- Lean.Server.References
Lean.Server.DirectImports.mk.sizeOf_spec : ∀ (ordered : Array Lean.Server.ModuleImport) (index : Lean.Server.ModuleImportIndex),
  sizeOf { ordered := ordered, index := index } = 1 + sizeOf ordered + sizeOf index
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- A helper structure that bundles the necessary data to
construct a `StrictPseudofunctor`.

`StrictPseudofunctorPreCore` does not construct a Pseudofunctor in general,
since it does not include the compatibility conditions on the associator
and unitors. However, when the underlying bicategories are strict, a
`StrictPseudofunctorPreCore` does induce a `StrictPseudofunctor`.  -/
CategoryTheory.StrictPseudofunctorPreCore : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
        ⟨k, v⟩ ∈ toInsert →
          Std.Internal.List.getValueCastD k' (Std.Internal.List.insertList l toInsert) fallback = cast ⋯ v
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The image of a finite-dimensional affine subspace under an affine map is finite-dimensional.  -/
finiteDimensional_direction_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] (s : AffineSubspace k P) [FiniteDimensional k ↥s.direction] (f : P →ᵃ[k] P₂),
  FiniteDimensional k ↥(AffineSubspace.map f s).direction
-- Mathlib.Analysis.SpecialFunctions.Sqrt
DifferentiableOn.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → (∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℝ (fun y => √(f y)) s
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.norm_rpow : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : NonnegSpectrumClass ℝ A]
  [inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : ℝ},
  0 < r → autoParam (0 ≤ a) CFC.norm_rpow._auto_1 → ‖a ^ r‖ = ‖a‖ ^ r
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.instInhabitedSecondObjBotSieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} → Inhabited (CategoryTheory.Equalizer.Sieve.SecondObj P ⊥)
-- Init.Data.Option.Lemmas
Option.get_merge : ∀ {α : Type u_1} {o o' : Option α} {f : α → α → α} {i : α} [Std.LawfulIdentity f i]
  {h : (Option.merge f o o').isSome = true}, (Option.merge f o o').get h = f (o.getD i) (o'.getD i)
-- Mathlib.CategoryTheory.Category.Cat.Op
/-- The endofunctor `Cat ⥤ Cat` assigning to each category its opposite category.  -/
CategoryTheory.Cat.opFunctor : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.Data.Setoid.Basic
Setoid.piSetoid_apply : ∀ {ι : Sort u_4} {α : ι → Sort u_5} {r : (i : ι) → Setoid (α i)} {x y : (i : ι) → α i},
  piSetoid x y ↔ ∀ (i : ι), (r i) (x i) (y i)
-- Lean.Elab.DocString
Lean.Doc.DocArg.ident.injEq : ∀ (val val_1 : Lean.Ident), (Lean.Doc.DocArg.ident val = Lean.Doc.DocArg.ident val_1) = (val = val_1)
-- Mathlib.CategoryTheory.Simple
CategoryTheory.cokernel_zero_of_nonzero_to_simple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  [CategoryTheory.Simple Y] {f : X ⟶ Y}, f ≠ 0 → CategoryTheory.Limits.cokernel.π f = 0
-- Mathlib.Data.List.Basic
List.getElem?_surjective_iff : ∀ {α : Type u} {l : List α}, (Function.Surjective fun n => l[n]?) ↔ ∀ (x : α), x ∈ l
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.left_inv : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : ContinuousMap.HomotopyEquiv X Y), (self.invFun.comp self.toFun).Homotopic (ContinuousMap.id X)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.ofInjective.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.IsAlgebraic] {f f_1 : L.Hom M N} (e_f : f = f_1) (hf : Function.Injective ⇑f),
  FirstOrder.Language.Embedding.ofInjective hf = FirstOrder.Language.Embedding.ofInjective ⋯
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.parser.inj : ∀ {catName declName : Lean.Name} {leading : Bool} {p : Lean.Parser.Parser} {prio : ℕ} {catName_1 declName_1 : Lean.Name}
  {leading_1 : Bool} {p_1 : Lean.Parser.Parser} {prio_1 : ℕ},
  Lean.Parser.ParserExtension.Entry.parser catName declName leading p prio =
      Lean.Parser.ParserExtension.Entry.parser catName_1 declName_1 leading_1 p_1 prio_1 →
    catName = catName_1 ∧ declName = declName_1 ∧ leading = leading_1 ∧ p = p_1 ∧ prio = prio_1
-- Lean.Server.Utils
Lean.Server.DocumentMeta.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {mod : Lean.Name} {version : ℕ} {text : Lean.FileMap}
  {dependencyBuildMode : Lean.Lsp.DependencyBuildMode} {uri_1 : Lean.Lsp.DocumentUri} {mod_1 : Lean.Name}
  {version_1 : ℕ} {text_1 : Lean.FileMap} {dependencyBuildMode_1 : Lean.Lsp.DependencyBuildMode},
  { uri := uri, mod := mod, version := version, text := text, dependencyBuildMode := dependencyBuildMode } =
      { uri := uri_1, mod := mod_1, version := version_1, text := text_1,
        dependencyBuildMode := dependencyBuildMode_1 } →
    uri = uri_1 ∧ mod = mod_1 ∧ version = version_1 ∧ text = text_1 ∧ dependencyBuildMode = dependencyBuildMode_1
-- Lean.Parser.Extension
Lean.Parser.instCoeForallParserParserAliasValue : Coe (Lean.Parser.Parser → Lean.Parser.Parser) Lean.Parser.ParserAliasValue
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairing_long_short : ∀ {ι : 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 : P.EmbeddedG2], P.pairing (RootPairing.EmbeddedG2.long P) (RootPairing.EmbeddedG2.short P) = -3
-- Init.Data.Vector.Lemmas
Vector.set!_eq_setIfInBounds : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α}, xs.set! i x = xs.setIfInBounds i x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instIsScalarTowerPolynomial : ∀ {K : Type u} [inst : CommRing K] {R : Type u_1} [IsDomain K] [inst_2 : Monoid R]
  [inst_3 : DistribMulAction R (Polynomial K)] [inst_4 : IsScalarTower R (Polynomial K) (Polynomial K)],
  IsScalarTower R (Polynomial K) (RatFunc K)
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.NatTrans.mapHomotopyCategory_comp : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (c : ComplexShape ι) {F G H : CategoryTheory.Functor V W} [inst_4 : F.Additive] [inst_5 : G.Additive]
  [inst_6 : H.Additive] (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) c =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomotopyCategory α c)
      (CategoryTheory.NatTrans.mapHomotopyCategory β c)
-- Mathlib.Order.Hom.BoundedLattice
/-- Copy of a `SupBotHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
SupBotHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Bot α] →
        [inst_2 : Max β] → [inst_3 : Bot β] → (f : SupBotHom α β) → (f' : α → β) → f' = ⇑f → SupBotHom α β
-- Mathlib.Data.Bool.Count
List.count_false_add_count_true : ∀ (l : List Bool), List.count false l + List.count true l = l.length
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Continuous maps out of the one point compactification of `ℕ` to a Hausdorff space `Y` correspond
bijectively to convergent sequences in `Y`.
 -/
OnePoint.continuousMapNatEquiv : (Y : Type u_3) →
  [inst : TopologicalSpace Y] →
    [T2Space Y] → C(OnePoint ℕ, Y) ≃ { f // ∃ L, Filter.Tendsto (fun x => f x) Filter.atTop (nhds L) }
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_val_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Create a `HahnSeries` with a `Finsupp` as coefficients.  -/
HahnSeries.ofFinsupp : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → ZeroHom (Γ →₀ R) (HahnSeries Γ R)