mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- The sum of a locally finite collection of sections is differentiable if each section is.  -/
MDifferentiable.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9}
  {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) → (∀ (i : ι), MDiff (T% t)) → MDiff fun x => ⟨x, ∑' (i : ι), t i x⟩
-- Mathlib.Data.Rat.Lemmas
Rat.add_num_den' : ∀ (q r : ℚ), (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
-- Mathlib.Algebra.Group.Units.Defs
/-- The element of the additive group of additive units, corresponding to an element
of an additive monoid which is an additive unit. When `α` is a `SubtractionMonoid`, use
`IsAddUnit.addUnit'` instead.  -/
IsAddUnit.addUnit : {M : Type u_1} → [inst : AddMonoid M] → {a : M} → IsAddUnit a → AddUnits M
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  ω₁ =ᶠ[nhdsWithin x s] ω₂ → extDerivWithin ω₁ s =ᶠ[nhdsWithin x s] extDerivWithin ω₂ s
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piFan_π_app : ∀ {ι : Type v} (α : ι → TopCat) (X : CategoryTheory.Discrete ι), (TopCat.piFan α).π.app X = TopCat.piπ α X.as
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn : {β : Type u_1} →
  {α : Type u_2} →
    [inst : LE β] → [DecidableLE β] → (α → β) → {xs ys : List α} → (i j : ℕ) → i < xs.length → j < ys.length → ℕ
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
/-- [Stacks Tag 00GX](https://stacks.math.columbia.edu/tag/00GX) (Part 3) -/
IsAlmostIntegral.isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsNoetherianRing R]
  [IsDomain S] [FaithfulSMul R S] {s : S}, IsAlmostIntegral R s → IsIntegral R s
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Variant of `prod_map` not applied to a function.  -/
Finset.prod_map' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (e : ι ↪ κ),
  (Finset.map e s).prod = fun f => ∏ x ∈ s, f (e x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q → P 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → IsUnit (W.dblZ P)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).isLimit.lift s =
    CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F)
      { pt := s.pt, π := { app := fun x => CategoryTheory.Limits.Pi.lift fun x_1 => s.π.app ↑x_1, naturality := ⋯ } }
-- Mathlib.Order.Heyting.Basic
OrderDual.instCoheytingAlgebra : {α : Type u_2} → [HeytingAlgebra α] → CoheytingAlgebra αᵒᵈ
-- ProofWidgets.Compat
/-- See `RpcEncodable`.  -/
ProofWidgets.LazyEncodable : Type → Type
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a ≤ b → ¬IsMax b → insert (b + 1) (Finset.Ioc a b) = Finset.Ioc a (b + 1)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxKey!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (x : Std.DTreeMap.Internal.Impl α β),
  x.maxKey! =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxKey!" 436 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => k
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      r.maxKey!
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Init.Internal.Order.Basic
Lean.Order.lfp : {α : Sort u} → [Lean.Order.CompleteLattice α] → (α → α) → α
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Open immersions are stable under base-change.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_fst_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instToForwardSearcherForallCharBoolDefaultForwardSearcher : {p : Char → Bool} →
  String.Slice.Pattern.ToForwardSearcher p (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher p)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_eq_tsum_rpow : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ (f : ↥(lp E p)), ‖f‖ = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.CategoryTheory.CommSq
