mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Often it is more convenient to use `Memℓp.mono`, where the bounding function is real-valued.
This version is provable from that one using `Memℓp.toNorm` applied to the argument with type
`Memℓp g p`.  -/
Memℓp.mono' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {F : α → Type u_5}
  [inst_1 : (i : α) → NormedAddCommGroup (F i)] {f : (i : α) → E i} {g : (i : α) → F i},
  Memℓp g p → (∀ (i : α), ‖f i‖ ≤ ‖g i‖) → Memℓp f p
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁_supportsStmt_mono : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {S : Finset Λ} {q₁ q₂ : Turing.TM2.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM2.stmts₁ q₂ → Turing.TM2.SupportsStmt S q₂ → Turing.TM2.SupportsStmt S q₁
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens : Type
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
hasDerivAt_of_tendstoLocallyUniformlyOn : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g : 𝕜 → G} {f' : ι → 𝕜 → G} {g' : 𝕜 → G}
  {x : 𝕜} [IsRCLikeNormedField 𝕜] [l.NeBot] {s : Set 𝕜},
  IsOpen s →
    TendstoLocallyUniformlyOn f' g' l s →
      (∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.injective_of_isPath_map : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {β : Type u_2} {H : SimpleGraph β} {a b : α}
  {p : G.Walk a b} {f : G →g H}, p.IsHamiltonian → (SimpleGraph.Walk.map f p).IsPath → Function.Injective ⇑f
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_div : ∀ (a b : UInt8), (a / b).toUInt32 = a.toUInt32 / b.toUInt32
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimit.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesLimit K F] {c : CategoryTheory.Limits.Cone K}
  (hc : CategoryTheory.Limits.IsLimit c), Nonempty (CategoryTheory.Limits.IsLimit (F.mapCone c))
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.reduce_flatten_replicate : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeAddGroup.reduce (List.replicate n L).flatten =
        if n = 0 then []
        else
          FreeAddGroup.reduceCyclically.conjugator L ++ (List.replicate n (FreeAddGroup.reduceCyclically L)).flatten ++
            FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The object in `SimplicialObject.Split C` attached to a splitting `s : Splitting X`
of a simplicial object `X`.  -/
CategoryTheory.SimplicialObject.Split.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} → X.Splitting → CategoryTheory.SimplicialObject.Split C
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.congr' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =o[l] g₁ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → f₂ =o[l] g₂
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.snd_mul : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Add ι] [inst_1 : GradedMonoid.GMul A] (x y : GradedMonoid A),
  (x * y).snd = GradedMonoid.GMul.mul x.snd y.snd
-- Mathlib.Data.ZMod.Basic
ZMod.subsingleton_iff : ∀ {n : ℕ}, Subsingleton (ZMod n) ↔ n = 1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The underlying set of configurations (additive monoid version).  -/
SymbolicDynamics.FullShift.Subshift.carrier : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    {G : Type u_2} → [inst_1 : AddMonoid G] → SymbolicDynamics.FullShift.Subshift A G → Set (G → A)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.has_swap_mem_of_lt_stabilizer : ∀ {α : Type u_2} [inst : DecidableEq α] (s : Set α) (G : Subgroup (Equiv.Perm α)),
  MulAction.stabilizer (Equiv.Perm α) s < G → ∃ g, g.IsSwap ∧ g ∈ G
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.fix : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.mono_homologyMap_shortComplexTruncLE_g : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Mono (HomologicalComplex.homologyMap (K.shortComplexTruncLE e).g i')
-- Mathlib.Algebra.GroupWithZero.Basic
eq_zero_of_mul_self_eq_zero : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a : M₀}, a * a = 0 → a = 0
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_trans : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), (PartialEquiv.refl α).trans e = e
-- Init.Data.List.TakeDrop
List.drop_add_one_eq_tail_drop : ∀ {α : Type u_1} {i : ℕ} {l : List α}, List.drop (i + 1) l = (List.drop i l).tail
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colim.ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] (j : J) (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.colim.ι j).app F = CategoryTheory.Limits.colimit.ι F j
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_disjoint_on : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LinearOrder ι] (f : ι → α),
  Pairwise (Function.onFun Disjoint f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_tensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  CategoryTheory.MonoidalCategoryStruct.tensorUnit D =
    e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The inverse in a group object  -/
CategoryTheory.MonObj.termι : Lean.ParserDescr
-- Mathlib.Order.TypeTags
WithTop.inhabited.eq_1 : ∀ {α : Type u_1}, WithTop.inhabited = { default := ⊤ }
-- Mathlib.Order.Lattice
le_sup_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ max b c ↔ a ≤ b ∨ a ≤ c
-- Mathlib.Analysis.Normed.Module.Connected
/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is connected.  -/
isConnected_compl_of_one_lt_codim : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] {E : Submodule ℝ F}, 1 < Module.rank ℝ (F ⧸ E) → IsConnected (↑E)ᶜ
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.eq_zero' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [IsEmpty α]
  (f : ↥(lp E p)), f = 0
