mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.mk : ∀ {G : Type u_1} [inst : Add G],
  (∀ {A B : Finset G},
      1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2) →
    TwoUniqueSums G
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_apply`. -/
Set.restrict_apply : ∀ {α : Type u_1} {π : α → Type u_6} (f : (a : α) → π a) (s : Set α) (x : ↑s), s.domRestrict f x = f ↑x
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.get_eq_get_ofSliceTo : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} {h : pos ≠ (s.sliceTo p₀).endPos},
  pos.get h = (String.Slice.Pos.ofSliceTo pos).get ⋯
-- Init.Data.String.Substring
Substring.bsize : Substring.Raw → ℕ
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.instPow.eq_1 : ∀ {M : Type u_5} [inst : Monoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] (S : A),
  SubmonoidClass.instPow S = { pow := fun a n => ⟨↑a ^ n, ⋯⟩ }
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.eventually_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β],
  Asymptotics.IsEquivalent l u v → (∀ᶠ (t : α) in l, 0 ≤ v t) → ∀ᶠ (x : α) in l, 0 ≤ u x
-- Batteries.Data.List.Basic
List.isChain_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
  List.IsChain R (a :: b :: l) ↔ R a b ∧ List.IsChain R (b :: l)
-- Mathlib.Data.List.Basic
List.injective_foldl_comp : ∀ {α : Type u} {l : List (α → α)} {f : α → α},
  (∀ f ∈ l, Function.Injective f) → Function.Injective f → Function.Injective (List.foldl Function.comp f l)
-- Mathlib.Algebra.Group.AddChar
/-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
`Additive M`.  -/
AddChar.toAddMonoidAddEquiv : {A : Type u_2} →
  {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : CommMonoid M] → Additive (AddChar A M) ≃+ (A →+ Additive M)
-- Init.Data.List.ToArray
List.zip_toArray : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (bs : List β), as.toArray.zip bs.toArray = (as.zip bs).toArray
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
instIsAlgebraicResidueFieldOfIsIntegral : ∀ {A : Type u_2} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (q : Ideal B) [inst_3 : q.LiesOver p] [inst_4 : p.IsPrime] [inst_5 : q.IsPrime]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q] [Algebra.IsIntegral A B],
  Algebra.IsAlgebraic p.ResidueField q.ResidueField
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.assump : ℕ → Mathlib.Tactic.Linarith.CompSource
-- Mathlib.Data.Int.ModEq
Int.modulus_add_modEq_iff : ∀ {n a b : ℤ}, n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ciSup_of_not_bddAbove : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f : ι → α},
  ¬BddAbove (Set.range f) → ⨆ i, f i = sSup ∅
-- Mathlib.Data.Int.Bitwise
Int.testBit_lor : ∀ (m n : ℤ) (k : ℕ), (m.lor n).testBit k = (m.testBit k || n.testBit k)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
              W.dblY P / W.dblZ P ^ 3 =
                W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                  (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Mathlib.Data.List.AList
AList.lookup_insert_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l : AList β} {k k' : α} {v : β k},
  AList.lookup k' (AList.insert k v l) = none ↔ k' ≠ k ∧ AList.lookup k' l = none
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_insert_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → insert b (Set.Ioc b a) = Set.Icc b a
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ext_iff : ∀ {X Y : MonCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isSome = !t.isEmpty
-- Mathlib.Data.Nat.Dist
Nat.dist_tri_left' : ∀ (n m : ℕ), n ≤ n.dist m + m
-- Lean.Meta.Sym.Util
/-- Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.
Gaps are `none` cells at `lctx.decls`. In `SymM`, we assume these cells don't exist.
 -/
_private.Lean.Meta.Sym.Util.0.Lean.Meta.Sym.preprocessLCtx : Lean.LocalContext → Lean.Meta.Sym.SymM Lean.LocalContext
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.uniqueLinearEquiv_symm_apply : ∀ (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : One M] [inst_4 : Subsingleton M] (s : S),
  (MonoidAlgebra.uniqueLinearEquiv R M).symm s = MonoidAlgebra.single 1 s
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMap : ∀ {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O)
  [inst_4 : IsDiscreteValuationRing O] {ϖ : O},
  Irreducible ϖ → ↑(IsLocalRing.maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}
-- Mathlib.Order.Filter.Basic
Filter.forall_eventually_of_eventually_forall : ∀ {α : Type u} {β : Type v} {f : Filter α} {p : α → β → Prop},
  (∀ᶠ (x : α) in f, ∀ (y : β), p x y) → ∀ (y : β), ∀ᶠ (x : α) in f, p x y
-- Init.Data.List.Nat.Count
_private.Init.Data.List.Nat.Count.0.List.filter.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 ()
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_symm_apply : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : M →ₗ[R] M') (i : ι),
  (b.constr S).symm f i = f (b i)
-- Mathlib.Data.Finset.Image
Finset.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Finset α),
  Finset.map g (Finset.map f s) = Finset.map (f.trans g) s
-- Mathlib.Algebra.Order.Archimedean.IndicatorCard
Set.limsup_eq_tendsto_sum_indicator_atTop : ∀ {α : Type u_1} {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R]
  [AddLeftStrictMono R] [Archimedean R] {r : R},
  0 < r →
    ∀ (s : ℕ → Set α),
      Filter.limsup s Filter.atTop =
        {ω | Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) Filter.atTop Filter.atTop}
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.hasExitPointPred.loop : (Lean.Elab.Term.Do.Code → Bool) → Lean.Elab.Term.Do.Code → Bool
-- Init.Core
Function.id_comp : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), id ∘ f = f
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isCircuit : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.IsCircuit
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_closedBall : ∀ {ι : Type u_1} [inst : Fintype ι] (a : ι → ℝ) {r : ℝ},
  0 ≤ r → MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- Eta-expanded form of `MeasureTheory.IntegrableOn.add` -/
MeasureTheory.IntegrableOn.fun_add : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ → MeasureTheory.IntegrableOn (fun i => f i + g i) s μ
-- Mathlib.GroupTheory.PGroup
IsPGroup.mono : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {q : ℕ}, p ∣ q → IsPGroup p G → IsPGroup q G
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Auxiliary instance for the order on pairs `(exp, coef)` used below to define `Sorted` in terms
of `Stream'.Seq.Pairwise`. `(exp₁, coef₁) ≤ (exp₂, coef₂)` iff `exp₁ ≤ exp₂`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.instPreorderProdReal : {basis : Tactic.ComputeAsymptotics.Basis} → Preorder (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis)
-- Lean.SubExpr
Lean.SubExpr.Pos.depth : Lean.SubExpr.Pos → ℕ
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.Node : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      Option β → Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Lean.PrefixTreeNode α β cmp
-- Std.Data.String.ToInt
String.toInt?_eq_toNat?_of_startsWith_eq_false : ∀ {s : String}, s.startsWith '-' = false → s.toInt? = Option.map (fun a => ↑a) s.toNat?
-- Lean.Elab.Tactic.Omega.Frontend
/-- A partially processed `omega` context.