/-- The assertion that a square has a `LiftStruct`.  -/
CategoryTheory.CommSq.HasLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} → {f : A ⟶ X} → {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → CategoryTheory.CommSq f i p g → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_toList_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {v : β}, (k, v) ∈ t.toList ↔ t[k]? = some v
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_perm_eraseKey_of_containsₘ_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    m.containsₘ a = false →
      (Std.DHashMap.Internal.toListModel (↑m).buckets).Perm
        (Std.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral over simple functions in L1 space.  -/
MeasureTheory.L1.SimpleFunc.integral : {α : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → [NormedSpace ℝ E] → ↥(α →₁ₛ[μ] E) → E
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.succMany?_toFun : ∀ {α : Type u} {β : Type v} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (self : Std.PRange.UpwardEnumerable.Map α β) (n : ℕ) (a : α),
  Std.PRange.succMany? n (self.toFun a) = Option.map self.toFun (Std.PRange.succMany? n a)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- `S` is cyclic, that is, `S ⊔ i S` is the whole space.  -/
StandardSubspace.IsCyclic : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] (self : StandardSubspace H),
  self.toClosedSubmodule ⊔ self.toClosedSubmodule.mulI = ⊤
-- Aesop.Rule
Aesop.instToStringUnsafeRule : ToString Aesop.UnsafeRule
-- Mathlib.Order.UpperLower.Principal
/-- Strict principal lower set. `Set.Iio` as a lower set.  -/
LowerSet.Iio : {α : Type u_1} → [inst : Preorder α] → α → LowerSet α
-- Init.Data.UInt.Lemmas
UInt32.mul_add : ∀ {a b c : UInt32}, a * (b + c) = a * b + a * c
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.isFixedPt : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → Function.IsFixedPt f^[n] x
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.mulRight_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (a r : R), (AddMonoidHom.mulRight r) a = a * r
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul'_comp_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocCommSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A],
  LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = LinearMap.mul' R A
-- Mathlib.Algebra.Order.Module.HahnEmbedding
FiniteArchimedeanClass.ball.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] (c c_1 : FiniteArchimedeanClass M),
  c = c_1 → FiniteArchimedeanClass.ball K c = FiniteArchimedeanClass.ball K c_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- Attempt to parse a `NatOffset` from an expression -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.fromExpr? : Lean.Expr → optParam ℕ 0 → Lean.Meta.SimpM (Option Nat.NatOffset✝)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) {r : ℝ}, 0 < r → T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' Metric.sphere 0 r
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The units of the algebra of continuous `R`-linear endomorphisms of `M` is multiplicatively
equivalent to the type of continuous linear equivalences between `M` and itself.  -/
ContinuousLinearEquiv.unitsEquiv : (R : Type u_1) →
  (M : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (M →L[R] M)ˣ ≃* M ≃L[R] M
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Rco.HasRcoIntersection α],
  (∀ {a : α} {r s : Std.Rco α}, a ∈ Std.Rco.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Rco.LawfulRcoIntersection α
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.all.eq_1 : ∀ (f : (i : ℕ) → i < 0 → Bool), Nat.all 0 f = true
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeftAux_contractLeftAux : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (v : M) (x fx : CliffordAlgebra Q),
  ((CliffordAlgebra.contractLeftAux Q d) v)
      ((CliffordAlgebra.ι Q) v * x, ((CliffordAlgebra.contractLeftAux Q d) v) (x, fx)) =
    Q v • fx
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation on `adicCompletion K v`, transported from the completion along `equiv`.
 -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                Valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (WithZero (Multiplicative ℤ))
-- Mathlib.Topology.Inseparable
Inseparable.mem_open_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, Inseparable x y → IsOpen s → (x ∈ s ↔ y ∈ s)
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.Raw.get? : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → Option (β a)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong mono category is a category in which every monomorphism is strong.  -/
CategoryTheory.StrongMonoCategory.strongMono_of_mono : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.StrongMonoCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.StrongMono f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (d : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to0.trAux M s (Turing.TM1.Stmt.move d q) x = ((some q, x), Turing.TM0.Stmt.move d)
-- Init.Data.Ord.Basic
/-- Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.lt`.
 -/
ltOfOrd : {α : Type u_1} → [Ord α] → LT α
-- Mathlib.Data.Finset.Max
Finset.max'.congr_simp : ∀ {α : Type u_2} [inst : LinearOrder α] (s s_1 : Finset α) (e_s : s = s_1) (H : s.Nonempty), s.max' H = s_1.max' ⋯
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State.mk.injEq : ∀ (perfect perfect_1 : Bool), ({ perfect := perfect } = { perfect := perfect_1 }) = (perfect = perfect_1)
-- Mathlib.Data.Set.Prod
Set.univ_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β}, Set.univ ×ˢ t = Prod.snd ⁻¹' t
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, 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_3 h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited α] (h : t.WF) {hc : Std.DTreeMap.Internal.Impl.contains t.maxKey! t = true},
  t.getKey t.maxKey! hc = t.maxKey ⋯
-- Mathlib.Topology.Metrizable.Urysohn
/-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`.  -/
TopologicalSpace.exists_embedding_l_infty : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T3Space X] [SecondCountableTopology X], ∃ f, Topology.IsEmbedding f
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α], Antitone (fixingAddSubgroup M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inl_iso_of_right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.Mon.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon C → C
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.mem_addGroupFilterBasis_iff : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B) {V : Set A}, V ∈ hB.toRingFilterBasis.toAddGroupFilterBasis ↔ ∃ i, V = ↑(B i)
-- Init.Data.List.Scan.Lemmas
List.idRun_scanrM : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → Id β} {as : List α},
  (List.scanrM f init as).run = List.scanr (fun x1 x2 => (f x1 x2).run) init as
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.of_surjective' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [IsLocalRing R] [inst_2 : Ring S] [Nontrivial S] (f : R →+* S),
  Function.Surjective ⇑f → IsLocalRing S
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (b : β a) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.Equicontinuous.mono : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H H' : Set (X → α)},
  H.Equicontinuous → H' ⊆ H → H'.Equicontinuous
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.zero_eq_eval : ∀ (M : Type u_3) [inst : AddMonoid M], 0 = Mathlib.Tactic.Module.NF.eval []
-- Mathlib.Analysis.InnerProductSpace.PiL2
Pi.orthonormalBasis.toBasis : ∀ {η : Type u_7} [inst : Fintype η] {ι : η → Type u_8} [inst_1 : (i : η) → Fintype (ι i)] {𝕜 : Type u_9}
  [inst_2 : RCLike 𝕜] {E : η → Type u_10} [inst_3 : (i : η) → NormedAddCommGroup (E i)]
  [inst_4 : (i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)),
  (Pi.orthonormalBasis B).toBasis = (Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
IsAddLeftRegular.withTop : ∀ {α : Type u} [inst : Add α] {a : α}, IsAddLeftRegular a → IsAddLeftRegular ↑a
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))) a) =
    (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x))
      ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op ⊤))) a)
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_eq_zero_iff : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, imaginaryPart x = 0 ↔ IsSelfAdjoint x
-- Mathlib.CategoryTheory.Sites.Sieves
/-- For an object `X` of a category `C`, a `Sieve X` is a predicate on morphisms to `X` which is closed
under left-composition.
 -/