-- Mathlib.Computability.Partrec
Computable.nat_casesOn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ},
  Computable f → Computable g → Computable₂ h → Computable fun a => Nat.casesOn (f a) (g a) (h a)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Icc_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ}, MeasureTheory.volume (Set.Icc a b) = ∏ i, ENNReal.ofReal (b i - a i)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.mem_normalizer_iff_map_conj_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {g : G},
  g ∈ Subgroup.normalizer ↑H ↔ Subgroup.map (↑(MulAut.conj g)) H = H
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex.eq_1 : ∀ (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane),
  Derivative.normalizedDerivOfComplex F z = (2 * ↑Real.pi * Complex.I)⁻¹ * deriv (F ∘ ↑UpperHalfPlane.ofComplex) ↑z
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_surjective_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)),
  Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
differentiableWithinAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E} {t : Set H} {y : H},
  DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (f x).ofLp i) t y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- This lemma uses the simp-normal form `⇑(T†) ∘ ⇑T` instead of `⇑(T† ∘L T)`
(note the difference between `∘` and `∘L`).
You may need to rewrite with `ContinuousLinearMap.coe_comp'` before applying this lemma.
 -/
ContinuousLinearMap.adjoint_comp_self_injective_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  Function.Injective (⇑(ContinuousLinearMap.adjoint T) ∘ ⇑T) ↔ Function.Injective ⇑T
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.obj.ε_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C) [inst_5 : CategoryTheory.ComonObj X] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.counit)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) h)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The isomorphism from the point of a limit kernel fork of `S.g` to `S.cycles`.  -/
CategoryTheory.ShortComplex.isoCyclesOfIsLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] →
          {kf : CategoryTheory.Limits.KernelFork S.g} → CategoryTheory.Limits.IsLimit kf → (kf.pt ≅ S.cycles)
-- Init.Data.String.Hashable
String.instHashableRaw.hash : String.Pos.Raw → UInt64
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyOpIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {Z : Cᵒᵖ}
  (h : S₁.op.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ).op
      (CategoryTheory.CategoryStruct.comp S₁.homologyOpIso.inv h) =
    CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ)) h)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The composition operator (in the target) with a Lipschitz map is continuous.  -/
BoundedContinuousFunction.continuous_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
  Continuous (BoundedContinuousFunction.comp G H)
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
/-- `ℂ` is a finite extension of `ℝ` of degree 2, i.e `[ℂ : ℝ] = 2`  -/
Complex.finrank_real_complex : Module.finrank ℝ ℂ = 2
-- Std.Data.DHashMap.Basic
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.DHashMap.Const.toArray : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → Array (α × β)
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.mk.injEq : ∀ (ref : Lean.Syntax) (kind : Lean.Elab.DefKind) (levelParams : List Lean.Name) (modifiers : Lean.Elab.Modifiers)
  (declName : Lean.Name) (binders : Lean.Syntax) (numSectionVars : ℕ) (type value : Lean.Expr)
  (termination : Lean.Elab.TerminationHints) (ref_1 : Lean.Syntax) (kind_1 : Lean.Elab.DefKind)
  (levelParams_1 : List Lean.Name) (modifiers_1 : Lean.Elab.Modifiers) (declName_1 : Lean.Name)
  (binders_1 : Lean.Syntax) (numSectionVars_1 : ℕ) (type_1 value_1 : Lean.Expr)
  (termination_1 : Lean.Elab.TerminationHints),
  ({ ref := ref, kind := kind, levelParams := levelParams, modifiers := modifiers, declName := declName,
        binders := binders, numSectionVars := numSectionVars, type := type, value := value,
        termination := termination } =
      { ref := ref_1, kind := kind_1, levelParams := levelParams_1, modifiers := modifiers_1, declName := declName_1,
        binders := binders_1, numSectionVars := numSectionVars_1, type := type_1, value := value_1,
        termination := termination_1 }) =
    (ref = ref_1 ∧
      kind = kind_1 ∧
        levelParams = levelParams_1 ∧
          modifiers = modifiers_1 ∧
            declName = declName_1 ∧
              binders = binders_1 ∧
                numSectionVars = numSectionVars_1 ∧ type = type_1 ∧ value = value_1 ∧ termination = termination_1)
