mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (W : CategoryTheory.MorphismProperty C) [inst_6 : W.HasLeftCalculusOfFractions]
  [inst_7 : W.IsCompatibleWithTriangulation] [inst_8 : W.HasLocalization] (n : ℤ),
  (CategoryTheory.shiftFunctor W.Localization' n).Additive
-- Mathlib.Data.Bool.Basic
Bool.eq_or_eq_not : ∀ (a b : Bool), a = b ∨ a = !b
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.prev : ∀ {c : Char} {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor (c :: l) r it → String.Legacy.Iterator.ValidFor l (c :: r) it.prev
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.alt.injEq : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i j : ι) (hm : m i = m j) (hij : i ≠ j) (m_1 : ι → M)
  (i_1 j_1 : ι) (hm_1 : m_1 i_1 = m_1 j_1) (hij_1 : i_1 ≠ j_1),
  (exteriorPower.presentation.Rels.alt m i j hm hij = exteriorPower.presentation.Rels.alt m_1 i_1 j_1 hm_1 hij_1) =
    (m = m_1 ∧ i = i_1 ∧ j = j_1)
-- Mathlib.CategoryTheory.EpiMono
/-- The section of a split epimorphism is itself a split monomorphism.  -/
CategoryTheory.section_isSplitMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsSplitEpi f], CategoryTheory.IsSplitMono (CategoryTheory.section_ f)
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_inv_inv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G),
  dist a⁻¹ b⁻¹ = dist a b
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If `f : X → Y` is an `IsUniformEmbedding`, the image `f '' s` of a set `s` is complete
if and only if `s` is complete.  -/
IsUniformEmbedding.isComplete_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  IsUniformEmbedding f → (IsComplete (f '' s) ↔ IsComplete s)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.alternatingMapLinearEquiv_symm_apply : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (F : ↥(⋀[R]^n M) →ₗ[R] N) (m : Fin n → M),
  (exteriorPower.alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (exteriorPower.ιMulti R n)) m
-- Mathlib.Data.Finmap
Finmap.dlookup_list_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : List (Sigma β)),
  Finmap.lookup a s.toFinmap = List.dlookup a s
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_baseSet : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K), (e.pullback f).baseSet = ⇑f ⁻¹' e.baseSet
-- Mathlib.Control.Functor
/-- `Const α` is the constant functor, mapping every type to `α`. When
`α` has a monoid structure, `Const α` has an `Applicative` instance.
(If `α` has an additive monoid structure, see `Functor.AddConst`.)  -/
Functor.Const : Type u_1 → Type u_2 → Type u_1
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
isTranscendenceBasis_subtype_range : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {f : ι → A}, Function.Injective f → (IsTranscendenceBasis R Subtype.val ↔ IsTranscendenceBasis R f)
-- Mathlib.CategoryTheory.CommSq
/-- The proposition that a square
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