CategoryTheory.Sieve : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.lt_top_of_tsum_ne_top : ∀ {α : Type u_1} {a : α → ENNReal}, ∑' (i : α), a i ≠ ⊤ → ∀ (j : α), a j < ⊤
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_toDual : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι],
  b.dualBasis.toDual ∘ₗ b.toDual = Module.Dual.eval R M
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.functorProdToProdFunctorAssociator_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : CategoryTheory.Functor A ((C × D) × E)),
  (CategoryTheory.prod.functorProdToProdFunctorAssociator C D E A).hom.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.CategoryStruct.id
        ((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.fst C (D × E))))
      (CategoryTheory.Prod.mkHom
        (CategoryTheory.CategoryStruct.id
          (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp
            (CategoryTheory.Prod.fst D E)))
        (CategoryTheory.CategoryStruct.id
          (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp
            (CategoryTheory.Prod.snd D E))))
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.ext_iff : ∀ {X Y : Bipointed} {x y : X.Hom Y}, x = y ↔ x.toFun = y.toFun
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.SimplyConnectedSpace.nonempty_sdiffeomorph_sphere_three : (M : Type u_1) →
  [inst : TopologicalSpace M] →
    [T2Space M] →
      [inst_2 : ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] →
        [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) (↑⊤) M] →
          [SimplyConnectedSpace M] →
            [CompactSpace M] →
              ProofWanted
                (Nonempty
                  (Diffeomorph (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3)))
                    (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) M ↑(Metric.sphere 0 1) ↑⊤))
-- Lean.Expr
/-- Returns the number of leading `∀` binders of an expression. Ignores metadata.
 -/
Lean.Expr.getNumHeadForalls : Lean.Expr → ℕ
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.IsRightContinuous.mk : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {𝓕 : MeasureTheory.Filtration ι m},
  𝓕.rightCont ≤ 𝓕 → 𝓕.IsRightContinuous
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_sub_right : ∀ {M : Type u} [inst : SubNegMonoid M] [inst_1 : PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  dist (a - c) (b - c) = dist a b
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.card_le_card_mul_right₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : DecidableEq α] {s t : Finset α} {a : α}
  [IsRightCancelMulZero α], a ∈ t → a ≠ 0 → s.card ≤ (s * t).card
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge_self_eq_bot : ∀ {V : Type u_1} (s : V), SimpleGraph.edge s s = ⊥
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRupUnits.eq_1 : ∀ {n : ℕ} (ls : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.insertRupUnits ls =
    match List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (rupUnits, assignments, false) ls with
    | (rupUnits, assignments, foundContradiction) =>
      ({ clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments },
        foundContradiction)
-- Mathlib.Data.PNat.Basic
Nat.succPNat_lt_succPNat : ∀ {m n : ℕ}, m.succPNat < n.succPNat ↔ m < n
-- Lean.Expr
Lean.instReprExpr : Repr Lean.Expr
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_inj : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R}, φ * PowerSeries.X = ψ * PowerSeries.X ↔ φ = ψ