mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀ : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → ℝ},
      MeasureTheory.AEStronglyMeasurable f μ →
        MeasureTheory.Integrable g μ → ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[f * g | m] =ᵐ[μ] f * μ[g | m]
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.domRestrict_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₁ M₁) (x : ↥p), (f.domRestrict p) x = f ↑x
-- Mathlib.Order.Filter.NAry
Filter.map₂_left_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {f : Filter α}
  {g : Filter β} {h : Filter γ} {m : α → δ → ε} {n : β → γ → δ} {m' : α → γ → δ'} {n' : β → δ' → ε},
  (∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)) →
    Filter.map₂ m f (Filter.map₂ n g h) = Filter.map₂ n' g (Filter.map₂ m' f h)
-- Lean.DocString.Markdown
/-- A set of registered Markdown renderers, keyed by custom element type names.
 -/
Lean.Doc.MdRendererState : Type
-- Init.Data.List.TakeDrop
List.take.eq_3 : ∀ {α : Type u} (n : ℕ) (a : α) (as : List α), List.take n.succ (a :: as) = a :: List.take n as
-- Init.Data.List.Sort.Lemmas
List.mem_merge_left : ∀ {α : Type u_1} {l : List α} {x : α} {r : List α} (s : α → α → Bool), x ∈ l → x ∈ l.merge r s
-- Lean.Data.Lsp.Extra
/-- `$/lean/rpc/connect` client<-server reply.

Indicates that an RPC connection had been made and a session started for it.  -/
Lean.Lsp.RpcConnected : Type
-- Init.Data.Nat.Lemmas
Nat.eq_mul_of_div_eq_right : ∀ {a b c : ℕ}, b ∣ a → a / b = c → a = b * c
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.toContinuousAffineMap_id : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  AffineIsometry.id.toContinuousAffineMap = ContinuousAffineMap.id 𝕜 P
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.degree_pos_of_nontrivial : ∀ {V : Type u} [Nontrivial V] {G : SimpleGraph V},
  G.Preconnected → ∀ (v : V) [inst : Fintype ↑(G.neighborSet v)], 0 < G.degree v
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_apply_coe : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (t : ↑unitInterval) (x : X), (F.extend ↑t) x = F (t, x)
-- Batteries.Data.Array.Scan
Array.scanl_reverse : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  Array.scanl f init as.reverse = (Array.scanr (flip f) init as).reverse
-- Lean.Expr
Lean.instInhabitedFVarIdHashSet : Inhabited Lean.FVarIdHashSet
-- Mathlib.Topology.Separation.Basic
/-- A topology inducing map from a T₀ space is injective.  -/
Topology.IsInducing.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space X] {f : X → Y},
  Topology.IsInducing f → Function.Injective f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? =
    Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least)
