mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- `homₚ` and `hom` need to be compatible with `HomologyPretheory.iso`.  -/
TopPair.HomologyPretheory.Hom.iso_comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (self : HP.Hom HP') (i : ι)
  {Z : CategoryTheory.Functor TopCat C} (h : TopPair.incl.comp (HP'.Hₚ i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HP.iso i).hom
      (CategoryTheory.CategoryStruct.comp (TopPair.incl.whiskerLeft (self.homₚ i)) h) =
    CategoryTheory.CategoryStruct.comp (self.hom i) (CategoryTheory.CategoryStruct.comp (HP'.iso i).hom h)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_eq_false_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.isEmpty = false ↔ ¬m = ∅
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
/-- The affine subspace orthogonal to the radius vector of the sphere `s` at the point `p` (if
`p` lies in `s`, this is the tangent space; generally, this is the polar of the inversion of `p`
in `s`).  -/
EuclideanGeometry.Sphere.orthRadius : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → EuclideanGeometry.Sphere P → P → AffineSubspace ℝ P
-- Mathlib.Data.Fintype.Sets
Set.disjoint_toFinset : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], Disjoint s.toFinset t.toFinset ↔ Disjoint s t
-- Mathlib.FieldTheory.Separable
IntermediateField.isSeparable_tower_bot : ∀ (F : Type u_1) [inst : Field F] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra F K] (M : IntermediateField F K)
  [Algebra.IsSeparable F K], Algebra.IsSeparable F ↥M
-- Lean.Elab.Tactic.Grind.Param
/-- Elaborates `grind` parameters.
`incremental = true` for tactics such as `finish`, in this case, we disable some kinds of parameters
such as `- ident`.
 -/
Lean.Elab.Tactic.elabGrindParams : Lean.Meta.Grind.Params →
  Lean.TSyntaxArray `Lean.Parser.Tactic.grindParam →
    Bool → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Lean.Meta.Grind.Params
-- Mathlib.Algebra.Group.Action.Defs
vadd_vadd : ∀ {M : Type u_1} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (a₁ a₂ : M) (b : α),
  a₁ +ᵥ a₂ +ᵥ b = (a₁ + a₂) +ᵥ b
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.allRealizations : Lean.Environment → Task (Lean.NameMap Lean.AsyncConst✝)
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".
 -/
CategoryTheory.ComonObj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type v₁
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- The inclusion map from the kernel in `TopModuleCat R`.  -/
TopModuleCat.kerι : {R : Type u} →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → {M N : TopModuleCat R} → (φ : M ⟶ N) → TopModuleCat.ker φ ⟶ M
-- Lean.Attributes
Lean.AttributeExtensionState : Type
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.equiv : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : Fintype I] {J : Type u_4} [inst_2 : Fintype J]
  (i : J ≃ I), CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e
-- Lean.Parser.Do
Lean.Parser.Term.doReassign.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceFrom_le_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  String.Slice.Pos.ofSliceFrom p ≤ q ↔ ∃ (h : p₀ ≤ q), p ≤ p₀.sliceFrom q h
-- Mathlib.Order.Closure
/-- Every lower adjoint induces a closure operator given by the composition. This is the partial
order version of the statement that every adjunction induces a monad.  -/
LowerAdjoint.closureOperator : {α : Type u_1} →
  {β : Type u_4} → [inst : PartialOrder α] → [inst_1 : Preorder β] → {u : β → α} → LowerAdjoint u → ClosureOperator α
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
_private.Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct.0.CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan.match_1_3.eq_2 : ∀ (motive : (i j : CategoryTheory.Limits.WalkingPair) → i ≠ j → Sort u_1)
  (hij : CategoryTheory.Limits.WalkingPair.right ≠ CategoryTheory.Limits.WalkingPair.left)
  (h_1 :
    (hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right) →
      motive CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.WalkingPair.right hij)
  (h_2 :
    (hij : CategoryTheory.Limits.WalkingPair.right ≠ CategoryTheory.Limits.WalkingPair.left) →
      motive CategoryTheory.Limits.WalkingPair.right CategoryTheory.Limits.WalkingPair.left hij),
  (match CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left, hij with
    | CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right, hij => h_1 hij
    | CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left, hij => h_2 hij) =
    h_2 hij
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_iInter : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_3} {s : ι → Set α},
  (∀ (i : ι), (s i).OrdConnected) → (⋂ i, s i).OrdConnected
-- Init.Data.Vector.Lemmas
Vector.countP_toArray : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Array.countP p xs.toArray = Vector.countP p xs
-- Mathlib.Tactic.Linarith.Parsing
/-- Variables (represented by natural numbers) map to their power.  -/
Mathlib.Tactic.Linarith.Monom : Type
-- Std.Time.Zoned.ZoneRules
/-- The array of transitions for the time zone.
 -/
Std.Time.TimeZone.ZoneRules.transitions : Std.Time.TimeZone.ZoneRules → Array Std.Time.TimeZone.Transition
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- A sort of triangle inequality.  -/
Set.uIcc_subset_uIcc_union_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
-- Lean.Expr
Lean.Expr.bvar.sizeOf_spec : ∀ (deBruijnIndex : ℕ), sizeOf (Lean.Expr.bvar deBruijnIndex) = 1 + sizeOf deBruijnIndex
-- Init.Data.String.Lemmas.Splits
String.splits_startPos : ∀ (s : String), s.startPos.Splits "" s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (e.counitInv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
      (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ e.functor X Y)
      (e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF)
  {hc : k' ∈ Std.DHashMap.Raw.Const.modify m k f},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.modify m k f) k' hc =
    if heq : (k == k') = true then f (Std.DHashMap.Raw.Const.get m k ⋯) else Std.DHashMap.Raw.Const.get m k' ⋯
-- Init.Data.String.Basic
String.Slice.rawEndPos_copy : ∀ {s : String.Slice}, s.copy.rawEndPos = s.rawEndPos
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.range_mapIncl : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid P]
  [inst_2 : AddCommMonoid Q] [inst_3 : Module R P] [inst_4 : Module R Q] (p : Submodule R P) (q : Submodule R Q),
  (TensorProduct.mapIncl p q).range = Submodule.map₂ (TensorProduct.mk R P Q) p q
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_uIcc : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.uIcc i j = Set.uIcc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given a walk, produces a path with the same endpoints using `SimpleGraph.Walk.bypass`.  -/
SimpleGraph.Walk.toPath : {V : Type u} → {G : SimpleGraph V} → {u v : V} → [DecidableEq V] → G.Walk u v → G.Path u v
-- Init.Data.Dyadic.Basic
Int.trailingZeros_neg : ∀ (x : ℤ), (-x).trailingZeros = x.trailingZeros
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instIsStarNormal : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], IsStarNormal a
-- Init.Data.Int.DivMod.Bootstrap
Int.zero_ediv : ∀ (b : ℤ), 0 / b = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G : C)
  {X Y : C} (f : X ⟶ Y) (j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C).obj G).map f).app j =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft j (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
Subalgebra.perfectClosure.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (p p_1 : ℕ)
  (e_p : p = p_1) [inst_3 : ExpChar A p], Subalgebra.perfectClosure R A p = Subalgebra.perfectClosure R A p_1
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_of_bijective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] {f : G →+ G'},
  Function.Bijective ⇑f → ∀ (H : AddSubgroup G), (AddSubgroup.map f H).index = H.index
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subRight.eq_1 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a : α),
  OrderIso.subRight a = { toEquiv := Equiv.subRight a, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Ring.Equiv
/-- The two paths coercion can take to a `NonUnitalRingEquiv` are equivalent  -/
RingEquiv.toNonUnitalRingHom_commutes : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S), ↑↑f = ↑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ → ∀ (f : α → β → γ), (Std.TreeMap.Raw.map f t₁).Equiv (Std.TreeMap.Raw.map f t₂)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- For all `ε > 0`, we can partition the remainders of any family of polynomials `A`
into classes, where all remainders in a class are close together.  -/
Polynomial.exists_partition_polynomial : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : Polynomial Fq},
      b ≠ 0 →
        ∀ (A : Fin n → Polynomial Fq),
          ∃ t,
            ∀ (i₀ i₁ : Fin n),
              t i₀ = t i₁ → ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
-- Mathlib.Algebra.Homology.HomologicalComplex
_private.Mathlib.Algebra.Homology.HomologicalComplex.0.ChainComplex.mkAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Std.Time.Format.Modifier
Std.Time.Modifier.c.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.c presentation = Std.Time.Modifier.c presentation_1 → presentation = presentation_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false →
        Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff m₂ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property of a function at a point in a charted space, by requiring that it holds
in the preferred chart.  -/
ChartedSpace.LiftPropAt : {H : Type u_1} →
  {M : Type u_2} →
    {H' : Type u_3} →
      {M' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [ChartedSpace H M] →
              [inst : TopologicalSpace H'] →
                [inst_2 : TopologicalSpace M'] →
                  [ChartedSpace H' M'] → ((H → H') → Set H → H → Prop) → (M → M') → M → Prop
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSemilatticeSup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] →
          [HasSolidNorm β] → [IsOrderedAddMonoid β] → SemilatticeSup (BoundedContinuousFunction α β)
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_curry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α × β →₀ M) (p : α → Prop)
  [inst_1 : DecidablePred p], (Finsupp.filter (fun a => p a.1) f).curry = Finsupp.filter p f.curry
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f g : R[X]`. Let `n` be a natural number.
Then `f` can be written in the form `g ^ n * (q + ∑ i : Fin n, r i / g ^ (i + 1))`, where
`degree (r i) < degree g` and the denominator cancels formally.
See `quo_mul_pow_add_sum_rem_mul_pow_unique` for the uniqueness of this representation.  -/
Polynomial.eq_quo_mul_pow_add_sum_rem_mul_pow : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R] (f : Polynomial R) {g : Polynomial R},
  g.Monic → ∀ (n : ℕ), ∃ q r, (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i, r i * g ^ ↑i
-- Mathlib.Control.Fold
Monoid.foldrM.ofFreeMonoid_apply : ∀ {m : Type u → Type u} [inst : Monad m] {α β : Type u} [inst_1 : LawfulMonad m] (f : α → β → m β) (xs : FreeMonoid α)
  (a : CategoryTheory.KleisliCat.mk m β),
  (Monoid.foldrM.ofFreeMonoid f) xs a = flip (List.foldrM f) (FreeMonoid.toList xs) a
-- Mathlib.Algebra.Group.Basic
mul_zsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m n : ℤ), (m * n) • a = m • n • a
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- a sequence of functors  -/
CategoryTheory.Functor.ShiftSequence.sequence : {C : Type u_1} →
  {A : Type u_3} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_3, u_3} A} →
        (F : CategoryTheory.Functor C A) →
          {M : Type u_4} →
            {inst_2 : AddMonoid M} →
              {inst_3 : CategoryTheory.HasShift C M} → [self : F.ShiftSequence M] → M → CategoryTheory.Functor C A
-- Mathlib.Order.BooleanAlgebra.Basic
sup_lt_of_lt_sdiff_left : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y < z \ x → x ≤ z → x ⊔ y < z
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.realSize.eq_1 : ∀ {α : Type u_1}, Batteries.BinomialHeap.Imp.HeapNode.nil.realSize = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s : Finset α), ∅ + s = ∅
-- Init.Data.UInt.Lemmas
UInt8.zero_add : ∀ (a : UInt8), 0 + a = a
-- Mathlib.Data.Nat.Fib.Basic
/-- Subsequent Fibonacci numbers are coprime,
see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime  -/
Nat.fib_coprime_fib_succ : ∀ (n : ℕ), (Nat.fib n).Coprime (Nat.fib (n + 1))
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr₂_left_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : γ → β → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ (List.Vector.mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            have r₂ := f₂ x y s₂;
            have r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressEnd : Lean.ToJson Lean.Lsp.WorkDoneProgressEnd
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `Differentiable.fun_finsetProd`. -/
Differentiable.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, Differentiable 𝕜 (f i)) → Differentiable 𝕜 fun x => ∏ i ∈ u, f i x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- The number of embeddings of a number field is equal to its finrank.  -/
NumberField.Embeddings.card : ∀ (K : Type u_1) [inst : Field K] (A : Type u_2) [inst_1 : Field A] [inst_2 : CharZero A] [inst_3 : NumberField K]
  [IsAlgClosed A], Fintype.card (K →+* A) = Module.finrank ℚ K
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.FixedTermElab : Type
-- Init.Tactics
/-- `mpure` moves a pure hypothesis from the stateful context into the pure context.
```lean
example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
  mintro Hφ
  mpure Hφ
  mexact (ψ Hφ)
```
 -/
