mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Countable unions of compact sets are σ-compact.  -/
isSigmaCompact_iUnion_of_isCompact : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [hι : Countable ι] (s : ι → Set X),
  (∀ (i : ι), IsCompact (s i)) → IsSigmaCompact (⋃ i, s i)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioc_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioc a.succ b.succ, f i = ∏ i ∈ Finset.Ioc a b, f i.succ
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coprodMonad_μ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (x : C),
  (CategoryTheory.coprodMonad X).μ.app x =
    CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ x))
-- Mathlib.Data.Finmap
Finmap.ext : ∀ {α : Type u} {β : α → Type v} {s t : Finmap β}, s.entries = t.entries → s = t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool)
  (lhs rhs : BitVec w) (n d q r : aig.RefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = false) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = false) →
          0#w < rhs →
            ∀ (idx : ℕ) (hidx : idx < w),
              ⟦assign,
                  { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w n d w 0 q r).aig,
                    ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w n d w 0 q r).q.get idx hidx }⟧ =
                (lhs / rhs).getLsbD idx
-- Mathlib.FieldTheory.SeparableDegree
/-- The minimal polynomial of an element `x` of `E / F` of exponential characteristic `q` has
separable degree one if and only if `x ^ (q ^ n) ∈ F` for some `n : ℕ`.  -/
minpoly.natSepDegree_eq_one_iff_pow_mem : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [hF : ExpChar F q] {x : E}, (minpoly F x).natSepDegree = 1 ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ofSuppBddBelow.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ] (f f_1 : Γ → R)
  (e_f : f = f_1) (hf : BddBelow (Function.support f)), HahnSeries.ofSuppBddBelow f hf = HahnSeries.ofSuppBddBelow f_1 ⋯
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_absolutelyContinuous : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → (ProbabilityTheory.gaussianReal μ v).AbsolutelyContinuous MeasureTheory.volume
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasRecursiveType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.instIsGrothendieckAbelian : ∀ {C : Type v} [inst : CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₁)
  [inst_1 : CategoryTheory.Category.{v₁, u₁} A] [inst_2 : CategoryTheory.Abelian A]
  [CategoryTheory.IsGrothendieckAbelian.{v, v₁, u₁} A] [inst_4 : CategoryTheory.HasSheafify J A],
  CategoryTheory.IsGrothendieckAbelian.{v, max v v₁, max (max (max u₁ v) v₁) v} (CategoryTheory.Sheaf J A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldl_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DTreeMap.foldl f init t = List.foldl (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.comp : ∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ),
  Nat.Primrec' f → (∀ (i : Fin n), Nat.Primrec' (g i)) → Nat.Primrec' fun a => f (List.Vector.ofFn fun i => g i a)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- The equalizer condition is preserved by natural isomorphism.  -/
CategoryTheory.regularTopology.equalizerCondition_of_natIso : ∀ {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] {P P' : CategoryTheory.Functor Cᵒᵖ D} (i : P ≅ P'),
  CategoryTheory.regularTopology.EqualizerCondition P → CategoryTheory.regularTopology.EqualizerCondition P'
-- Mathlib.Algebra.Divisibility.Basic
rightDvd_iff_dvd : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ᵣ b ↔ a ∣ b
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h).inv (K.pOpcycles j) =
    CategoryTheory.CategoryStruct.id (K.opcycles j)
-- Mathlib.Data.Multiset.ZeroCons
_private.Mathlib.Data.Multiset.ZeroCons.0.Multiset.rel_flip_aux : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β},
  Multiset.Rel r s t → Multiset.Rel (flip r) t s
-- Mathlib.Analysis.SpecialFunctions.Exp
Filter.Tendsto.cexp : ∀ {α : Type u_1} {l : Filter α} {f : α → ℂ} {z : ℂ},
  Filter.Tendsto f l (nhds z) → Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds (Complex.exp z))
-- Mathlib.Control.Traversable.Lemmas
Traversable.id_sequence : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {α : Type u} (x : t α),
  sequence (pure <$> x) = pure x