We have:
* a `Problem` representing the integer linear constraints extracted so far, and their proofs
* the unprocessed `facts : List Expr` taken from the local context,
* the unprocessed `disjunctions : List Expr`,
  which will only be split one at a time if we can't otherwise find a contradiction.

We begin with `facts := ← getLocalHyps` and `problem := .trivial`,
and progressively process the facts.

As we process the facts, we may generate additional facts
(e.g. about coercions and integer divisions).
To avoid duplicates, we maintain a `HashSet` of previously processed facts.
 -/
Lean.Elab.Tactic.Omega.MetaProblem : Type
-- Mathlib.FieldTheory.Minpoly.Basic
/-- If `B/A` is an injective ring extension, and `a` is an element of `A`,
then the minimal polynomial of `algebraMap A B a` is `X - C a`.  -/
minpoly.eq_X_sub_C_of_algebraMap_inj : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (a : A),
  Function.Injective ⇑(algebraMap A B) → minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
-- Mathlib.Data.ENat.Pow
ENat.epow_natCast : ∀ {x : ℕ∞} {y : ℕ}, x ^ ↑y = x ^ y
-- Mathlib.Tactic.Translate.Core
/-- An optional doc string.  -/
Mathlib.Tactic.Translate.Config.doc : Mathlib.Tactic.Translate.Config → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Aesop.Tree.Data
Aesop.Rapp.assignedMVars : Aesop.Rapp → Aesop.UnorderedArraySet Lean.MVarId
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_nsmul : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (n : ℕ) (x : 𝔸),
  NormedSpace.exp (n • x) = NormedSpace.exp x ^ n
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_init : ∀ {M : Type u_2} [inst : Monoid M] {n : ℕ} {f : Fin (n + 1) → M} (i : Fin (n + 1)),
  Fin.partialProd (Fin.init f) i = Fin.partialProd f i.castSucc
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_consecutive : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) {m n k : ℕ},
  m ≤ n → n ≤ k → (∏ i ∈ Finset.Ico m n, f i) * ∏ i ∈ Finset.Ico n k, f i = ∏ i ∈ Finset.Ico m k, f i
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D},
  (CategoryTheory.PreZeroHypercover.map F E).presieve₀ = CategoryTheory.Presieve.map F E.presieve₀
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.toIsNontrivial : ∀ {R : Type u_1} {Γ₀ : Type u_2} {inst : Ring R} {inst_1 : LinearOrderedCommGroupWithZero Γ₀} {v : Valuation R Γ₀}
  [self : v.RankOne], v.IsNontrivial
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_inter_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ∩ Set.Ici b = Set.Icc b a
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.foldUntil.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (∀ (a : α), x = some a → False) →
    (match x with
      | some a => h_1 a
      | x => h_2 x) =
      h_2 x