```
is a commuting square.
 -/
CategoryTheory.CommSq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {W X Y Z : C} → (W ⟶ X) → (W ⟶ Y) → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective R]
  (X : (CategoryTheory.reflectorAdjunction R).toMonad.Algebra),
  CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction R).unit.app X.A)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mk.injEq : ∀ {C : Type u} (as as_1 : C), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).size =
    if k ∈ m ∧ (f (Std.ExtDHashMap.Const.get? m k)).isNone = true then m.size - 1
    else if k ∉ m ∧ (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then m.size + 1 else m.size
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- representation function for dependent sums  -/
MvQPF.Sigma.repr : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) →
      [inst : (α : A) → MvQPF (F α)] → ⦃α : TypeVec.{u} n⦄ → MvQPF.Sigma F α → ↑(MvQPF.Sigma.P F) α
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Module.finBasisOfFinrankEq.congr_simp : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M] {n : ℕ}
  (hn : Module.finrank R M = n), Module.finBasisOfFinrankEq R M hn = Module.finBasisOfFinrankEq R M hn
-- Init.System.FilePath
/-- Joins a list of paths into a suitable value for the current platform's `$PATH` (or `%PATH%`)
environment variable.
 -/
System.SearchPath.toString : System.SearchPath → String
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork
diagram of the Stacks entry.  -/
CategoryTheory.Presheaf.forkMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {U : C} →
          (R : CategoryTheory.Presieve U) →
            (P : CategoryTheory.Functor Cᵒᵖ A) →
              [inst_2 : CategoryTheory.Limits.HasProducts A] →
                P.obj (Opposite.op U) ⟶ CategoryTheory.Presheaf.firstObj R P
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- The inclusion of an open subset `s` of a space `X` into `X` is an open partial homeomorphism
from the subtype `s` to `X`.  -/
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe : {X : Type u_1} →
  [inst : TopologicalSpace X] → (s : TopologicalSpace.Opens X) → Nonempty ↥s → OpenPartialHomeomorph (↥s) X
-- Mathlib.Order.ModularLattice
IsModularLattice.isModularLattice_Ici : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a : α}, IsModularLattice ↑(Set.Ici a)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_mk : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f),
  { toLinearMap := f, isIntertwining' := h }.toLinearMap = f
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_zero : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : LT α] [inst_1 : Zero R], Matrix.BlockTriangular 0 b
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.integrable_comp_snd_map_prodMk_iff : ∀ {β : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] {mβ : MeasurableSpace β} {Ω : Type u_5}
  {x : MeasurableSpace Ω} {X : Ω → β} {μ : MeasureTheory.Measure Ω},
  Measurable X →
    ∀ {f : Ω → F},
      MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) ↔
        MeasureTheory.Integrable f μ
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.memSobolev_besselPotential_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s r : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)]
  {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s p ((TemperedDistribution.besselPotential E F r) f) ↔
    TemperedDistribution.MemSobolev (r + s) p f
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.join_join : ∀ {α : Type u} (SS : Stream'.WSeq (Stream'.WSeq (Stream'.WSeq α))),
  SS.join.join ~ʷ (Stream'.WSeq.map Stream'.WSeq.join SS).join
-- Lean.Meta.FunInfo
Lean.Meta.getFunInfo : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.FunInfo
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_of_mem_orbit_submonoid : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {S : Submonoid M} {a b : α},
  a ∈ MulAction.orbit (↥S) b → a ∈ MulAction.orbit M b
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ : AlgebraicGeometry.Scheme.Γ.IsRightAdjoint
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- `ζ - 1` is prime if `ζ` is a primitive `p ^ (k + 1)`-th root of unity.  -/
IsPrimitiveRoot.zeta_sub_one_prime : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))), Prime (hζ.toInteger - 1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonAddHom.eq_1 : ∀ {α : Type u_2} [inst : Add α], Set.singletonAddHom = { toFun := singleton, map_add' := ⋯ }
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = none ↔ t.contains k = false
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.elabDoElemFns : Lean.DoElem →
  Lean.Elab.Do.DoElemCont →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Do.DoElab) →
      optParam Bool true → Lean.Elab.Do.DoElabM Lean.Expr
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_1 : HSub Std.Time.DateTime Std.Time.Week.Offset Std.Time.DateTime
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.instHasFactorizationInverseImageOfIsEquivalenceOfRespectsIso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  (F : CategoryTheory.Functor D C) [F.IsEquivalence] [W₁.RespectsIso] [W₂.RespectsIso] [W₁.HasFactorization W₂],
  (W₁.inverseImage F).HasFactorization (W₂.inverseImage F)
-- Init.Data.Option.Lemmas
Option.getD_or : ∀ {α : Type u_1} {o o' : Option α} {fallback : α}, (o.or o').getD fallback = o.getD (o'.getD fallback)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radicalInfTopHom_apply : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), Ideal.radicalInfTopHom I = I.radical
-- Mathlib.Data.Set.Monotone
Function.antitoneOn_of_rightInvOn_of_mapsTo : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β}
  {s : Set α}, AntitoneOn φ t → Set.RightInvOn ψ φ s → Set.MapsTo ψ s t → AntitoneOn ψ s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.lift_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (F : CliffordAlgebra Q →ₐ[R] A),
  (CliffordAlgebra.lift Q).symm F = ⟨F.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Free groups are torsion-free, i.e., taking powers is injective. Our proof idea is as follows:
if `x ^ n = y ^ n`, then also `x ^ (2 * n) = y ^ (2 * n)`. We then compare the reduced words
representing the powers in terms of the cyclic reductions of `x.toWord` and `y.toWord` using
`reduce_flatten_replicate`. We conclude that the cyclic reductions of `x.toWord` and `y.toWord` must
have the same length, and in fact they have to agree.  -/
FreeGroup.instIsMulTorsionFree : ∀ {α : Type u}, IsMulTorsionFree (FreeGroup α)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_1 : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  ν ≤ n →
    Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) =
      (-1) ^ (n - ν) * Polynomial.eval (↑ν + 1) (ascPochhammer R (n - ν))
-- Init.Data.BitVec.Bitblast
/-- If `x &&& y = 0`, then the carry bit `(x + y + 0)` is always `false` for any index `i`.
Intuitively, this is because a carry is only produced when at least two of `x`, `y`, and the
previous carry are true. However, since `x &&& y = 0`, at most one of `x, y` can be true,
and thus we never have a previous carry, which means that the sum cannot produce a carry.
 -/
BitVec.carry_of_and_eq_zero : ∀ {w i : ℕ} {x y : BitVec w}, x &&& y = 0#w → BitVec.carry i x y false = false
-- Lean.Expr
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`.  -/
Lean.Expr.withApp : {α : Sort u_1} → Lean.Expr → (Lean.Expr → Array Lean.Expr → α) → α
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instIsCharPQOfAddRightCancel : ∀ {α : Type u} {p : ℕ} [inst : Lean.Grind.Semiring α] [Lean.Grind.AddRightCancel α] [Lean.Grind.IsCharP α p],
  Lean.Grind.IsCharP (Lean.Grind.Ring.OfSemiring.Q α) p
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- The quotient of a module `M` by a submodule `p ⊆ M`.  -/
Submodule.hasQuotient : {R : Type u_1} →
  {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → HasQuotient M (Submodule R M)
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α]
  (a : Subtype p),
  (∀ ⦃a x : α⦄, a ≤ x → p a → p x) → Finset.map (Function.Embedding.subtype p) (Finset.Ioi a) = Finset.Ioi ↑a