-- Std.Async.Basic
/-- Creates a new `EAsync` out of a `ETask`.
 -/
Std.Async.EAsync.ofETask : {ε α : Type} → Std.Async.ETask ε α → Std.Async.EAsync ε α
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_inj : ∀ {a b : Ordinal.{v}}, Ordinal.lift.{u, v} a = Ordinal.lift.{u, v} b ↔ a = b
-- Init.Data.Rat.Lemmas
Rat.mul_lt_mul_of_pos_left : ∀ {a b c : ℚ}, a < b → 0 < c → c * a < c * b
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.toSubgroup_closure : ∀ {A : Type u_2} [inst : AddGroup A] (S : Set A),
  AddSubgroup.toSubgroup (AddSubgroup.closure S) = Subgroup.closure (⇑Multiplicative.toAdd ⁻¹' S)
-- Init.Data.Nat.Lemmas
Nat.add_eq_three_iff : ∀ {m n : ℕ}, m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_obj_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {E : Type u₂} [inst_1 : CategoryTheory.Groupoid E]
  (φ : CategoryTheory.Functor C E) (X : C),
  (CategoryTheory.FreeGroupoid.lift φ).obj (CategoryTheory.FreeGroupoid.mk X) = φ.obj X
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- If a compact closed set is everywhere positive with respect to a left-invariant measure on a
topological group, then it is a Gδ set. This is nontrivial, as there is no second-countability or
metrizability assumption in the statement, so a general compact closed set has no reason to be
a countable intersection of open sets.  -/
MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant : ∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G},
  μ.IsEverywherePos k → IsCompact k → IsClosed k → IsGδ k
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_comp : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDedekindDomain A] (C : Type u_3) [inst_5 : CommRing C]
  [inst_6 : Algebra B C] [inst_7 : Algebra A C] [IsScalarTower A B C] [inst_9 : Module.IsTorsionFree B C]
  [inst_10 : Module.IsTorsionFree A C] [inst_11 : IsDedekindDomain C] [inst_12 : IsDedekindDomain B],
  (ClassGroup.extendedHom B C).comp (ClassGroup.extendedHom A B) = ClassGroup.extendedHom A C
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.center_eq_top : ∀ (M : Type u_1) [inst : AddCommSemigroup M], AddSubsemigroup.center M = ⊤
-- Lean.Meta.WHNF
/-- Returns `true` if `declName` is the name of class field.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.isProjInst : Lean.Name → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Monotone convergence theorem**, version with `Measurable` functions.  -/
MeasureTheory.lintegral_iSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), Measurable (f n)) → Monotone f → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
-- Lean.Elab.Do.Basic
/-- Given a continuation `dec`, a reference `ref`, and an element result type `elementType`, returns a
continuation derived from `dec` with result type `elementType`.
If `dec` already has result type `elementType`, simply returns `dec`.
Otherwise, an error is logged and a new continuation is returned that calls `dec` with `sorry` as a
result. The error is reported at `ref`.
 -/
