mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.eventually_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  HasFPowerSeriesAt f 0 x → ∀ᶠ (z : E) in nhds x, f z = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H2Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H2Iso A =
    (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 2).leftHomologyIso.symm ≪≫
      CategoryTheory.ShortComplex.leftHomologyMapIso' (groupHomology.isoShortComplexH2 A)
        (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 2).leftHomologyData
        (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData
-- Mathlib.Topology.Order.Basic
/-- An order-theoretically right-continuous function is topologically right-continuous, assuming
the function is between conditionally complete linear orders with order topologies.  -/
RightOrdContinuous.continuousWithinAt_Ici : ∀ {X : Type u_1} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X]
  {Y : Type u_2} [inst_3 : ConditionallyCompleteLinearOrder Y] [inst_4 : TopologicalSpace Y] [OrderTopology Y]
  {f : X → Y} {x : X}, RightOrdContinuous f → ContinuousWithinAt f (Set.Ici x) x
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- All functors `F : J ⥤ C` from all small `J` have limits  -/
CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f = g` on some neighbourhood of `x`,
then `f` is an immersion at `x` if and only if `g` is an immersion at `x`.  -/
Manifold.IsImmersionAtOfComplement.congr_iff_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M},
  f =ᶠ[nhds x] g → (Manifold.IsImmersionAtOfComplement F I J n f x ↔ Manifold.IsImmersionAtOfComplement F I J n g x)
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- Characterization of uniform equicontinuity for families of functions taking values in a
(pseudo) metric space.  -/
Metric.uniformEquicontinuous_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F ↔ ∀ ε > 0, ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), dist (F i xy.1) (F i xy.2) < ε
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.value : {α : Type} → Lean.Lsp.ProgressParams α → α
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pair_add : ∀ {α : Type u_2} [inst : Add α] (a b : α) (s : Set α), {a, b} + s = (a +ᵥ s) ∪ (b +ᵥ s)
-- Init.Tactics
/-- `solve_by_elim` calls `apply` on the main goal to find an assumption whose head matches
and then repeatedly calls `apply` on the generated subgoals until no subgoals remain,
performing at most `maxDepth` (defaults to 6) recursive steps.

`solve_by_elim` discharges the current goal or fails.

`solve_by_elim` performs backtracking if subgoals can not be solved.

By default, the assumptions passed to `apply` are the local context, `rfl`, `trivial`,
`congrFun` and `congrArg`.

The assumptions can be modified with similar syntax as for `simp`:
* `solve_by_elim [h₁, h₂, ..., hᵣ]` also applies the given expressions.
* `solve_by_elim only [h₁, h₂, ..., hᵣ]` does not include the local context,
  `rfl`, `trivial`, `congrFun`, or `congrArg` unless they are explicitly included.
* `solve_by_elim [-h₁, ... -hₙ]` removes the given local hypotheses.
* `solve_by_elim using [a₁, ...]` uses all lemmas which have been labelled
  with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).

`solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal
makes other goals impossible.
(Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)

Optional arguments passed via a configuration argument as `solve_by_elim (config := { ... })`
- `maxDepth`: number of attempts at discharging generated subgoals
- `symm`: adds all hypotheses derived by `symm` (defaults to `true`).
- `exfalso`: allow calling `exfalso` and trying again if `solve_by_elim` fails
  (defaults to `true`).
- `transparency`: change the transparency mode when calling `apply`. Defaults to `.default`,
  but it is often useful to change to `.reducible`,
  so semireducible definitions will not be unfolded when trying to apply a lemma.

