mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.zero_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → α), PreErgodic f 0
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is multiplicative.  -/
NormMulClass.norm_mul : ∀ {α : Type u_5} {inst : Norm α} {inst_1 : Mul α} [self : NormMulClass α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
-- Std.Sync.Channel
/-- Receive a value from the channel, blocking until the transmission could be completed. Note that the
return value may be `none` if the channel was closed before it could be completed.
 -/
Std.CloseableChannel.Sync.recv : {α : Type} → Std.CloseableChannel.Sync α → BaseIO (Option α)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosReflectLE_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  MulPosReflectLE α ↔ ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
DifferentiableWithinAt.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {s : Set E} {a : E},
  DifferentiableWithinAt ℝ c s a →
    DifferentiableWithinAt ℝ R s a →
      DifferentiableWithinAt ℝ x s a →
        x a ≠ c a → DifferentiableWithinAt ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_principal : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {s : Set α},
  f =O[Filter.principal s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.Algebra.Group.Semiconj.Basic
AddSemiconjBy.zsmul_right : ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → ∀ (m : ℤ), AddSemiconjBy a (m • x) (m • y)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- The map `toReal` defined as a `ℝ≥0`-linear map.  -/
CompactlySupportedContinuousMap.toRealLinearMap : {α : Type u_2} →
  [inst : TopologicalSpace α] → CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] CompactlySupportedContinuousMap α ℝ
-- Batteries.Data.Random.MersenneTwister
/-- Tempering mask parameters (`d`, `b`, `c`).  -/
Batteries.Random.MersenneTwister.Config.temperingMasks : (self : Batteries.Random.MersenneTwister.Config) → BitVec self.wordSize × BitVec self.wordSize × BitVec self.wordSize
-- Init.System.IOError
IO.Error.mkUnsatisfiedConstraints : UInt32 → String → IO.Error
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d),
  (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun K =>
        CategoryTheory.Limits.Cocone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multicofork I)).obj K).pt) ⋯)
      ⋯
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Analysis.RCLike.Extend
/-- Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.

Norm properties of this extension can be found in
`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`.  -/
StrongDual.extendRCLike : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousConstSMul 𝕜 F] → [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F → StrongDual 𝕜 F
-- Init.Control.Except
/-- An alternative unconditional error recovery operator that allows callers to specify which exception
to throw in cases where both operations throw exceptions.

By default, the first is thrown, because the `<|>` operator throws the second.
 -/
MonadExcept.orelse' : {ε : Type u} → {m : Type v → Type w} → [MonadExcept ε m] → {α : Type v} → m α → m α → optParam Bool true → m α
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.cardinalMk_le_max : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type v)
  [inst_2 : AddAction R X],
  Cardinal.mk (AddOreLocalization S X) ≤
    max (Cardinal.lift.{v, u} (Cardinal.mk ↥S)) (Cardinal.lift.{u, v} (Cardinal.mk X))
-- Mathlib.Probability.Process.Stopping
/-- Given a map `u : ι → Ω → E`, the stopped process with respect to `τ` is `u i ω` if
`i ≤ τ ω`, and `u (τ ω) ω` otherwise.

Intuitively, the stopped process stops evolving once the stopping time has occurred.  -/
MeasureTheory.stoppedProcess : {Ω : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [Nonempty ι] → [LinearOrder ι] → (ι → Ω → β) → (Ω → WithTop ι) → ι → Ω → β
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.mk : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool) → Mathlib.Tactic.GRewrite.Progress✝ → Mathlib.Tactic.GRewrite.State✝
-- Init.Data.List.Erase
List.eraseIdx_subset : ∀ {α : Type u_1} {l : List α} {k : ℕ}, l.eraseIdx k ⊆ l
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.below : {α : Type u} →
  {β : α → Type v} →
    {motive : (a : Std.DTreeMap.Internal.Impl α β) → a.Balanced → Prop} →
      {a : Std.DTreeMap.Internal.Impl α β} → a.Balanced → Prop