-- Init.Data.Nat.Basic
Nat.lt_of_add_left_lt : ∀ {n m k : ℕ}, k + n < m → n < m
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- Construct the object part of the desired left adjoint as the coequalizer of `F'Uε_Y` with
`otherMap`.
 -/
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor B C} →
              {F : CategoryTheory.Functor C B} →
                (R : CategoryTheory.Functor A B) →
                  (F' : CategoryTheory.Functor C A) →
                    (F ⊣ U) → (F' ⊣ R.comp U) → [CategoryTheory.Limits.HasReflexiveCoequalizers A] → B → A
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_trans_addEquiv : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] (f : α ≃+o β) (g : β ≃+o γ), ↑(f.trans g) = (↑f).trans ↑g
-- Mathlib.Data.EReal.Inv
EReal.top_div_of_neg_ne_bot : ∀ {a : EReal}, a < 0 → a ≠ ⊥ → ⊤ / a = ⊥
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  (F : CategoryTheory.Functor J (CategoryTheory.Arrow T))
  [i₁ : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Arrow.leftFunc)]
  [i₂ : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Arrow.rightFunc)], CategoryTheory.Limits.HasLimit F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {a : α} {fallback b : β a}, (Std.DTreeMap.Internal.Impl.insert! a b t).getD a fallback = b
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeInr_apply_inr : ∀ (α : Type u_3) {β : Type u_4} (x : β), (Equiv.Set.rangeInr α β) ⟨Sum.inr x, ⋯⟩ = x
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyLE.countable_bInter`. -/
EventuallyLE.countable_bInter : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Mathlib.Data.Seq.Basic
Stream'.tail.eq_1 : ∀ {α : Type u} (s : Stream' α) (i : ℕ), s.tail i = s.get (i + 1)
-- Mathlib.Analysis.Complex.Trigonometric
Real.inv_one_add_tan_sq : ∀ {x : ℝ}, Real.cos x ≠ 0 → (1 + Real.tan x ^ 2)⁻¹ = Real.cos x ^ 2
-- Mathlib.Analysis.Convex.Jensen
/-- **Minimum principle** for concave functions on an interval. If a function `f` is concave on the
interval `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`.  -/
ConcaveOn.min_le_of_mem_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module 𝕜 β]
  [IsStrictOrderedModule 𝕜 β] {s : Set 𝕜} {f : 𝕜 → β} {x y z : 𝕜},
  ConcaveOn 𝕜 s f → x ∈ s → y ∈ s → z ∈ Set.Icc x y → min (f x) (f y) ≤ f z
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_add_one : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} (n : ℕ),
  MeasureTheory.predictablePart f ℱ μ (n + 1) = MeasureTheory.predictablePart f ℱ μ n + μ[f (n + 1) - f n | ↑ℱ n]
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.prefix.injEq : ∀ (a : Lean.Name) (a_1 : Lean.Syntax) (a_2 : Lean.Name) (a_3 : Lean.Syntax),
  (Simps.ProjectionRule.prefix a a_1 = Simps.ProjectionRule.prefix a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Probability.Process.LocalProperty
/-- A property of stochastic processes is said to be stable if it is preserved under taking
the stopped process by a stopping time.  -/
ProbabilityTheory.IsStable : {ι : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [inst : LinearOrder ι] → [OrderBot ι] → [Zero E] → MeasureTheory.Filtration ι mΩ → ((ι → Ω → E) → Prop) → Prop
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableArray : {α : Type} → [Lean.Server.RpcEncodable α] → Lean.Server.RpcEncodable (Array α)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.map_add : ∀ {𝕜 : 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'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquiv_symm_none : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  W'.nonsingularPointEquiv.symm none = WeierstrassCurve.Affine.Point.zero
-- Mathlib.Algebra.Group.Action.Defs
instIsLeftCancelVAddOfIsLeftCancelAdd : ∀ (G : Type u_9) [inst : Add G] [IsLeftCancelAdd G], IsLeftCancelVAdd G G
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.PseudoMetrizableSpace.exists_countably_generated : ∀ {X : Type u_5} {t : TopologicalSpace X} [self : TopologicalSpace.PseudoMetrizableSpace X],
  ∃ u, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.instInhabited : Inhabited Nat.Partrec.Code
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.pentagonIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D)
  (K : CategoryTheory.Functor D E),
  CategoryTheory.Functor.isoWhiskerRight (F.associator G H) K ≪≫
      F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) =
    (F.comp G).associator H K ≪≫ F.associator G (H.comp K)
-- Mathlib.Data.ENNReal.Basic
/-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `Fact` for use with `Lp` spaces.  -/
fact_one_le_one_ennreal : Fact (1 ≤ 1)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂)
  (iso₃ : A.obj₃ ≅ B.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) =
        CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_5),
  (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.homMk A iso₁.inv iso₂.inv iso₃.inv ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.ae_map_mem_range : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} (f : α → β),
  MeasurableSet (Set.range f) →
    ∀ (μ : MeasureTheory.Measure α), ∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x ∈ Set.range f
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.mk : {α : Type u_4} →
  {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → (toHom : A →g B) → Function.Injective ⇑toHom → A.Copy B
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The identity homomorphism from a graph to itself.  -/
SimpleGraph.Hom.id : {V : Type u_1} → {G : SimpleGraph V} → G →g G
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.mk.inj : ∀ {openClose : Bool} {change : Lean.Lsp.TextDocumentSyncKind} {willSave willSaveWaitUntil : Bool}
  {save? : Option Lean.Lsp.SaveOptions} {openClose_1 : Bool} {change_1 : Lean.Lsp.TextDocumentSyncKind}
  {willSave_1 willSaveWaitUntil_1 : Bool} {save?_1 : Option Lean.Lsp.SaveOptions},
  { openClose := openClose, change := change, willSave := willSave, willSaveWaitUntil := willSaveWaitUntil,
        save? := save? } =
      { openClose := openClose_1, change := change_1, willSave := willSave_1, willSaveWaitUntil := willSaveWaitUntil_1,
        save? := save?_1 } →
    openClose = openClose_1 ∧
      change = change_1 ∧ willSave = willSave_1 ∧ willSaveWaitUntil = willSaveWaitUntil_1 ∧ save? = save?_1
-- Mathlib.Analysis.Seminorm
Seminorm.smul_closedBall_subset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ}, k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)
-- Mathlib.Algebra.Free
FreeMagma.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_descResidueField_assoc : ∀ {K : Type u} [inst : Field K] {X : AlgebraicGeometry.Scheme} {x : ↥X} (f : X.presheaf.stalk x ⟶ CommRingCat.of K)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)] {Z : CommRingCat} (h : CommRingCat.of K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.residue x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.descResidueField f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Lean.DocString.DeferredCheck
Lean.Doc.instReprDeferredCheckSite.repr : Lean.Doc.DeferredCheckSite → ℕ → Std.Format
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.ParserContext.mk.inj : ∀ {toParserContextCore toParserContextCore_1 : Lean.Parser.ParserContextCore},
  { toParserContextCore := toParserContextCore } = { toParserContextCore := toParserContextCore_1 } →
    toParserContextCore = toParserContextCore_1
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi).start = min (lo + 1) (min hi xs.size)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of `Matroid.restrict_eRk_eq` with no `X ⊆ R` hypothesis and thus a less simple RHS.  -/
Matroid.restrict_eRk_eq' : ∀ {α : Type u_1} (M : Matroid α) (R X : Set α), (M.restrict R).eRk X = M.eRk (X ∩ R)