See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options
`proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
Both `apply_assumption` and `apply_rules` are implemented via these hooks.
 -/
Lean.Parser.Tactic.solveByElim : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Mixin for a `VectorBundleCore` stating that transition functions are `C^n`.  -/
VectorBundleCore.IsContMDiff : {𝕜 : Type u_1} →
  {B : Type u_2} →
    {F : Type u_4} →
      [inst : NontriviallyNormedField 𝕜] →
        {EB : Type u_7} →
          [inst_1 : NormedAddCommGroup EB] →
            [inst_2 : NormedSpace 𝕜 EB] →
              {HB : Type u_8} →
                [inst_3 : TopologicalSpace HB] →
                  [inst_4 : TopologicalSpace B] →
                    [ChartedSpace HB B] →
                      [inst_6 : NormedAddCommGroup F] →
                        [inst_7 : NormedSpace 𝕜 F] →
                          {ι : Type u_11} → VectorBundleCore 𝕜 B F ι → ModelWithCorners 𝕜 EB HB → WithTop ℕ∞ → Prop
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instInhabited : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Inhabited (Std.ExtTreeMap α β cmp)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_add : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {f g : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ →
    MeasureTheory.Integrable (⇑g) μ →
      MeasureTheory.SimpleFunc.integral μ (f + g) =
        MeasureTheory.SimpleFunc.integral μ f + MeasureTheory.SimpleFunc.integral μ g
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.limsup_sub_const : ∀ {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) (c : ENNReal),
  Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
-- Mathlib.Topology.Algebra.Monoid
continuousOn_nsmul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] {s : Set M} (n : ℕ),
  ContinuousOn (fun x => n • x) s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {fallback : α}, t.getKeyD (t.maxKey he) fallback = t.maxKey he
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- Variant of `algebraicIndependent_of_finite` using `Transcendental`.  -/
algebraicIndependent_of_finite' : ∀ {R : Type u_3} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A),
  Function.Injective ⇑(algebraMap R A) →
    (∀ t ⊆ s,
        t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(Algebra.adjoin R t)) a) →
      AlgebraicIndependent R Subtype.val
-- Mathlib.Topology.Path
Path.inv.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : Inv X] [inst_2 : ContinuousInv X] (γ : Path a b),
  γ.inv = γ.map ⋯
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.memLp_prod_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : X → E × F},
  MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp (fun x => (f x).1) p μ ∧ MeasureTheory.MemLp (fun x => (f x).2) p μ
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.ofNat_succ : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : ℕ),
  Lean.Grind.Ring.OfSemiring.natCast (a + 1) =
    Lean.Grind.Ring.OfSemiring.add (Lean.Grind.Ring.OfSemiring.natCast a) (Lean.Grind.Ring.OfSemiring.natCast 1)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_pos_iff : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ],
  0 < ProbabilityTheory.mgf X μ t ↔ MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Std.Time.Date.Unit.Month
Std.Time.Month.Ordinal.days_gt_27 : ∀ (leap : Bool) (i : Std.Time.Month.Ordinal), Std.Time.Month.Ordinal.days leap i > 27
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.derivative_U_eval_one_dvd : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] (n : ℤ), 3 ∣ (↑n + 2) * (↑n + 1) * ↑n
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCancelCommMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCancelCommMonoid (f i)],
  Pi.addCancelCommMonoid = { toAddMonoid := Pi.addLeftCancelMonoid.toAddMonoid, add_comm := ⋯, toIsLeftCancelAdd := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- Implementation: If each structured arrow category on `G` has an initial object, an equivalence
which is helpful for constructing a left adjoint to `G`.
 -/
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] →
            (A : C) → (B : D) → ((⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B) ≃ (A ⟶ G.obj B)
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.prodAdditive_symm_apply : ∀ (G : Type u_2) (H : Type u_3) [inst : Mul G] [inst_1 : Mul H] (x : Additive G × Additive H),
  (AddEquiv.prodAdditive G H).symm x =
    match x with
    | (x, y) => Additive.ofMul (Additive.toMul x, Additive.toMul y)
-- Mathlib.Tactic.NormNum.Result
/-- Extract the raw natlit representing the absolute value of a raw integer literal
(of the type produced by `Mathlib.Meta.NormNum.mkRawIntLit`) along with an equality proof.  -/
Mathlib.Meta.NormNum.rawIntLitNatAbs : (n : Q(ℤ)) → (m : Q(ℕ)) × Q(«$n».natAbs = «$m»)
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.instMembershipOfLT : {α : Type u} → [LT α] → Membership α (Std.Roi α)
-- Mathlib.Algebra.Order.Algebra
algebraMap_mono : ∀ {α : Type u_1} (β : Type u_2) [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [SMulPosMono α β], Monotone ⇑(algebraMap α β)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k k' : α}, t.getKey? k = some k' → (Std.TreeMap.filter f t)[k]? = Option.filter (fun x => f k' x) t[k]?
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_inv_mul_right_singleton : ∀ {α : Type u_2} [inst : Group α] {a b : α}, (fun x => x⁻¹ * a) ⁻¹' {b} = {a / b}
-- Mathlib.Topology.Constructible
Topology.IsConstructible.union : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsConstructible s → Topology.IsConstructible t → Topology.IsConstructible (s ∪ t)
-- Init.Data.SInt.Basic
instAndOpInt8 : AndOp Int8
-- Mathlib.Data.Num.Bitwise
/-- Add a bit at the end of a `SNum`. This mimics `NzsNum.bit`.  -/
SNum.bit : Bool → SNum → SNum
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- The product of two completely pseudometrizable spaces is completely pseudometrizable.  -/
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X]
  [inst_2 : TopologicalSpace Y] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace (X × Y)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_iff_norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β), MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.setPreimage_apply : ∀ {α : Type u_2} {β : Type u_3} (f : α → β) (s : Set β), (CompleteLatticeHom.setPreimage f) s = f ⁻¹' s
-- Lean.Elab.Term.TermElabM
/-- `true` when elaborating patterns. It affects how we elaborate named holes.  -/
Lean.Elab.Term.Context.inPattern : Lean.Elab.Term.Context → Bool
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.closure_eq : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] {s : ClosedSubmodule R M},
  (↑s).closure = s
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.comp_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ S₃ : CategoryTheory.SimplicialObject.Split C}
  (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) (n : ℕ),
  (CategoryTheory.CategoryStruct.comp Φ₁₂ Φ₂₃).f n = CategoryTheory.CategoryStruct.comp (Φ₁₂.f n) (Φ₂₃.f n)
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_getMsbD : ∀ {w : ℕ} {x : BitVec w} {i : ℕ}, x.getMsbD i = true → i < w
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_filter_piFinset_const : ∀ {ι : Type u_4} {κ : Type u_5} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] (s : Finset κ)
  (i : ι) (j : κ), {f ∈ Fintype.piFinset fun x => s | f i = j}.card = if j ∈ s then s.card ^ (Fintype.card ι - 1) else 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.mk.sizeOf_spec : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing N] [inst_2 : LieAlgebra R N]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : SizeOf R] [inst_6 : SizeOf N] [inst_7 : SizeOf M]
  (L : Type u_5) (instLieRing : LieRing L) (instLieAlgebra : LieAlgebra R L) (incl : N →ₗ⁅R⁆ L) (proj : L →ₗ⁅R⁆ M)
  (IsExtension : LieAlgebra.IsExtension incl proj),
  sizeOf
      { L := L, instLieRing := instLieRing, instLieAlgebra := instLieAlgebra, incl := incl, proj := proj,
        IsExtension := IsExtension } =
    1 + sizeOf L + sizeOf instLieRing + sizeOf instLieAlgebra + sizeOf incl + sizeOf proj + sizeOf IsExtension
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.isIndContained_iff_exists_iso_subgraph`. -/
SimpleGraph.IsIndContained.of_exists_iso_subgraph : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, (∃ H' _e, H'.IsInduced) → G.IsIndContained H
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  ∃ Q, ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.mul_log_strictMonoOn : StrictMonoOn (fun x => x * Real.log x) (Set.Ici (Real.exp (-1)))
-- Mathlib.GroupTheory.Congruence.Defs
/-- The negation induced on the quotient by an additive congruence relation on a type
with a negation.  -/
AddCon.hasNeg : {M : Type u_1} → [inst : AddGroup M] → (c : AddCon M) → Neg c.Quotient
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
/-- For any `w`-small type `X`, there exists a regular cardinal `κ : Cardinal.{w}`
such that `HasCardinalLT X κ`.  -/
HasCardinalLT.exists_regular_cardinal : ∀ (X : Type u) [Small.{w, u} X], ∃ κ, κ.IsRegular ∧ HasCardinalLT X κ
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.center_le_centralizer : ∀ {R : Type u_1} [inst : NonUnitalRing R] (s : Set R), NonUnitalSubring.center R ≤ NonUnitalSubring.centralizer s
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.pi : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → AddMonoid (α i)] {x : (i : ι) → α i} [Finite ι],
  (∀ (i : ι), IsOfFinAddOrder (x i)) → IsOfFinAddOrder x
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_eq_pow_single : ∀ {M : Type u_4} [inst : Monoid M] {l : List M} [inst_1 : DecidableEq M] (a : M),
  (∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1) → l.prod = a ^ List.count a l
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.mono_iff_injective : ∀ {A B : AddGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Combinatorics.HalesJewett
/-- The type of combinatorial subspaces. A subspace `l : Subspace η α ι` in the hypercube `ι → α`
defines a function `(η → α) → ι → α` from `η → α` to the hypercube, such that for each coordinate
`i : ι` and direction `e : η`, the function `fun x ↦ l x i` is either `fun x ↦ x e` for some
direction `e : η` or constant. We require subspaces to be non-degenerate in the sense that, for
every `e : η`, `fun x ↦ l x i` is `fun x ↦ x e` for at least one `i`.

Formally, a subspace is represented by a word `l.idxFun : ι → α ⊕ η` which says whether
`fun x ↦ l x i` is `fun x ↦ x e` (corresponding to `l.idxFun i = Sum.inr e`) or constantly `a`
(corresponding to `l.idxFun i = Sum.inl a`).

When `α` has size `1` there can be many elements of `Subspace η α ι` defining the same function.  -/
Combinatorics.Subspace : Type u_5 → Type u_6 → Type u_7 → Type (max (max u_5 u_6) u_7)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α} {x : α}, x ∈ -s ↔ ∃ y ∈ s, -y = x
-- Init.Data.Array.Lemmas
Array.foldr_eq_foldr_extract : ∀ {α : Type u_1} {β : Type u_2} {start stop : ℕ} {xs : Array α} {f : α → β → β} {init : β},
  Array.foldr f init xs start stop = Array.foldr f init (xs.extract stop start)