-- Mathlib.Data.Bundle
Bundle.TotalSpace.snd : {B : Type u_1} → {F : Type u_4} → {E : B → Type u_5} → (self : Bundle.TotalSpace F E) → E self.proj
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.lt_iff_exists_lt : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsPredPrelimit b → (b < a ↔ ∃ c, b < c ∧ c < a)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Reformulation of the doubling formula in terms of `Gammaℝ`.  -/
Complex.Gammaℝ_mul_Gammaℝ_add_one : ∀ (s : ℂ), s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.gaussNorm_nonneg : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  (∀ (a : R), v a ≥ 0) → 0 ≤ PowerSeries.gaussNorm v c f
-- Mathlib.Order.Category.BoolAlg
BoolAlg.coe_id : ∀ {X : BoolAlg}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.mk.inj : ∀ {fvarId : Lean.FVarId} {userName : Lean.Name} {id : Lean.Meta.Origin} {origType type proof : Lean.Expr}
  {fvarId_1 : Lean.FVarId} {userName_1 : Lean.Name} {id_1 : Lean.Meta.Origin} {origType_1 type_1 proof_1 : Lean.Expr},
  { fvarId := fvarId, userName := userName, id := id, origType := origType, type := type, proof := proof } =
      { fvarId := fvarId_1, userName := userName_1, id := id_1, origType := origType_1, type := type_1,
        proof := proof_1 } →
    fvarId = fvarId_1 ∧ userName = userName_1 ∧ id = id_1 ∧ origType = origType_1 ∧ type = type_1 ∧ proof = proof_1
-- Mathlib.LinearAlgebra.Trace
/-- When `M` is finite free, the trace of a linear map corresponds to the contraction pairing under
the isomorphism `End(M) ≃ M* ⊗ M`.  -/
LinearMap.trace_eq_contract : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M], LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.keep : (basis_hd : ℝ → ℝ) →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.BasisExtension basis_tl → Tactic.ComputeAsymptotics.BasisExtension (basis_hd :: basis_tl)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.diagonal_updateCol_single : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (v : n → α) (i : n) (x : α),
  (Matrix.diagonal v).updateCol i (Pi.single i x) = Matrix.diagonal (Function.update v i x)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.get! m₁ k
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.fieldIdx.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → (s.dropEndWhile pat).copy = (t.dropEndWhile pat).copy
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.density_sub_eps_le_sum_density_div_card : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts} {A B : Finset (Finset α)},
        A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts →
          B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts →
            ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
              (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
-- Lean.ResolveName
/-- Like `Lean.unresolveNameGlobalAvoidingLocals?`, but returns `n₀` unchanged if the name cannot be referred to.  -/
Lean.unresolveNameGlobalAvoidingLocals : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] → [Lean.MonadLCtx m] → Lean.Name → optParam Bool false → m Lean.Name
-- Mathlib.Data.Ordering.Basic
/-- `Compares o a b` means that `a` and `b` have the ordering relation `o` between them, assuming
that the relation `a < b` is defined.  -/
Ordering.Compares : {α : Type u_1} → [LT α] → Ordering → α → α → Prop
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  [inst_2 : SizeOf α] (n₀ : ℕ) (n₀_gt_zero : 0 < n₀) (a_pos : ∀ (i : α), 0 < a i) (b_pos : ∀ (i : α), 0 < b i)
  (b_lt_one : ∀ (i : α), b i < 1) (g_nonneg : ∀ x ≥ 0, 0 ≤ g x) (g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g)
  (h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) (T_gt_zero' : ∀ n < n₀, 0 < T n)
  (r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n)
  (dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2),
  sizeOf
      { n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
        g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n,
        dist_r_b := dist_r_b } =
    1 + sizeOf n₀ + sizeOf n₀_gt_zero
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_mul_inl : ∀ {R : Type u} {M : Type v} [inst : MonoidWithZero R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M),
  TrivSqZeroExt.inr m * TrivSqZeroExt.inl r = TrivSqZeroExt.inr (MulOpposite.op r • m)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β}, k' ∈ Std.ExtDTreeMap.Const.modify t k f ↔ k' ∈ t
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabWhere : Lean.Elab.Command.CommandElab
-- Lean.Meta.Offset
/-- Checks that expression `e` is definitional equal to `inst`.

