mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Topology
/-- If `x ∈ s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`.  -/
Convex.add_smul_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [AddRightMono 𝕜] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → x + y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • y ∈ interior s
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.summable_norm_apply : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E}, x ∈ Metric.eball 0 p.radius → Summable fun n => ‖(p n) fun x_1 => x‖
-- Init.Grind.Ring.Basic
/-- Scalar multiplication by integers.  -/
Lean.Grind.Ring.zsmul : {α : Type u} → [self : Lean.Grind.Ring α] → SMul ℤ α
-- Mathlib.Control.Monad.Writer
WriterT.run_liftM : ∀ {M : Type u → Type v} {α ω : Type u} [inst : Monad M] (empty : ω) (cmd : M α),
  (liftM cmd).run = (fun a => (a, empty)) <$> cmd
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
/-- Return `true` if `t` contains a metavariable that is not in `mvarSet`  -/
_private.Lean.Meta.Tactic.Simp.SimpCongrTheorems.0.Lean.Meta.mkSimpCongrTheorem.onlyMVarsAt : Lean.Expr → Lean.MVarIdSet → Bool
-- Mathlib.Topology.Continuous
denseRange_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], DenseRange id
-- Aesop.Script.SpecificTactics
Aesop.tryClearS : Lean.MVarId → Lean.FVarId → Aesop.ScriptM (Option Lean.MVarId)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.append.eq_def : ∀ (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.append p₂ =
    match p₁ with
    | Int.Internal.Linear.Poly.num k₁ => p₂.addConst k₁
    | Int.Internal.Linear.Poly.add k x p₁ => Int.Internal.Linear.Poly.add k x (p₁.append p₂)
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- The norm of the extension is bounded by `‖fr‖`.  -/
StrongDual.norm_extendRCLike_bound : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F),
  ‖fr.extendRCLike x‖ ≤ ‖fr‖ * ‖x‖
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vsub : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VSub α β] (s : ι → Set β) (t : Set β),
  (⋃ i, s i) -ᵥ t = ⋃ i, s i -ᵥ t
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_one : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : ℕ → M), ∑ k ∈ Finset.range 1, f k = f 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).contains k = Option.any (f k) (t.get? k)
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `ContinuousOn.domRestrict`.

---

**Alias** of the forward direction of `continuousOn_iff_continuous_domRestrict`. -/
ContinuousOn.restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → Continuous (s.domRestrict f)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ), Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.pop k a q) = Turing.TM2.SupportsStmt S q
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.checkSplitInfoArgStatus : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from rings to types preserves all limits. (That is, the underlying
types could have been computed instead as limits in the category of types.)
 -/
RingCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget RingCat)
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.mul_const' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x * a)) (c / a)
-- Mathlib.Data.Semiquot
Semiquot.mk'.inj : ∀ {α : Type u_1} {s : Set α} {val : Trunc ↑s} {s_1 : Set α} {val_1 : Trunc ↑s_1},
  { s := s, val := val } = { s := s_1, val := val_1 } → s = s_1 ∧ val ≍ val_1
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.mkCasesResultSeq : Lean.TSyntax `grind → Array (List (Lean.TSyntax `grind)) → Bool → Lean.CoreM (List (Lean.TSyntax `grind))
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The bottom-right `d × r` part of a `(u+d) × (l+r)` matrix.  -/
Matrix.subDownRight : {α : Type v} → {d u l r : ℕ} → Matrix (Fin (u + d)) (Fin (l + r)) α → Matrix (Fin d) (Fin r) α
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_map_eq : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V), SimpleGraph.comap (⇑f) (SimpleGraph.map (⇑f) G) = G
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k))
  (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.alter k f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match h : compare k k' with
    | Ordering.lt =>
      match Std.DTreeMap.Internal.Impl.alter k f l' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.gt =>
      match Std.DTreeMap.Internal.Impl.alter k f r' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.eq =>
      match f (some (cast ⋯ v')) with
      | none => { impl := l'.glue r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some v =>
        { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)]
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCast! a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil =>
      panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.getCast!" 153
        11 "key is not present in hash table"
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if h : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.AssocList.getCast! a es
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- The pullback of an ultrafilter along an injection whose range is large with respect to the given
ultrafilter.  -/
Ultrafilter.comap : {α : Type u} → {β : Type v} → {m : α → β} → (u : Ultrafilter β) → Function.Injective m → Set.range m ∈ u → Ultrafilter α
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.zsmul_add : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n : ℤ) (a b : M), n • (a + b) = n • a + n • b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed suprema of two functions are comparable if the functions are pointwise comparable  -/
ciSup_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  BddAbove (Set.range g) → (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup g
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.pre_comm_ihom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  [inst_2 : CategoryTheory.Closed W] [inst_3 : CategoryTheory.Closed X] (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Y) ((CategoryTheory.ihom W).map g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).map g) ((CategoryTheory.MonoidalClosed.pre f).app Z)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.insert.eq_1 : ∀ (k : ℕ) (v : Nat.Internal.Linear.Var), Nat.Internal.Linear.Poly.insert k v [] = [(k, v)]
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.instIsFilteredI : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  (P : CategoryTheory.IndParallelPairPresentation f g), CategoryTheory.IsFiltered P.I
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instProductivenessRelation : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : Std.Iterator α m β] →
        [Std.Iterators.Productive α m] →
          {P : β → Prop} → Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Attach α m P) m
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.Lean.Order.Example.findF.eq_1 : ∀ (P : ℕ → Bool) (rec : ℕ → Option ℕ) (x : ℕ),
  Lean.Order.Example.findF P rec x = if P x = true then some x else rec (x + 1)
-- Mathlib.Topology.Homotopy.Equiv
/-- If `X i` is homotopy equivalent to `Y i` for each `i`, then the space of functions (a.k.a. the
indexed product) `∀ i, X i` is homotopy equivalent to `∀ i, Y i`.  -/
ContinuousMap.HomotopyEquiv.piCongrRight : {ι : Type u_1} →
  {X : ι → Type u_2} →
    {Y : ι → Type u_3} →
      [inst : (i : ι) → TopologicalSpace (X i)] →
        [inst_1 : (i : ι) → TopologicalSpace (Y i)] →
          ((i : ι) → ContinuousMap.HomotopyEquiv (X i) (Y i)) →
            ContinuousMap.HomotopyEquiv ((i : ι) → X i) ((i : ι) → Y i)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.map_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} {f g : X ⟶ Y}, F.map f = F.map g → f = g
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverLine : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- In the specific case of continuous alternating maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `Π(i : Fin (n+1)), M i` using `cons`, one can express directly the
additivity of an alternating map along the first variable.  -/
ContinuousAlternatingMap.vecCons_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] {n : ℕ}
  (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x y : M),
  f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.mk : {α : Type u} → α → Std.Ric α
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.add_iff_right` -/
DifferentiableAt.fun_add_iff_right : ∀ {𝕜 : 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 g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜 (fun i => f i + g i) x ↔ DifferentiableAt 𝕜 g x)
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.orderedSub : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α], OrderedSub { x // 0 ≤ x }
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.toInitResults : {α : Type} →
  Lean.Meta.RefinedDiscrTree.ImportErrorData✝ →
    Lean.Meta.RefinedDiscrTree.PreDiscrTree α → BaseIO (Lean.Meta.RefinedDiscrTree.InitResults✝ α)
-- Mathlib.Order.Filter.Pointwise
Filter.map_one' : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] (f : α → β), Filter.map f 1 = pure (f 1)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Equivalence between a `TensorProduct` of `PiTensorProduct`s and a single
`PiTensorProduct` indexed by a `Sum` type. If `N` is a constant family of
modules, use the non-dependent version `PiTensorProduct.tmulEquiv` instead.  -/
PiTensorProduct.tmulEquivDep : {ι : Type u_1} →
  {ι₂ : Type u_2} →
    (R : Type u_4) →
      [inst : CommSemiring R] →
        (N : ι ⊕ ι₂ → Type u_12) →
          [inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)] →
            [inst_2 : (i : ι ⊕ ι₂) → Module R (N i)] →
              TensorProduct R (PiTensorProduct R fun i₁ => N (Sum.inl i₁))
                  (PiTensorProduct R fun i₂ => N (Sum.inr i₂)) ≃ₗ[R]
                PiTensorProduct R fun i => N i
-- Mathlib.Tactic.ApplyFun
/-- Apply a function to a hypothesis.  -/
Mathlib.Tactic.applyFunHyp : Lean.Term → Option Lean.Term → Lean.FVarId → Lean.MVarId → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The set of lists of natural integers of length `l` with coefficients `< b` as a `Finset`.
This can be seen as the set of lists of length `l` of the digits in base `b` of
the integers `< b ^ l`.
Having this set as a `Finset` can be helpful for some proofs.
 -/
List.fixedLengthDigits : {b : ℕ} → 1 < b → ℕ → Finset (List ℕ)
-- Mathlib.GroupTheory.Complement
AddSubgroup.instInhabitedRightTransversal : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → Inhabited H.RightTransversal
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.ker_toSpanSingleton_eq_bot_iff : ∀ {R : Type u_1} [inst : Semiring R] {x : R}, (LinearMap.toSpanSingleton R R x).ker = ⊥ ↔ x ∈ nonZeroDivisorsRight R
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.mk : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α},
  Monotone (f a) →
    Filter.Tendsto (f a) Filter.atTop (nhds 1) →
      Filter.Tendsto (f a) Filter.atBot (nhds 0) →
        (∀ (t : ℚ), ⨅ r, f a ↑r = f a t) → ProbabilityTheory.IsRatStieltjesPoint f a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_div_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s / t).inf f = s.inf fun x => t.inf fun x_1 => f (x / x_1)
-- Init.Data.Nat.ToString
Nat.zero_eq_digitChar : ∀ {n : ℕ}, '0' = n.digitChar ↔ n = 0
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Second.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subSeconds : Std.Time.Timestamp → Std.Time.Second.Offset → Std.Time.Timestamp
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence that converges uniformly is also uniformly Cauchy  -/
TendstoUniformlyOnFilter.uniformCauchySeqOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α}, TendstoUniformlyOnFilter F f p p' → UniformCauchySeqOnFilter F p p'
-- Mathlib.Order.Filter.IndicatorFunction
Antitone.tendsto_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : One β] (s : ι → Set α),
  Antitone s →
    ∀ (f : α → β) (a : α),
      Filter.Tendsto (fun i => (s i).mulIndicator f a) Filter.atTop (pure ((⋂ i, s i).mulIndicator f a))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Internal.Raw₀.Const.getD (m₁.diff m₂) k fallback =
          if m₂.contains k = true then fallback else Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback
-- Mathlib.Topology.Category.Stonean.Basic
/-- The morphism from `presentation X` to `X`.  -/
Profinite.presentation.π : (X : Profinite) → Stonean.toProfinite.obj X.presentation ⟶ X
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instUnique : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → [Unique R] → Unique (WithAbs v)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.mem_closure_neg : ∀ {G : Type u_2} [inst : AddGroup G] (s : Set G) (x : G), x ∈ AddSubmonoid.closure (-s) ↔ -x ∈ AddSubmonoid.closure s
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.inner_eq_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι), inner 𝕜 (b i) (b i) = 1
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.root_mul_left_of_isRoot : ∀ {R : Type u} {a : R} [inst : CommSemiring R] (p : Polynomial R) {q : Polynomial R}, q.IsRoot a → (p * q).IsRoot a
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localAlgEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] [inst_4 : Algebra R P] (I : Ideal S) [inst_5 : I.IsPrime] (J : Ideal P) [inst_6 : J.IsPrime]
  (f : S ≃ₐ[R] P) (hIJ : I = Ideal.comap f J) (a : Localization.AtPrime J),
  (Localization.localAlgEquiv I J f hIJ).symm a = (Localization.localRingEquiv I J f.toRingEquiv hIJ).invFun a
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_mul : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S) (x y : R), f (x * y) = f x * f y
-- Mathlib.Topology.Order.NhdsSet
Iic_mem_nhdsSet_Iic_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a b : α}
  [(nhdsWithin b (Set.Ioi b)).NeBot], Set.Iic a ∈ nhdsSet (Set.Iic b) ↔ b < a
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.mk.injEq : ∀
  (trueExpr falseExpr natZExpr btrueExpr bfalseExpr ordEqExpr intExpr trueExpr_1 falseExpr_1 natZExpr_1 btrueExpr_1
    bfalseExpr_1 ordEqExpr_1 intExpr_1 : Lean.Expr),
  ({ trueExpr := trueExpr, falseExpr := falseExpr, natZExpr := natZExpr, btrueExpr := btrueExpr,
        bfalseExpr := bfalseExpr, ordEqExpr := ordEqExpr, intExpr := intExpr } =
      { trueExpr := trueExpr_1, falseExpr := falseExpr_1, natZExpr := natZExpr_1, btrueExpr := btrueExpr_1,
        bfalseExpr := bfalseExpr_1, ordEqExpr := ordEqExpr_1, intExpr := intExpr_1 }) =
    (trueExpr = trueExpr_1 ∧
      falseExpr = falseExpr_1 ∧
        natZExpr = natZExpr_1 ∧
          btrueExpr = btrueExpr_1 ∧ bfalseExpr = bfalseExpr_1 ∧ ordEqExpr = ordEqExpr_1 ∧ intExpr = intExpr_1)