-- Mathlib.CategoryTheory.Limits.MonoCoprod
_private.Mathlib.CategoryTheory.Limits.MonoCoprod.0.CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum.match_1.eq_1 : ∀ {I₁ : Type u_1} {I₂ : Type u_2} (motive : I₁ ⊕ I₂ → Sort u_3) (i₁ : I₁) (h_1 : (i₁ : I₁) → motive (Sum.inl i₁))
  (h_2 : (i₂ : I₂) → motive (Sum.inr i₂)),
  (match Sum.inl i₁ with
    | Sum.inl i₁ => h_1 i₁
    | Sum.inr i₂ => h_2 i₂) =
    h_1 i₁
-- Lean.Meta.CoeAttr
Lean.Meta.instReprCoeFnType.repr : Lean.Meta.CoeFnType → ℕ → Std.Format
-- Mathlib.Analysis.InnerProductSpace.Basic
instInnerProductSpaceRealComplex : InnerProductSpace ℝ ℂ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Build a new pseudometric space from an old one where the bundled uniform structure is provably
(but typically non-definitionaly) equal to some given uniform structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
PseudoMetricSpace.replaceUniformity : {α : Type u_3} → [U : UniformSpace α] → (m : PseudoMetricSpace α) → uniformity α = uniformity α → PseudoMetricSpace α
-- Aesop.Index.RulePattern
Aesop.instInhabitedRulePatternIndex : Inhabited Aesop.RulePatternIndex
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.comap_map_eq_self : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : Ring B] [inst_4 : Algebra R B] {f : A →ₐ[R] B} {S : Subalgebra R A},
  ⇑f ⁻¹' {0} ⊆ ↑S → Subalgebra.comap f (Subalgebra.map f S) = S
-- Lean.Elab.Tactic.Rewrite
/-- Runs `Lean.MVarId.rewrite`, and also handles filtering out the old metavariables in the rewrite result.
This should be used from within `withSynthesize`.
Use `finishElabRewrite` once elaboration is complete to make final updates to `RewriteResult`.
 -/