-- Mathlib.Algebra.Torsor.Basic
Prod.mk_vadd_mk : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (v : G) (v' : G') (p : P) (p' : P'),
  (v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_getD : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, a ∈ m → m.get? a = some (m.getD a fallback)
-- Mathlib.Algebra.Free
/-- `FreeMagma` is traversable.  -/
FreeMagma.traverse : {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.List.compareLex.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      (Unit → motive [] []) →
        ((x : List α) → (x = [] → False) → motive [] x) →
          ((x : List α) → (x = [] → False) → motive x []) →
            ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive x x_1
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.prefix.inj : ∀ {s s_1 : Lean.Grind.AC.Seq}, Lean.Grind.AC.SubseqResult.prefix s = Lean.Grind.AC.SubseqResult.prefix s_1 → s = s_1
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.le_inf_support_coeff_finsetProd`. -/
AddMonoidAlgebra.le_inf_support_finsetProd : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} {ι : Type u_6} [inst : SemilatticeInf T] [inst_1 : OrderTop T]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid T] [AddLeftMono T] [AddRightMono T]
  {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        ∑ i ∈ s, (f i).coeff.support.inf degt ≤ (∏ i ∈ s, f i).coeff.support.inf degt
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.coe_sum : ∀ {α : Type u_1} {ι : Type u_2} [inst : AddCommMonoid α] [inst_1 : DecidableEq α] (s : Finset ι) (f : ι → Finset α),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerived_fac_app_assoc : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F) (X : C) {Z : H}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((LF.leftDerivedLift α W G β).app (L.obj X))
      (CategoryTheory.CategoryStruct.comp (α.app X) h) =
    CategoryTheory.CategoryStruct.comp (β.app X) h
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.mk.sizeOf_spec : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toInfTopHom : InfTopHom α β)
  (map_sSup' : ∀ (s : Set α), toInfTopHom.toFun (sSup s) = sSup (toInfTopHom.toFun '' s)),
  sizeOf { toInfTopHom := toInfTopHom, map_sSup' := map_sSup' } = 1 + sizeOf toInfTopHom
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instAddMonoidHomClassAddHom_1 : ∀ {M : Type u_10} {N : Type u_11} [inst : AddMonoid M] [inst_1 : AddRightCancelMonoid N],
  AddMonoidHomClass (M →ₙ+ N) M N
-- Init.System.Platform
System.Platform.instNeZeroNatNumBits : NeZero System.Platform.numBits
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.Abelian.tfae_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (Z : C),
  [CategoryTheory.Mono f, CategoryTheory.Limits.kernel.ι f = 0,
      { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE
-- Mathlib.Algebra.BigOperators.Finprod
MonoidHom.map_finprod : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {f : α → M} (g : M →* N),
  Function.HasFiniteMulSupport f → g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_lt_one_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] [Nontrivial Γ₀] {x : R}, 1 x < 1 ↔ x = 0
-- Aesop.Frontend.Extension
Aesop.Frontend.getDefaultGlobalRuleSets : Lean.CoreM (Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name))
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_zero : Ordinal.preOmega 0 = 0
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.equivalenceOfReindexing`.

---

The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
 -/
CategoryTheory.Limits.Cones.equivalenceOfReindexing : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {G : CategoryTheory.Functor K C} →
                (e : K ≌ J) → (e.functor.comp F ≅ G) → (CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.natTrans_ext : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W]
  {F₁ F₂ : CategoryTheory.Functor D E} {τ τ' : F₁ ⟶ F₂}, (∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)) → τ = τ'
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- The partial sums of a formal multilinear series are continuous.  -/
FormalMultilinearSeries.partialSum_continuous : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), Continuous (p.partialSum n)
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.iget_map : ∀ {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} [inst : DecidableEq P.A] [inst_1 : Inhabited α]
  [inst_2 : Inhabited β] (x : ↑P α) (f : α → β) (i : P.Idx), i.fst = x.fst → (P.map f x).iget i = f (x.iget i)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circle average of a nonnegative function is nonnegative.
 -/
Real.circleAverage_nonneg_of_nonneg : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ}, (∀ x ∈ Metric.sphere c |R|, 0 ≤ f x) → 0 ≤ Real.circleAverage f c R
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- This is the same as `ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq`, where
`embed` is upgraded to `orderMonoidIso`.  -/
ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (γ : ValuativeRel.ValueGroupWithZero R),
  MonoidWithZeroHom.ValueGroup₀.embedding
      ((ValuativeRel.ValueGroupWithZero.orderMonoidIso (ValuativeRel.valuation R)) γ) =
    γ
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.nsmul_le_nsmul : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.NatModule M] [Lean.Grind.OrderedAdd M]
  {k : ℕ} {a b : M}, a ≤ b → k • a ≤ k • b
-- Init.Data.Random
instReprStdGen : Repr StdGen
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.left_notMem_uIoo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ∉ Set.uIoo a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {k : α} {v : β},
  Std.DTreeMap.Raw.Const.ofList [(k, v)] cmp = ∅.insert k v
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.union.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₂ : Std.ExtTreeMap α β cmp),
  t₁.union t₂ = { inner := t₁.inner.union t₂.inner }
-- Mathlib.Data.NNReal.Defs
NNReal.instAddCancelCommMonoid : AddCancelCommMonoid NNReal
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_fdiv_left : ∀ (b : ℤ) {a : ℤ} (c : ℤ), a ≠ 0 → (a * b + c).fdiv a = c.fdiv a + b
-- Mathlib.Data.Rat.Lemmas
Rat.natCast_sub_den : ∀ (n : ℕ) (q : ℚ), (↑n - q).den = q.den
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instInvolutiveStarSubtypeAEEqFunMemAddSubgroup : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {R : Type u_6} →
        [inst : NormedAddCommGroup R] →
          [inst_1 : StarAddMonoid R] → [NormedStarGroup R] → {p : ENNReal} → InvolutiveStar ↥(MeasureTheory.Lp R p μ)
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  (ModuleCat.localizedModuleFunctor S).PreservesProjectiveObjects
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_one : ∀ {F : Type u} [inst : Field F], Polynomial.natSepDegree 1 = 0
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.emb_zero : ∀ {n : ℕ} (c : OrderedFinpartition n) [inst : NeZero n], c.emb (c.index 0) 0 = 0
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.delayedAssignment : Lean.DelayedMetavarAssignment → Aesop.EqualUpToIds.MVarValue
-- Mathlib.Analysis.Convex.StdSimplex
/-- The (sup metric) diameter of a standard simplex indexed by a subsingleton is 0.  -/
diam_stdSimplex_of_subsingleton : ∀ {ι : Type u_1} [inst : Fintype ι] [Subsingleton ι], Metric.diam (stdSimplex ℝ ι) = 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.prod_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (f : MultilinearMap R M₁ M₂)
  (g : MultilinearMap R M₁ M₃) (m : (i : ι) → M₁ i), (f.prod g) m = (f m, g m)
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Bijective ⇑(algebraMap R S) → Algebra.IsStandardSmoothOfRelativeDimension 0 R S
-- Init.Data.SInt.Lemmas
ISize.toInt16_toInt32 : ∀ (n : ISize), n.toInt32.toInt16 = n.toInt16
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Init.Data.List.Impl
List.eraseIdx.eq_3 : ∀ {α : Type u} (a : α) (as : List α) (n : ℕ), (a :: as).eraseIdx n.succ = a :: as.eraseIdx n
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.AlmostMono.mk.congr_simp : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} (line line_1 : Combinatorics.Line (Option α) ι)
  (e_line : line = line_1) (color color_1 : κ) (e_color : color = color_1)
  (has_color : ∀ (x : α), C (↑line (some x)) = color),
  { line := line, color := color, has_color := has_color } = { line := line_1, color := color_1, has_color := ⋯ }
-- Mathlib.LinearAlgebra.Complex.Module
Complex.ofRealAm_coe : ⇑Complex.ofRealAm = Complex.ofReal
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `mul_right_cancel`. -/
mul_right_cancel'' : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.ofBijective_apply : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M), (AddEquiv.ofBijective f hf) a = f a
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.map_iterateFrobenius_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) [inst_1 : ExpChar R p] (f : MvPowerSeries σ R)
  (n : ℕ), (MvPowerSeries.map (iterateFrobenius R p n)) ((MvPowerSeries.expand (p ^ n) ⋯) f) = f ^ p ^ n
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.exists_isNIndepSet_indepNum : ∀ {α : Type u_3} {G : SimpleGraph α}, ∃ s, G.IsNIndepSet G.indepNum s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.subsingleton_of_subsingleton_span_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P}, s.Subsingleton → affineSpan k s = ⊤ → Subsingleton P
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.iInf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_2} (S : ι → NonUnitalSubalgebra R A),
  (⨅ i, S i).toSubmodule = ⨅ i, (S i).toSubmodule
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The partial inverse to `toFun`. Its value outside of the `target` subset is irrelevant.  -/
PartialEquiv.invFun : {α : Type u_5} → {β : Type u_6} → PartialEquiv α β → β → α
-- Mathlib.Tactic.DepRewrite
/-- The cast mode specifies when `rewrite!` is permitted to insert casts
in order to correct subterms that become type-incorrect
as a result of rewriting.