-- Mathlib.Data.Nat.ModEq
Nat.add_mod_of_add_mod_lt : ∀ {a b c : ℕ}, a % c + b % c < c → (a + b) % c = a % c + b % c
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.norm_fract_le : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] [HasSolidNorm K] (m : E), ‖ZSpan.fract b m‖ ≤ ∑ i, ‖b i‖
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- `f =ᵐ[μ] g` means `f` and `g` are eventually equal along the a.e. filter,
i.e. `f=g` away from a null set.

This is notation for `Filter.EventuallyEq (MeasureTheory.ae μ) f g`.  -/
MeasureTheory.«term_=ᵐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.addNegClosureNhd.nhds : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : AddGroup G],
  IsTopologicalAddGroup.addNegClosureNhd T W → T ∈ nhds 0
-- Mathlib.Tactic.TermCongr
/-- If the expression is a congruence hole, returns `(forLhs, sideVal, pf)`.
If `mvarCounterSaved?` is not none, then only returns the hole if it is at least as recent.  -/
Mathlib.Tactic.TermCongr.cHole? : Lean.Expr → optParam (Option ℕ) none → Option (Bool × Lean.Expr × Lean.Expr)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.cauchy_map_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → ∀ {F : Filter α}, Cauchy (Filter.map f F) ↔ Cauchy F
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- An alternate version of Beck's comonadicity theorem. If `F` reflects isomorphisms, preserves
equalizers of `F`-cosplit pairs and `C` has equalizers of `F`-cosplit pairs, then it is comonadic.
 -/
CategoryTheory.Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [F.ReflectsIsomorphisms] →
                [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] →
                  [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] → CategoryTheory.ComonadicLeftAdjoint F
-- Init.Data.Array.Nat
Array.prod_replicate_nat : ∀ {n a : ℕ}, (Array.replicate n a).prod = a ^ n
-- Std.Time.DateTime.WallTime
Std.Time.instInhabitedWallTime.default : Std.Time.WallTime
-- Mathlib.Computability.StateTransition
/-- Reflexivity of `EvalsTo` in 0 steps.  -/
StateTransition.EvalsTo.refl : {σ : Type u_1} → (f : σ → Option σ) → (a : σ) → StateTransition.EvalsTo f a (some a)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrLeft'_apply : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A₁ i)]
  [inst_2 : (i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι ≃ ι') (x : (i : ι) → A₁ i),
  (AlgEquiv.piCongrLeft' R A₁ e) x = (Equiv.piCongrLeft' A₁ e) x
-- Mathlib.Algebra.Group.Pi.Basic
Pi.rightCancelSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → RightCancelSemigroup (f i)] → RightCancelSemigroup ((i : I) → f i)
-- Mathlib.Order.SemiconjSup
IsOrderRightAdjoint.comp_orderIso : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {g : β → α}, IsOrderRightAdjoint f g → ∀ (e : γ ≃o α), IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)
-- Mathlib.Logic.OpClass
/-- `IsSymmOp op` where `op : α → α → β` says that `op` is a symmetric operation,
i.e. `op a b = op b a`.
It is the natural generalisation of `Std.Commutative` (`β = α`) and `IsSymm` (`β = Prop`).  -/
IsSymmOp : {α : Sort u} → {β : Sort v} → (α → α → β) → Prop
-- Mathlib.MeasureTheory.Measure.Haar.Basic
_private.Mathlib.MeasureTheory.Measure.Haar.Basic.0.MeasureTheory.Measure.steinhaus_add_aux : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.InnerRegularCompactLTTop] [LocallyCompactSpace G] (E : Set G),
  MeasurableSet E → (∃ K ⊆ E, IsCompact K ∧ 0 < μ K) → E - E ∈ nhds 0