Uses `instances` transparency so that reducible terms and instances extended
other instances are unfolded.
 -/
Lean.Meta.matchesInstance : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Http.Data.Status
/-- 208 Already Reported
 -/
Std.Http.Status.alreadyReported : Std.Http.Status
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_add' : ∀ {α : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α] (f : α → M) (a b c : α),
  ∏ x ∈ Finset.Ico a b, f (x + c) = ∏ x ∈ Finset.Ico (a + c) (b + c), f x
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplex_counitIso : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.dgoEquivHomologicalComplex b V).counitIso =
    HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.inv_add_inv_eq_inv : ∀ (p q : ENNReal) (r : semiOutParam ENNReal) [self : p.HolderTriple q r], p⁻¹ + q⁻¹ = r⁻¹
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], CauSeq.Completion.ofRat 1 = 1
-- Mathlib.CategoryTheory.Category.Basic
/-- A `SmallCategory` has objects and morphisms in the same universe level.
 -/
CategoryTheory.SmallCategory : Type u → Type (u + 1)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatchAt_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt p pos pos' ↔
    ∃ (h : pos' ≠ s.startPos), pos = pos'.prev h ∧ p ((pos'.prev h).get ⋯) = true
-- Lean.Setup
/-- Phases for which some IR is available for execution.  -/
Lean.IRPhases : Type
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Formula for the distance between the images of two nonzero points under an inversion with center
zero. See also `EuclideanGeometry.dist_inversion_inversion` for inversions around a general
point.  -/
dist_div_norm_sq_smul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  x ≠ 0 → y ≠ 0 → ∀ (R : ℝ), dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iio_mul_bij : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Set.BijOn (fun x => x * a) (Set.Iio b) (Set.Iio (b * a))
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_toLocallyRingedSpace : ∀ (R : CommRingCat), (AlgebraicGeometry.Spec R).toLocallyRingedSpace = AlgebraicGeometry.Spec.locallyRingedSpaceObj R
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
/-- Given a polynomial `f ∈ R[x]`, `imageOfDf` is the subset of `Spec R` where at least one
of the coefficients of `f` does not vanish.  Lemma `imageOfDf_eq_comap_C_compl_zeroLocus`
proves that `imageOfDf` is the image of `(zeroLocus {f})ᶜ` under the morphism
`comap C : Spec R[x] → Spec R`.  -/
AlgebraicGeometry.Polynomial.imageOfDf : {R : Type u_1} → [inst : CommRing R] → Polynomial R → Set (PrimeSpectrum R)
-- Mathlib.Order.Antichain
/-- The intersection of a chain and an antichain is subsingleton.  -/
inter_subsingleton_of_isChain_of_isAntichain : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsChain r s → IsAntichain r t → (s ∩ t).Subsingleton
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum of finite terms is finite.  -/
WithBot.sum_lt_bot : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M} [inst_1 : LT M],
  (∀ i ∈ s, f i ≠ ⊥) → ⊥ < ∑ i ∈ s, f i
-- Mathlib.Analysis.Real.Sqrt
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`.  -/
Real.sum_mul_le_sqrt_mul_sqrt : ∀ {ι : Type u_2} (s : Finset ι) (f g : ι → ℝ), ∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2)
-- Init.Data.Float.Model.Float
/-- The underlying bit pattern of the `Float.Model`.  -/
Float.Model.toBits : Float.Model → UInt64
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.pow_two_mem : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) (x : R), x ^ 2 ∈ P
-- Mathlib.SetTheory.ZFC.PSet
/-- The n-th von Neumann ordinal  -/
PSet.ofNat : ℕ → PSet.{u_1}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insert.match_3.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isFibrant_of_fibration : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] {X Y : C}
  (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] [hY : HomotopicalAlgebra.IsFibrant Y], HomotopicalAlgebra.IsFibrant X
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.inv_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R) (y : ↥(ValuativeRel.posSubmonoid R))
  (hx : ¬x ≤ᵥ 0), (ValuativeRel.ValueGroupWithZero.mk x y)⁻¹ = ValuativeRel.ValueGroupWithZero.mk ↑y ⟨x, hx⟩
-- Mathlib.Data.Set.Lattice
Set.nonempty_sUnion : ∀ {α : Type u_1} {S : Set (Set α)}, (⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty
-- Mathlib.Data.Nat.ModEq
Nat.add_div_of_dvd_right : ∀ {a b c : ℕ}, c ∣ a → (a + b) / c = a / c + b / c
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Arity of the function  -/
ValuedCSP.Term.n : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] → [inst_2 : IsOrderedAddMonoid C] → {Γ : ValuedCSP D C} → {ι : Type u_3} → Γ.Term ι → ℕ
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor_comp_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p p' p'' : Submodule R M} (H1 : p ≤ p') (H2 : p' ≤ p'') (x : M ⧸ p),
  (Submodule.factor H2) ((Submodule.factor H1) x) = (Submodule.factor ⋯) x
-- Mathlib.Data.Num.Basic
/-- Auxiliary definition for `PosNum.divMod`.  -/
PosNum.divModAux : PosNum → Num → Num → Num × Num
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig : Type
-- Mathlib.Geometry.Manifold.Riemannian.Basic
eventually_norm_mfderivWithin_symm_extChartAt_comp_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow h
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullbackLift_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] {S S' X Y : C} (f : S' ⟶ S) {v₁₂ : X ⟶ S} {v₂₂ : Y ⟶ S} {g : X ⟶ Y}
  (hv₁₂ : v₁₂ = CategoryTheory.CategoryStruct.comp g v₂₂) [inst_2 : CategoryTheory.Limits.HasPullback v₁₂ f]
  [inst_3 : CategoryTheory.Limits.HasPullback v₂₂ f],
  P g →
    P
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst v₁₂ f) g)
        (CategoryTheory.Limits.pullback.snd v₁₂ f) ⋯)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (r : α),
  Lean.Grind.Linarith.Poly.denote'.go ctx r Lean.Grind.Linarith.Poly.nil = r
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.drop : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → ∀ (n : ℕ), (p.drop n).IsPath
-- Mathlib.Algebra.Homology.Linear
CategoryTheory.Functor.mapHomologicalComplex_linear : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  {ι : Type u_4} (F : CategoryTheory.Functor C D) [inst_7 : F.Additive] [CategoryTheory.Functor.Linear R F]
  (c : ComplexShape ι), CategoryTheory.Functor.Linear R (F.mapHomologicalComplex c)
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_eq_zero : ∀ {xs : Lean.Omega.IntList}, xs.gcd = 0 ↔ ∀ x ∈ xs, x = 0
-- Mathlib.Topology.UnitInterval
unitInterval.instNontrivialElemReal : Nontrivial ↑unitInterval
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.comp_id : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (x : E), p.comp (FormalMultilinearSeries.id 𝕜 E x) = p
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` vanishes iff `a` and `b` are not coprime (assuming `b ≠ 0`).  -/
jacobiSym.eq_zero_iff_not_coprime : ∀ {a : ℤ} {b : ℕ} [NeZero b], jacobiSym a b = 0 ↔ a.gcd ↑b ≠ 1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- **Chinese Remainder Theorem**. Eisenbud Ex.2.6.
Similar to Atiyah-Macdonald 1.10 and Stacks 00DT  -/
Ideal.quotientInfRingEquivPiQuotient : {R : Type u_2} →
  [inst : CommRing R] →
    {ι : Type u_3} →
      [Finite ι] → (f : ι → Ideal R) → Pairwise (Function.onFun IsCoprime f) → R ⧸ ⨅ i, f i ≃+* ((i : ι) → R ⧸ f i)
-- Init.SimpLemmas
have_unused_dep' : ∀ {α : Sort u} {β : Sort v} (a : α) {b : α → β} {b' : β}, (∀ (x : α), b x = b') → b a = b'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  (p q : ℤ) (hpq : p + 1 = q),
  (CochainComplex.mappingCone.desc φ α β eq).f p =
    CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) (α.v q p ⋯) +
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯) (β.f p)