mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (m n : ℤ)
  (hmn :
    autoParam (m + n = 0) CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app._auto_1),
  (CategoryTheory.shiftFunctor Cᵒᵖ m).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app
        ((CategoryTheory.shiftFunctor Cᵒᵖ m).obj (Opposite.op X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
          ((CategoryTheory.shiftFunctor C n).map
              ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop).op)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).inv.app
              (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X))))
          ((CategoryTheory.shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X)))))
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.le_iff_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] {x : A} {s : NonUnitalSubalgebra R A},
  IsClosed ↑s → (NonUnitalAlgebra.elemental R x ≤ s ↔ x ∈ s)
-- Mathlib.Order.Filter.CountableInter
countableInterFilter_principal : ∀ {α : Type u_2} (s : Set α), CountableInterFilter (Filter.principal s)
-- Mathlib.RingTheory.PowerSeries.Order
/-- Given a non-zero power series `f`, `divXPowOrder f` is the power series obtained by
dividing out the largest power of X that divides `f`, that is its order  -/
PowerSeries.divXPowOrder : {R : Type u_1} → [Semiring R] → PowerSeries R → PowerSeries R
-- Mathlib.Topology.EMetricSpace.Defs
Metric.pos_of_mem_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε → 0 < ε
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If a property of maps of topological spaces is satisfied by homeomorphisms and is stable
under composition, the induced property on schemes respects isomorphisms.  -/
AlgebraicGeometry.topologically_respectsIso : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop),
  (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f) →
    (∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
        (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)) →
      (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplFunctor_obj : ∀ {V : Type u} (G : SimpleGraph V) (K : (Finset V)ᵒᵖ),
  G.componentComplFunctor.obj K = G.ComponentCompl ↑(Opposite.unop K)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The closed `n`-cell given by the index `i`. Use this instead of `map n i '' closedBall 0 1`
whenever possible.  -/
Topology.RelCWComplex.closedCell : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → (n : ℕ) → Topology.RelCWComplex.cell C n → Set X
-- Mathlib.Order.Filter.Pointwise
Filter.pure_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {g : Filter β} {a : β}, pure a -ᵥ g = Filter.map (fun x => a -ᵥ x) g
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticAt : ∀ {𝕜 : 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] (f : E →L[𝕜] F)
  (x : E), AnalyticAt 𝕜 (⇑f) x
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_nsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoDiv hp a (m • p + b) = ↑m + toIcoDiv hp a b
-- Mathlib.Lean.Meta.CongrTheorems
/-- Driver for `trySolveCore`.  -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.trySolve : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.SubExpr
Lean.SubExpr.mk.inj : ∀ {expr : Lean.Expr} {pos : Lean.SubExpr.Pos} {expr_1 : Lean.Expr} {pos_1 : Lean.SubExpr.Pos},
  { expr := expr, pos := pos } = { expr := expr_1, pos := pos_1 } → expr = expr_1 ∧ pos = pos_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filterMap_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  Std.ExtDTreeMap.filterMap f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = none
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.aestronglyMeasurable_one : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : One β], MeasureTheory.AEStronglyMeasurable 1 μ
-- Mathlib.Data.Vector.Defs
/-- Vector obtained by repeating an element.  -/
List.Vector.replicate : {α : Type u_1} → (n : ℕ) → α → List.Vector α n
-- Init.WF
PSigma.lexAccessible : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a : α},
  Acc r a → (∀ (a : α), WellFounded (s a)) → ∀ (b : β a), Acc (PSigma.Lex r s) ⟨a, b⟩
-- Init.Data.Repr
instReprPUnit : Repr PUnit.{u + 1}
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.collectFVars : Lean.Meta.Match.MkMatcherInput → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).π = h.π
-- Lean.Meta.Basic
Lean.Meta.instInhabitedContext : Inhabited Lean.Meta.Context
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : X ⟶ F.partialRightAdjointObj Y)
  (g : Y ⟶ Y'),
  F.partialRightAdjointHomEquiv (CategoryTheory.CategoryStruct.comp f (F.partialRightAdjointMap g)) =
    CategoryTheory.CategoryStruct.comp (F.partialRightAdjointHomEquiv f) g.hom
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_natCast : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (n : ℕ) (s : Set A),
  Algebra.adjoin R (insert (↑n) s) = Algebra.adjoin R s
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.dischargeWrapper : Lean.Elab.Tactic.MkSimpContextResult → Lean.Elab.Tactic.Simp.DischargeWrapper
-- Mathlib.Computability.TuringDegree
TuringReducible.trans : ∀ {f g h : ℕ →. ℕ}, TuringReducible f g → TuringReducible g h → TuringReducible f h
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.trySend : {α : Type} → Std.CloseableChannel.Zero✝ α → α → BaseIO Bool
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_ne_zero_iff_squarefree : ∀ {n : ℕ}, ArithmeticFunction.moebius n ≠ 0 ↔ Squarefree n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α Unit cmp}, t₁.keys.Perm t₂.keys → t₁.Equiv t₂
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Post-composition by a *fixed* continuous linear map as a continuous linear map for the uniform
convergence topology.  -/
ContinuousLinearMap.postcompUniformConvergenceCLM : {𝕜₁ : Type u_6} →
  {𝕜₂ : Type u_7} →
    {𝕜₃ : Type u_8} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_9} →
                      {F : Type u_10} →
                        {G : Type u_11} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            (𝔖 : Set (Set E)) →
                                              [inst_13 : IsTopologicalAddGroup F] →
                                                [inst_14 : IsTopologicalAddGroup G] →
                                                  [inst_15 : ContinuousConstSMul 𝕜₃ G] →
                                                    [inst_16 : ContinuousConstSMul 𝕜₂ F] →
                                                      (F →SL[τ] G) →
                                                        UniformConvergenceCLM σ F 𝔖 →SL[τ] UniformConvergenceCLM ρ G 𝔖
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.wIso.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (w w_1 : X ⟶ Y) (e_w : w = w_1) (hw : W w),
  CategoryTheory.Localization.Construction.wIso w hw = CategoryTheory.Localization.Construction.wIso w_1 ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 1),
  ∃ X₀ X₁ f, X = CategoryTheory.ComposableArrows.mk₁ f
-- Init.Data.Option.Attach
Option.filter_attachWith : ∀ {α : Type u_1} {P : α → Prop} {o : Option α} {h : ∀ (x : α), o = some x → P x} {q : α → Bool},
  (Option.filter q do
      let a ← o.attachWith P h
      pure ↑a) =
    do
    let a ← (Option.filter q o).attachWith P ⋯
    pure ↑a
-- Lean.Elab.Tactic.ElabTerm
/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
elaboration and then a `TypeMismatchError` will be thrown if the elaborated type doesn't match.   -/
Lean.Elab.Tactic.elabTermEnsuringType : Lean.Syntax → Option Lean.Expr → optParam Bool false → Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.decidableEq : {α : Type u_1} →
  [inst : AddCommMonoid α] → [IsCancelAdd α] → {s : AddSubmonoid α} → [DecidableEq α] → DecidableEq (AddLocalization s)
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n] (A : Matrix m n α)
  (x y : n → α), A.mulVec (x - y) = A.mulVec x - A.mulVec y
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_mono : ∀ {x y : PSet.{u}}, x ⊆ y → x.rank ≤ y.rank
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
operation on `Pi.single` and at zero. Analogous to `LinearMap.pi_ext`. See also `pi_ext_nonempty`,
which instead of agreement at zero requires `Nonempty ι`.  -/
AffineMap.pi_ext_zero : ∀ {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V2] [inst_2 : AddTorsor V2 P2]
  [inst_3 : Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [inst_4 : (i : ι) → AddCommGroup (φv i)]
  [inst_5 : (i : ι) → Module k (φv i)] [Finite ι] [inst_7 : DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2},
  (∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) → f 0 = g 0 → f = g
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Neg.neg '' Set.Ico a b = Set.Ioc (-b) (-a)
-- Mathlib.Topology.Algebra.ClopenNhdofOne
IsTopologicalAddGroup.exist_openNormalAddSubgroup_sub_clopen_nhds_of_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  {W : Set G}, IsClopen W → 0 ∈ W → ∃ H, ↑H ⊆ W
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.frobenius_zmod : ∀ {σ : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)),
  (frobenius (MvPolynomial σ (ZMod p)) p) f = (MvPolynomial.expand p) f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
and `x` has been eliminated using the equality `c`.
 -/
Lean.Grind.Linarith.Poly.findVarToSubst : Lean.Grind.Linarith.Poly →
  Lean.Meta.Grind.Arith.Linear.LinearM (Option (ℤ × Lean.Grind.Linarith.Var × Lean.Meta.Grind.Arith.Linear.EqCnstr))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- (Implementation.) The projection map when constructing the pullback along an open immersion.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) → [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → (g : Y ⟶ Z) → Y.restrict ⋯ ⟶ X
-- Mathlib.Data.List.ProdSigma
List.sigma_nil : ∀ {α : Type u_1} {σ : α → Type u_3} (l : List α), (l.sigma fun a => []) = []
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.union_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t u : Set X},
  SeparatedNhds s t → SeparatedNhds s u → SeparatedNhds s (t ∪ u)
-- Std.Http.Protocol.H1.Config
Std.Http.Protocol.H1.Config.mk : ℕ →
  ℕ →
    ℕ →
      Bool →
        Option Std.Http.Header.Value →
          ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Std.Http.Protocol.H1.Config
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If the quadratic form `Q` is equivalent to a weighted sum of squares with weights `w`, then
the rank of `Q.radical` is equal to the number of zero weights.  -/
QuadraticForm.finrank_radical_of_equiv_weightedSumSquares : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Field 𝕜] [NeZero 2] [inst_2 : Fintype ι] {w : ι → 𝕜} {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {Q : QuadraticForm 𝕜 M},
  QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w) →
    Module.finrank 𝕜 ↥(QuadraticMap.radical Q) = {i | w i = 0}.ncard
-- Batteries.Data.Vector.Lemmas
Vector.scanrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α → β → β} {as : Vector α n}, Vector.scanrM (fun x1 x2 => pure (f x1 x2)) init as = pure (Vector.scanr f init as)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_adj_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ},
  i < w.length → w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- An `AffineMap k P1 P2` (notation: `P1 →ᵃ[k] P2`) is a map from `P1` to `P2` that
induces a corresponding linear map from `V1` to `V2`.  -/
«term_→ᵃ[_]_» : Lean.TrailingParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insertIfNew k v).contains k = true
-- Lean.Elab.DocString
/-- Gadget that indicates that a function's parameter should be treated as a Boolean flag when used in
a docstring extension.
 -/
Lean.Doc.flag : Bool → Type
-- Mathlib.Tactic.Translate.Core
/-- The attributes which we want to give to the original and translated declaration.
For `simps` this will also add generated lemmas to the translation dictionary.  -/
Mathlib.Tactic.Translate.Config.attrs : Mathlib.Tactic.Translate.Config → Array Lean.Syntax
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierInvAdd` is a function space on which the inverse Fourier transform is additive.  -/
FourierInvAdd : (E : Type u_5) → (F : outParam (Type u_6)) → [Add E] → [Add F] → [FourierTransformInv E F] → Prop
-- Std.Internal.Do.PredTrans
/-- Unfolding `>>=` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_bind : ∀ {α β : Type u_1} {Pred : Type u} {EPred : Type v} (x : Std.Internal.Do.PredTrans Pred EPred α)
  (f : α → Std.Internal.Do.PredTrans Pred EPred β) (post : β → Pred) (epost : EPred),
  (x >>= f).apply post epost = x.apply (fun a => (f a).apply post epost) epost
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).contains k = (f (t.get? k)).isSome
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.smul.injEq : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i : ι) (r : R) (x : M) (m_1 : ι → M) (i_1 : ι) (r_1 : R)
  (x_1 : M),
  (exteriorPower.presentation.Rels.smul m i r x = exteriorPower.presentation.Rels.smul m_1 i_1 r_1 x_1) =
    (m = m_1 ∧ i = i_1 ∧ r = r_1 ∧ x = x_1)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.empty : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp
-- Mathlib.Order.Filter.AtTopBot.Floor
FloorSemiring.eventually_mul_pow_lt_factorial_sub : ∀ {K : Type u_1} [inst : Ring K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a c : K) (d : ℕ),
  ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < ↑(n - d).factorial
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_intCast_le : ∀ {R : Type u} [inst : Ring R] (n : ℤ), (↑n).degree ≤ 0
-- Lean.Util.Trace
Lean.instMonadAlwaysExceptMonadCacheT : {α : Type} →
  {m : Type → Type} →
    {ε ω β : Type} →
      [always : Lean.MonadAlwaysExcept ε m] →
        [inst : STWorld ω m] →
          [inst_1 : BEq α] → [inst_2 : Hashable α] → Lean.MonadAlwaysExcept ε (Lean.MonadCacheT α β m)
-- Mathlib.Algebra.Order.Group.Defs
inv_le_one_of_one_le : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α}, 1 ≤ a → a⁻¹ ≤ 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (ho : Homotopy φ₁ φ₂),
  ↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) ho) = CochainComplex.HomComplex.Cochain.ofHomotopy ho
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.compl_def : ∀ {R : Type u} {M : Type v} [inst : AddGroup R] [inst_1 : AddAction R M] (s : SubAddAction R M), sᶜ.carrier = (↑s)ᶜ
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.ballSubgroup_top : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M], ⊤.ballSubgroup = ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).contains k = (f t[k]?).isSome
-- Mathlib.Order.Atoms.Finite
instIsStronglyCoatomic : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α], IsStronglyCoatomic α
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.rewritePost : optParam Bool false → Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_nilRankAux_ne_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) [Nontrivial R], (φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_eq_one : ∀ {α : Type u_1} [inst : One α] {x : Additive α}, Additive.toMul x = 1 ↔ x = 0
-- Init.Data.Vector.Lemmas
Vector.getElem_swap : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n) {k : ℕ} (hk : k < n),
  (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.map_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
  {f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤}, X (f - f') = X f - X f'
-- Init.MetaTypes
Lean.Meta.Simp.instBEqConfig.beq : Lean.Meta.Simp.Config → Lean.Meta.Simp.Config → Bool
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsChord.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (e : Sym2 V),
  p.IsChord e = (e ∈ G.edgeSet ∧ e ∉ p.edges ∧ Sym2.lift ⟨fun v_1 w => v_1 ∈ p.support ∧ w ∈ p.support, ⋯⟩ e)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.sign.eq_1 : Tactic.ComputeAsymptotics.UnitMonomial.sign [] = Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero
-- Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
/-- If a function `f` is summable in a uniform additive group `α`, then its sum in `α` is the same
as its sum in `Completion α`.  -/
Summable.toCompl_tsum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : IsUniformAddGroup α]
  {L : SummationFilter β} [L.NeBot] {f : β → α},
  Summable f L → ∑'[L] (i : β), UniformSpace.Completion.toCompl (f i) = ↑(∑'[L] (i : β), f i)