Lean.Parser.Tactic.mpureMacro : Lean.ParserDescr
-- Mathlib.Data.Set.Operations
/-- Given a set `s` of functions `α → β` and `t : Set α`, `seq s t` is the union of `f '' t` over
all `f ∈ s`.  -/
Set.seq : {α : Type u} → {β : Type v} → Set (α → β) → Set α → Set β
-- Mathlib.Data.Nat.Bits
Nat.div2.eq_1 : ∀ (n : ℕ), n.div2 = n / 2
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalCommRing : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalCommRing R] → [IsTopologicalRing R] → NonUnitalCommRing (SeparationQuotient R)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.instCovariantClassHSMulLe : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G],
  CovariantClass α (Subgroup G) HSMul.hSMul LE.le
-- Init.Data.List.Lemmas
List.foldl_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : γ → β → γ} {l : List α} {init : γ},
  List.foldl g init (List.filterMap f l) =
    List.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspResponseError : IO.FS.Stream → Lean.JsonRpc.ResponseError Unit → IO Unit
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_ne_one_iff : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] {i : ι} {x : M i},
  Pi.mulSingle i x ≠ 1 ↔ x ≠ 1
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.concat.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (b : α) (h_1 : (b : α) → motive [] b)
  (h_2 : (a : α) → (as : List α) → (b : α) → motive (a :: as) b),
  (match [], b with
    | [], b => h_1 b
    | a :: as, b => h_2 a as b) =
    h_1 b
-- Mathlib.Order.Hom.Basic
OrderHom.comp_coe : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.Indep.insert_isCircuit_of_forall : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  M.Indep I → e ∉ I → e ∈ M.closure I → (∀ f ∈ I, e ∉ M.closure (I \ {f})) → M.IsCircuit (insert e I)
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {x : α} {z : Set β},
  UpperHemicontinuousAt (fun _x => z) x
-- Init.System.IO
/-- File access time.  -/
IO.FS.Metadata.accessed : IO.FS.Metadata → IO.FS.SystemTime
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `weight w d < n`.  -/
MvPowerSeries.le_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ∞},
  (∀ (d : σ →₀ ℕ), ↑((Finsupp.weight w) d) < n → (MvPowerSeries.coeff d) f = 0) → n ≤ MvPowerSeries.weightedOrder w f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x : AddMonoidAlgebra R M),
  (AddMonoidAlgebra.mapDomain f x).coeff = Finsupp.mapDomain f x.coeff
-- Mathlib.Data.Set.Restrict
Set.val_codRestrict_apply : ∀ {α : Type u_1} {ι : Sort u_5} (f : ι → α) (s : Set α) (h : ∀ (x : ι), f x ∈ s) (x : ι),
  ↑(Set.codRestrict f s h x) = f x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.exists_ne_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}, f ≠ 0 → ∃ x, f x ≠ 0
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.Map.instIterator : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [Std.Iterator α m β] →
          {lift : ⦃α : Type w⦄ → m α → n α} →
            {f : β → Std.Iterators.PostconditionT n γ} → Std.Iterator (Std.Iterators.Types.Map α m n lift f) n γ
-- Mathlib.FieldTheory.Perfect
PerfectRing.mk : ∀ {R : Type u_1} {p : ℕ} [inst : Pow R ℕ], (Function.Bijective fun x => x ^ p) → PerfectRing R p
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b), IsNonarchimedean (v.adicAbvDef hb)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictFDerivAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E}
  {x : E},
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt g g' x →
      0 < f x →
        HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
-- Lean.Elab.Tactic.Basic
/-- Like `Meta.withRestoreOrSaveFull` for `TermElabM`, but also takes a `tacSnap?` that
* when running `act`, is set as `Context.tacSnap?`
* otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's
  value.
This extra restore step is necessary because while `reusableResult?` can be used to replay any
effects on `State`, `Context.tacSnap?` is not part of it but changed via an `IO` side effect, so
it needs to be replayed separately.

We use an explicit parameter instead of accessing `Context.tacSnap?` directly because this prevents
`withRestoreOrSaveFull` and `withReader` from being used in the wrong order.
 -/
Lean.Elab.Tactic.withRestoreOrSaveFull : {α : Type} →
  Option (α × Lean.Elab.Tactic.SavedState) →
    Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (α × Lean.Elab.Tactic.SavedState)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_le_one : ∀ {ι : 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] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (x : M), ∑ᶠ (i : ι), (f i) x ≤ 1