Lean.Elab.Tactic.elabRewrite : Lean.MVarId →
  Lean.Expr →
    Lean.Syntax →
      optParam Bool false → optParam Lean.Meta.Rewrite.Config { } → Lean.Elab.Tactic.TacticM Lean.Meta.RewriteResult
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_lt_card_sdiff_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (s \ t).card < (t \ s).card ↔ s.card < t.card
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.toList.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β),
  m.toList = Std.DHashMap.Raw.Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) [] m
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filterMapM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n (Option β₂)}
  {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.Iter.filterMapM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      match __do_lift with
        | some c => g c acc
        | none => pure (ForInStep.yield acc)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.coeff_reflect : ∀ {R : Type u_1} [inst : Semiring R] (N : ℕ) (f : Polynomial R) (i : ℕ),
  (Polynomial.reflect N f).coeff i = f.coeff ((Polynomial.revAt N) i)
-- Init.Data.Array.MinMax
Array.max_replicate : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {n : ℕ} {a : α} (h : Array.replicate n a ≠ #[]),
  (Array.replicate n a).max h = a
-- Mathlib.Data.Finset.Sum
Finset.toLeft_monotone : ∀ {α : Type u_1} {β : Type u_2}, Monotone Finset.toLeft
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instCategorySkeleton : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] → CategoryTheory.Category.{u_1, u_2} (CategoryTheory.Skeleton C)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mk : (toOrderHom : ℝ →o ℝ) → (∀ (x : ℝ), toOrderHom.toFun (x + 1) = toOrderHom.toFun x + 1) → CircleDeg1Lift
-- Mathlib.Algebra.Star.BigOperators
star_finsuppProd : ∀ {R : Type u_1} {ι : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : CommMonoid R] [inst_2 : StarMul R] (s : ι →₀ M)
  (f : ι → M → R), star (s.prod f) = s.prod fun i m => star f i m
-- Mathlib.Topology.Algebra.Monoid
ContinuousAt.pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {x : X}, ContinuousAt f x → ∀ (n : ℕ), ContinuousAt (f ^ n) x
-- Mathlib.Data.Multiset.Defs
Multiset.instIsNonstrictStrictOrder : ∀ {α : Type u_1}, IsNonstrictStrictOrder (Multiset α) (fun x1 x2 => x1 ⊆ x2) fun x1 x2 => x1 ⊂ x2
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- If `f x = O(g x)` along `cofinite`, then there exists a positive constant `C` such that
`‖f x‖ ≤ C * ‖g x‖` whenever `g x ≠ 0`.  -/
Asymptotics.bound_of_isBigO_cofinite : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {g'' : α → F''}, f =O[Filter.cofinite] g'' → ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldRevM_eq_foldrM_toList : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM f init ↑m =
    List.foldrM (fun a b => f b a.1 a.2) init (Std.DHashMap.Raw.Const.toList ↑m)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.iterateRange_coe : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  (n : ℕ), f.iterateRange n = (f ^ n).range
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
NNReal.borelSpace : BorelSpace NNReal
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (n : ℤ) (e : M) {t t_n t_d : Mathlib.Tactic.FieldSimp.NF M},
  t.eval = t_n.eval / t_d.eval → ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.instIsOrderedAddMonoid : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : AddCommMonoid β] [IsOrderedAddMonoid β] [inst_5 : ContinuousAdd β], IsOrderedAddMonoid C(α, β)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.map_le_iff_le_comap : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal ℬ},
  HomogeneousIdeal.map f I ≤ J ↔ I ≤ HomogeneousIdeal.comap f J
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).minKey?.isSome = true
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_swap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.areaForm x) y = -(o.areaForm y) x
-- Batteries.Data.List.Lemmas
List.countBefore_zero : ∀ {α : Type u_1} {xs : List α} {p : α} [inst : BEq α], List.countBefore p xs 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.rhs : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → Lean.Expr
-- Mathlib.Algebra.Symmetrized
SymAlg.addCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup αˢʸᵐ
-- Mathlib.Data.Sym.Basic
/-- The symmetric product over `Option` is a disjoint union over simpler symmetric products.  -/
symOptionSuccEquiv : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → Sym (Option α) n.succ ≃ Sym (Option α) n ⊕ Sym α n.succ
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Non-unital normed ring structure on the product of two non-unital normed rings,
using the sup norm.  -/
Prod.nonUnitalNormedRing : {α : Type u_2} → {β : Type u_3} → [NonUnitalNormedRing α] → [NonUnitalNormedRing β] → NonUnitalNormedRing (α × β)
-- Mathlib.LinearAlgebra.FreeModule.IdealQuotient
/-- Ideal quotients over a free finite extension of `ℤ` are isomorphic to a direct product of
`ZMod`.  -/
Ideal.quotientEquivPiZMod : {ι : Type u_1} →
  {S : Type u_3} →
    [inst : CommRing S] →
      [inst_1 : IsDomain S] →
        [inst_2 : Finite ι] →
          (I : Ideal S) →
            (b : Module.Basis ι ℤ S) → (hI : I ≠ ⊥) → S ⧸ I ≃+ ((i : ι) → ZMod (Ideal.smithCoeffs b I hI i).natAbs)
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_iff_superset : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s
-- Mathlib.RingTheory.Ideal.Operations
Ideal.top_pow : ∀ (R : Type u) [inst : Semiring R] (n : ℕ), ⊤ ^ n = ⊤
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsInducedId : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁},
  (CategoryTheory.LocalizerMorphism.id W₁).IsInduced