-- Mathlib.Data.Finset.Lattice.Basic
Finset.instCommutativeUnion : ∀ {α : Type u_1} [inst : DecidableEq α], Std.Commutative fun x1 x2 => x1 ∪ x2
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_iSup_of_directed : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} [Nonempty ι] {S : ι → Subgroup G},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.Order.Monotone.Monovary
monovaryOn_comm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s ↔ MonovaryOn g f s
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mem_chartAt_ind_source : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M)
  (hx : x ∈ s), x ∈ (chartAt H (fs.c (fs.ind x hx))).source
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, k ∈ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl
-- Mathlib.LinearAlgebra.Matrix.Diagonal
Matrix.proj_diagonal : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type v} [inst_2 : CommSemiring R] (i : n) (w : n → R),
  LinearMap.proj i ∘ₗ Matrix.toLin' (Matrix.diagonal w) = w i • LinearMap.proj i
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Polynomial evaluation commutes with `Finset.prod`
 -/
Polynomial.eval_prod : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R),
  Polynomial.eval x (∏ j ∈ s, p j) = ∏ j ∈ s, Polynomial.eval x (p j)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termY₂ : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.support_finsetSum : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} [inst : DecidableEq β] [inst_1 : AddCommMonoid M] {s : Finset α}
  {f : α → β →₀ M}, (s.sum f).support ⊆ s.biUnion fun x => (f x).support
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.match_1.splitter : {α : Type u_1} →
  (xs : Array α) →
    (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) →
      (x : ℕ) →
        (x_1 : x ≤ xs.size) →
          ((x : 0 ≤ xs.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h) → motive x x_1
-- Init.Data.SInt.Bitwise
UInt32.toInt32_and : ∀ (a b : UInt32), (a &&& b).toInt32 = a.toInt32 &&& b.toInt32
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderiv_continuousAlternatingMap_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  [inst_7 : Fintype ι],
  DifferentiableAt 𝕜 c x → ∀ (u : ι → F), fderiv 𝕜 (fun y => (c y) u) x = (fderiv 𝕜 c x).flipAlternating u
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- For any sum along `{0, ..., n - 1}` of a commutative-monoid-valued function, we
can verify that it's equal to a different function just by checking differences of adjacent terms
up to `n`.

This is a discrete analogue of the fundamental theorem of calculus.  -/
Finset.sum_range_induction : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f s : ℕ → M),
  s 0 = 0 → ∀ (n : ℕ), (∀ k < n, s (k + 1) = s k + f k) → ∑ k ∈ Finset.range n, f k = s n
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Notation `log⁺` for the positive part of the logarithm.  -/
Real.«termLog⁺» : Lean.ParserDescr
-- Mathlib.Data.Matrix.Basic
LinearEquiv.mapMatrix_toLinearMap : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [inst_6 : RingHomInvPair σᵣₛ σₛᵣ]
  [inst_7 : RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β), ↑f.mapMatrix = (↑f).mapMatrix
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_injective_of_injective : ∀ {n : ℕ} {α : Type u_1} {x₀ : α} {x : Fin n → α},
  x₀ ∉ Set.range x → Function.Injective x → Function.Injective (Fin.cons x₀ x)