For example, given `P : Nat → Prop`, `f : (n : Nat) → P n → Nat` and `h : P n₀`,
rewriting `f n₀ h` by `eq : n₀ = n₁` produces `f n₁ h`,
where `h` does not typecheck at `P n₁`.
The tactic will cast `h` to `eq ▸ h : P n₁` iff `.proofs ≤ castMode`.  -/
Mathlib.Tactic.DepRewrite.Config.castMode : Mathlib.Tactic.DepRewrite.Config → Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- An orientation-reversing isometry of the hyperbolic plane has a fixed point
iff the corresponding matrix has zero trace.  -/
UpperHalfPlane.exists_gl_smul_eq_self_iff_trace_eq_zero : ∀ {g : GL (Fin 2) ℝ}, (↑g).det < 0 → ((∃ z, g • z = z) ↔ (↑g).trace = 0)
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.submoduleOf_eq_top : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M}, p.submoduleOf q = ⊤ ↔ q ≤ p
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toWithBotNat_zero : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsDiscreteValuationRing.toWithBotNat 0 = ⊥
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instAddCommGroupRepr : {R : Type u_1} → [inst : Ring R] → (x : FGModuleRepr R) → AddCommGroup x.repr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A measure is a vector measure over `ℝ≥0∞`.  -/
MeasureTheory.Measure.toENNRealVectorMeasure : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.VectorMeasure α ENNReal
-- Mathlib.Data.W.Constructions
WType.Natα.noConfusionType : Sort v✝ → WType.Natα → WType.Natα → Sort v✝
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.
("The maximum is at least the mean" specialized to integers.)

More formally, given a function between finite sets `s` and `t` and a natural number `n` such that
`#t * n < #s`, there exists `y ∈ t` such that its preimage in `s` has more than `n`
elements.  -/
Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  (∀ a ∈ s, f a ∈ t) → t.card * n < s.card → ∃ y ∈ t, n < {x ∈ s | f x = y}.card
-- Mathlib.Algebra.Group.Defs
add_left_injective : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] (a : G), Function.Injective fun x => x + a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Cfg.mk.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {l : Option Λ} {var : σ} {stk : (k : K) → List (Γ k)}
  {l_1 : Option Λ} {var_1 : σ} {stk_1 : (k : K) → List (Γ k)},
  { l := l, var := var, stk := stk } = { l := l_1, var := var_1, stk := stk_1 } → l = l_1 ∧ var = var_1 ∧ stk = stk_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_left_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α}, (fun x => a + x) ⁻¹' {b} = {-a + b}
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.false.sizeOf_spec : sizeOf Lean.Meta.ArrowPropResult.false✝ = 1
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- If `a` is even and `b` is odd, then we can remove a factor `2` from `a`,
but we may have to change the sign, depending on `b % 8`.
We give one version for each of the four odd residue classes mod `8`.  -/
Mathlib.Meta.NormNum.jacobiSymNat.even_odd₁ : ∀ (a b c : ℕ) (r : ℤ),
  a % 2 = 0 →
    b % 8 = 1 → a / 2 = c → Mathlib.Meta.NormNum.jacobiSymNat c b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The roots of `cyclotomic' n R` are the primitive `n`-th roots of unity.  -/
Polynomial.roots_of_cyclotomic : ∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R],
  (Polynomial.cyclotomic' n R).roots = (primitiveRoots n R).val
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The delaborated right-hand sides for each match alternative.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.rhss : Lean.PrettyPrinter.Delaborator.AppMatchState → Array Lean.Term
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version for sums over finite sets, with `ℝ≥0∞`-valued
functions and real exponents.  -/
ENNReal.rpow_arith_mean_le_arith_mean_rpow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ENNReal),
  ∑ i ∈ s, w i = 1 → ∀ {p : ℝ}, 1 ≤ p → (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.ext_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  {R S : HomogeneousSubsemiring 𝒜}, R = S ↔ R.toSubsemiring = S.toSubsemiring
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively,
`p.quotient` is isomorphic to `q.quotient`.  -/
FiniteDimensional.LinearEquiv.quotEquivOfEquiv : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {V₂ : Type v'} →
            [inst_3 : AddCommGroup V₂] →
              [inst_4 : Module K V₂] →
                [FiniteDimensional K V] →
                  [FiniteDimensional K V₂] →
                    {p : Subspace K V} → {q : Subspace K V₂} → (↥p ≃ₗ[K] ↥q) → (V ≃ₗ[K] V₂) → (V ⧸ p) ≃ₗ[K] V₂ ⧸ q
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

This function is deprecated. Instead of `it.allowNontermination.find?`, use `it.find?`.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 1) = none`
 -/
Std.Iter.Partial.find? : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter.Partial β → (β → Bool) → Option β