-- Init.Data.List.Attach
List.length_attachWith : ∀ {α : Type u_1} {p : α → Prop} {l : List α} {H : ∀ x ∈ l, p x}, (l.attachWith p H).length = l.length
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- In a ring the companion bilinear form is unique and equal to `QuadraticMap.polar`.  -/
QuadraticMap.choose_exists_companion : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N), ⋯.choose = Q.polarBilin
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.right_inl : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (q : Q), (RegularWreathProduct.inl q).right = q
-- Mathlib.Data.Rel
SetRel.image_id : ∀ {α : Type u_1} (s : Set α), SetRel.id.image s = s
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.top_lowerCentralSeries_one`. -/
Subgroup.lowerCentralSeries_one : ∀ {G : Type u_1} [inst : Group G], ⊤.lowerCentralSeries 1 = commutator G
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.getCommandSuggestions : LeanSearchClient.SearchServer → String → ℕ → Lean.MetaM (Array Lean.Meta.Tactic.TryThis.Suggestion)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment : Std.Tactic.BVDecide.BVExpr.Assignment → Std.Tactic.BVDecide.BVBit → Bool
-- Mathlib.Data.Nat.Totient
Nat.totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.logTaylor_zero : Complex.logTaylor 0 = fun x => 0
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Interpret `Finsupp.subtypeDomain s` as a linear map.  -/
Finsupp.lsubtypeDomain : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (s : Set α) → (α →₀ M) →ₗ[R] ↑s →₀ M
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIsoAt_ιTruncLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n q : ℤ), q ≤ n → QuasiIsoAt (K.ιTruncLE n) q
-- Init.Data.List.OfFn
List.mem_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} {a : α}, a ∈ List.ofFn f ↔ ∃ i, f i = a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.veq_refl`. -/
ValuativeRel.veq.refl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x =ᵥ x
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_map₂ : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) {a b : B} {f g : a ⟶ b}
  (a_1 : f ⟶ g), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map₂ a_1 = (F' a b).map a_1
-- Aesop.Stats.Basic
Aesop.Stats : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_inter_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = true →
          Std.DHashMap.Internal.Raw₀.Const.get! (m₁.inter m₂) k = Std.DHashMap.Internal.Raw₀.Const.get! m₁ k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKeyD k' fallback = k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.edges = List.map SimpleGraph.Dart.edge p.darts
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofIntClamp : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofIntClamp n).toInt16 = Int16.ofInt n
-- Mathlib.Data.Multiset.Find
Multiset.find?_coe : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α) (hp : {x | x ∈ ↑l ∧ p x}.Subsingleton),
  Multiset.find? p (↑l) hp = List.find? (fun a => decide (p a)) l
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.noncommPiCoprod_range : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y},
  (AddSubgroup.noncommPiCoprod hcomm).range = ⨆ i, H i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- If a subgraph is locally finite at a vertex, then so are subgraphs of that subgraph.

This is not an instance because `G''` cannot be inferred.  -/
SimpleGraph.Subgraph.finiteAtOfSubgraph : {V : Type u} →
  {G : SimpleGraph V} →
    {G' G'' : G.Subgraph} →
      [DecidableRel G'.Adj] →
        G' ≤ G'' → (v : ↑G'.verts) → [Fintype ↑(G''.neighborSet ↑v)] → Fintype ↑(G'.neighborSet ↑v)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_restrict_subset : ∀ {α : Type u} {X Y : Set α} (M : Matroid α), Y ⊆ X → (M.restrict X).cRk Y = M.cRk Y