Lean.Elab.Do.DoElemCont.ensureHasTypeAt : Lean.Elab.Do.DoElemCont → Lean.Syntax → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.refl.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G),
  AddGroupExtension.Equiv.refl S = { toAddEquiv := AddEquiv.refl E, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Batteries.Data.MLList.Basic
/-- Take the initial segment of the lazy list,
up to and including the first place where `f` gives `true`.  -/
MLList.takeUpToFirst : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → (α → Bool) → MLList m α
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
        (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from semirings to types preserves all limits.
 -/
SemiRingCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget SemiRingCat)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.to_isTotallyComplex : ∀ {K : Type u_1} {inst : Field K} {inst_1 : CharZero K} [self : NumberField.IsCMField K], NumberField.IsTotallyComplex K
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.ofAIGAux.go.eq_def : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) (idx : ℕ)
  (state : Std.Sat.AIG.RelabelNat.State α decls idx),
  Std.Sat.AIG.RelabelNat.State.ofAIGAux.go decls idx state =
    if hidx : idx < decls.size then
      let decl := decls[idx];
      match hdecl : decl with
      | Std.Sat.AIG.Decl.atom a => Std.Sat.AIG.RelabelNat.State.ofAIGAux.go decls (idx + 1) (state.addAtom a hdecl)
      | Std.Sat.AIG.Decl.false => Std.Sat.AIG.RelabelNat.State.ofAIGAux.go decls (idx + 1) (state.addFalse hdecl)
      | Std.Sat.AIG.Decl.gate lhs rhs =>
        Std.Sat.AIG.RelabelNat.State.ofAIGAux.go decls (idx + 1) (state.addGate lhs rhs hdecl)
    else
      have this := ⋯;
      this ▸ state
-- Mathlib.Data.Seq.Defs
Stream'.Seq.mem_iff_exists_get? : ∀ {α : Type u} {s : Stream'.Seq α} {x : α}, x ∈ s ↔ ∃ i, some x = s.get? i
-- Init.Data.Sum.Lemmas
Sum.getLeft?_eq_some_iff : ∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α ⊕ β}, x.getLeft? = some a ↔ x = Sum.inl a
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is an `AddSemigroup` under pointwise operations if `α` is.  -/
Filter.addSemigroup : {α : Type u_2} → [AddSemigroup α] → AddSemigroup (Filter α)
-- Mathlib.Algebra.Group.Action.Defs
MulAction.ext : ∀ {α : Type u_9} {β : Type u_10} {inst : Monoid α} {x y : MulAction α β}, SMul.smul = SMul.smul → x = y
-- Init.Data.Vector.Zip
Vector.zip_map_left : ∀ {α : Type u_1} {γ : Type u_2} {n : ℕ} {β : Type u_3} {f : α → γ} {as : Vector α n} {bs : Vector β n},
  (Vector.map f as).zip bs = Vector.map (Prod.map f id) (as.zip bs)
-- Mathlib.Data.Finsupp.Option
Finsupp.some_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f g : Option α →₀ M), (f + g).some = f.some + g.some
-- Mathlib.Topology.Algebra.Group.Torsor
/-- A topological torsor over a topological additive group is a torsor where `+ᵥ` and `-ᵥ` are
continuous.  -/
IsTopologicalAddTorsor : {V : Type u_1} →
  [inst : AddGroup V] → [TopologicalSpace V] → (P : Type u_2) → [AddTorsor V P] → [TopologicalSpace P] → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') x
-- Lean.Elab.MutualDef
/-- Logs a snapshot task that waits for the entire snapshot tree in `defsParsedSnap` and then logs a
`goalsAccomplished` silent message for theorems and `Prop`-typed examples if the entire mutual block
is error-free and contains no syntactical `sorry`s.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask : Array Lean.Elab.DefView → Lean.Elab.DefsParsedSnapshot → Lean.Elab.TermElabM Unit
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (l : List α) → (Unit → motive []) → ((x : α) → (xs : List α) → motive (x :: xs)) → motive l
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_re_lt : ∀ (r : ℝ), Convex ℝ {c | c.re < r}
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- If `F i → f` in `L1`, then `∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ]`.  -/
MeasureTheory.VectorMeasure.tendsto_integral_of_L1 : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_8} (f : X → E),
  MeasureTheory.AEStronglyMeasurable f μ.variation →
    ∀ {F_1 : ι → X → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, μ.Integrable (F_1 i)) →
        Filter.Tendsto (fun i => ∫⁻ (x : X), ‖F_1 i x - f x‖ₑ ∂μ.variation) l (nhds 0) →
          Filter.Tendsto (fun i => ∫ᵛ (x : X), F_1 i x ∂[B; μ]) l (nhds ∫ᵛ (x : X), f x ∂[B; μ])