-- Mathlib.Order.Heyting.Basic
sup_le_of_le_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ c \ b → b ≤ c → a ⊔ b ≤ c
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.op_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y), φ.op.s = φ.s.op
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α} {h : k ∈ Std.HashSet.filter f m}, (Std.HashSet.filter f m).get k h = m.get k ⋯
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.toSlashInvariantForm_coe : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : CuspForm Γ k), ⇑f.toSlashInvariantForm = ⇑f
-- Lean.Language.Basic
/-- General elaboration metadata produced by this step.  -/
Lean.Language.Snapshot.infoTree? : Lean.Language.Snapshot → Option Lean.Elab.InfoTree
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapFun.eq_1 : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier)
  (s : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x) (y : ↥V),
  AlgebraicGeometry.StructureSheaf.comapFun f U V hUV s y =
    (AlgebraicGeometry.StructureSheaf.Localizations.comapFun f ↑y) (s ⟨PrimeSpectrum.comap σ ↑y, ⋯⟩)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.maxKey? (Std.Internal.List.modifyKey k f l) = Std.Internal.List.maxKey? l
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (m : ℕ) → motive m.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | m.succ.succ => h_3 m) =
    h_1 ()
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_ae : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
      μ.restrict (⋃ i, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s i)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A submodule contained in a finite-dimensional submodule is
finite-dimensional.  -/
Submodule.finiteDimensional_of_le : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂], S₁ ≤ S₂ → FiniteDimensional K ↥S₁
-- Mathlib.Analysis.Distribution.Distribution
Distribution.instLineDerivLeftSMulRealTopENat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F], LineDerivLeftSMul ℝ E (Distribution Ω F ⊤) (Distribution Ω F ⊤)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.toLocalizationMap_sec : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  (IsLocalization.toLocalizationMap M S).sec = IsLocalization.sec M
-- Mathlib.Algebra.BigOperators.Finprod
hasFiniteMulSupport_of_finprod_ne_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, ∏ᶠ (i : α), f i ≠ 1 → Function.HasFiniteMulSupport f
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_le : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0}, ↑p ≤ ↑q ↔ p ≤ q