-- Mathlib.Order.Types.Defs
OrderType.type_eq_type : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.type α = OrderType.type β ↔ Nonempty (α ≃o β)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.brecOn.eq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u}
  {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u}
  {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} {e : Q(«$α»)}
  (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e)
  (F_1 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t)
  (F_2 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t)
  (F_3 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_1 e t (Mathlib.Tactic.Ring.Common.ExBase.brecOn.go t F_1 F_2 F_3).2
-- Init.Data.Range.Polymorphic.PRange
/-- An upward-unbounded range of elements of `α` with a closed lower bound.

`a...*` is the range of all values greater than or equal to `a : α`.
This is notation for `Rci.mk a`.
 -/
Std.Rci : Type u → Type u
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t : Set β}, s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mk_coe : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] (S : Set L)
  (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0)
  (h₃ :
    ∀ (c : A) {x : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {a b : L},
      a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
          ⁅a, b⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier),
  ↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S
-- Mathlib.NumberTheory.EulerProduct.Basic
tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Multipliable f →
    Function.mulSupport f ⊆ {n | IsPrimePow n} →
      ∏' (n : ℕ), f n = (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
/-- The equivalence from the union over `n` of `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+`
given by sending `n = a * b` to `(a, b)`.  -/
sigmaAntidiagonalEquivProd : (n : ℕ+) × ↥(↑n).divisorsAntidiagonal ≃ ℕ+ × ℕ+
-- Mathlib.Order.Interval.Basic
/-- Allow lifting a pair `(a, b)` with `a ≤ b` to `NonemptyInterval`
in the `lift` tactic.  -/
NonemptyInterval.instCanLift : ∀ {α : Type u_1} [inst : LE α], CanLift (α × α) (NonemptyInterval α) NonemptyInterval.toProd fun x => x.1 ≤ x.2
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_neg_distrib : ∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : SubtractionCommMonoid G] (f : α → G),
  s.Finite → ∑ᶠ (x : α) (_ : x ∈ s), -f x = -∑ᶠ (x : α) (_ : x ∈ s), f x
-- Mathlib.Order.Comparable
AntisymmRel.compRel_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (CompRel (fun x1 x2 => x1 ≤ x2) a c ↔ CompRel (fun x1 x2 => x1 ≤ x2) b c)
-- Std.Data.DTreeMap.Raw.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DTreeMap.Raw.beq : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → [(k : α) → BEq (β k)] → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Bool
-- Mathlib.Data.List.Duplicate
List.Duplicate.elim_nil : ∀ {α : Type u_1} {x : α}, List.Duplicate x [] → False
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The basis `Pi.basisFun`, bundled as an orthonormal basis of `EuclideanSpace 𝕜 ι`.  -/
EuclideanSpace.basisFun : (ι : Type u_1) → (𝕜 : Type u_3) → [inst : RCLike 𝕜] → [inst_1 : Fintype ι] → OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {v : β},
  Std.DHashMap.Raw.Const.get (m.insert k v) k ⋯ = v
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f`
and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0`
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃` is exact and `φ.τ₂` is a mono.  -/
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.f = 0 →
    ∀ (hg₁ : S₁.g = 0),
      S₂.f = 0 →
        (CategoryTheory.ShortComplex.QuasiIso φ ↔
          { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ CategoryTheory.Mono φ.τ₂)
-- Mathlib.Data.ENNReal.Basic
ENNReal.abs_toReal : ∀ {x : ENNReal}, |x.toReal| = x.toReal
-- Mathlib.Order.UpperLower.Closure
upperClosure_singleton : ∀ {α : Type u_1} [inst : Preorder α] (a : α), upperClosure {a} = UpperSet.Ici a
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `G` is finite and `IsGaloisGroup G A B` with `A` and `B` domains, then `G` is also
a Galois group for `FractionRing B / FractionRing A` for the action defined by
`IsFractionRing.mulSemiringAction`.
 -/
IsGaloisGroup.toFractionRing : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) [inst : Group G] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [IsDomain A] [inst_6 : IsDomain B] [Finite G]
  [IsGaloisGroup G A B] [inst_9 : Algebra (FractionRing A) (FractionRing B)]
  [IsScalarTower A (FractionRing A) (FractionRing B)], IsGaloisGroup G (FractionRing A) (FractionRing B)
-- Std.Data.TreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.TreeMap.forIn : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → β → δ → m (ForInStep δ)) → δ → Std.TreeMap α β cmp → m δ
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.congr_simp : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (hf : Function.Injective ⇑f)
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {k : ℕ}
  (hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)) (x : AdicCompletion.AdicCauchySequence I N)
  (hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) (n : ℕ),
  AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker n = AdicCompletion.mapExactAux✝ hf ⋯ ⋯ hkn x ⋯ n
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.ghostComponent_zero_verschiebung : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R),
  (WittVector.ghostComponent 0) (WittVector.verschiebung x) = 0