mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k fallback : α}, m₂.contains k = true → (m₁.inter m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Order.RelIso.Basic
RelIso.instEquivLike : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → EquivLike (r ≃r s) α β
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.map_id : ∀ (p : ENNReal) {V : Type u_4}, WithLp.map p id = id
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.vadd_apply : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : VAdd M α] (c : Mᵈᵃᵃ) (f : α → β) (a : α),
  (c +ᵥ f) a = f (DomAddAct.mk.symm c +ᵥ a)
-- Lean.Elab.App
/-- If the function being applied is a constant, search `namedArgs` for an argument whose name is
a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
error). The returned `namedArg` retains its original (old) name.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.findDeprecatedBinderName? : List Lean.Elab.Term.NamedArg → Lean.Expr → Lean.Name → Lean.Elab.TermElabM (Option Lean.Elab.Term.NamedArg)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Submodule.coe_toSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Submodule R A)
  (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p), ↑(p.toSubalgebra h_one h_mul) = p.carrier
-- Mathlib.ModelTheory.Algebra.Field.CharP
/-- The first-order theory of fields of characteristic `p` as a theory over the language of rings  -/
FirstOrder.Language.Theory.fieldOfChar : ℕ → FirstOrder.Language.ring.Theory
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_two_mul_add_one : ∀ {α : Type u_4} {f : α → α}, Function.Involutive f → ∀ (n : ℕ), f^[2 * n + 1] = f
-- Mathlib.Dynamics.FixedPoints.Basic
Function.Injective.isFixedPt_apply_iff : ∀ {α : Type u_1} {f : α → α}, Function.Injective f → ∀ {x : α}, Function.IsFixedPt f (f x) ↔ Function.IsFixedPt f x
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {p : ENNReal} (f g : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 →
    p ≠ ⊤ →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ) →
        (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑g) s μ) →
          (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ) →
            ↑↑f =ᵐ[μ] ↑↑g
-- Lean.Message
Lean.MessageData.compose.injEq : ∀ (a a_1 a_2 a_3 : Lean.MessageData), (a.compose a_1 = a_2.compose a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Data.Set.Image
Set.subset_preimage_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s ⊆ f ⁻¹' f '' s
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (x : K),
  x ∈ (Localization.mapToFractionRing K S B hS).range ↔
    ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
NumberField.discr_eq_discr_of_algEquiv : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {L : Type u_2} [inst_2 : Field L] [inst_3 : NumberField L]
  (f : K ≃ₐ[ℚ] L), NumberField.discr K = NumberField.discr L
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- The proposition that a bilinear form is alternating  -/
LinearMap.BilinForm.IsAlt : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.inr_apply : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (i : M₂),
  (QuadraticMap.Isometry.inr Q₁ Q₂) i = (0, i)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.mem_orderTopSubOnePos_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : (HahnSeries Γ R)ˣ), x ∈ HahnSeries.orderTopSubOnePos Γ R ↔ 0 < (↑x - 1).orderTop
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.continuousAt_const_smul_iff : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {c : M},
  IsUnit c → (ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.rankFinite : ∀ {α : Type u_1} {N M : Matroid α} [M.RankFinite], N.IsRestriction M → N.RankFinite
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isSupFiniteCompact_iff_all_elements_compact : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `P` is stable under composition and `f : X ⟶ Y` satisfies `P`,
this is the functor `P.Under Q Y ⥤ P.Under Q X` given by composing with `f`.  -/
CategoryTheory.MorphismProperty.Under.map : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          {X Y : T} →
            [P.IsStableUnderComposition] → {f : X ⟶ Y} → P f → CategoryTheory.Functor (P.Under Q Y) (P.Under Q X)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The ordering on ring topologies on the ring `R`.
`t ≤ s` if every set open in `s` is also open in `t` (`t` is finer than `s`).  -/
RingTopology.instPartialOrder : {R : Type u_1} → [inst : Ring R] → PartialOrder (RingTopology R)
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap'` with the application of additive functors  -/
Homotopy.map_nullHomotopicMap' : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [inst_4 : G.Additive]
  (hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
  (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap' hom) =
    Homotopy.nullHomotopicMap' fun i j hij => G.map (hom i j hij)
-- Mathlib.FieldTheory.Separable
Polynomial.isUnit_of_self_mul_dvd_separable : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R}, p.Separable → q * q ∣ p → IsUnit q
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_comp_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : B × C} (f : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)) (g : (Y.1 ⟶ Z.1) × (Y.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).2 = CategoryTheory.CategoryStruct.comp f.2 g.2
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.Internal.List.containsKey a l)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.sup_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (W W' : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y), (W ⊔ W') f ↔ W f ∨ W' f
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_mul_add : ∀ {x y : ENNReal}, (x * y).log = x.log + y.log
-- Mathlib.Algebra.GCDMonoid.Nat
Int.instGCDMonoid : GCDMonoid ℤ
-- Init.Data.UInt.Lemmas
UInt16.ofNat_le_iff : ∀ {n : UInt16} {m : ℕ}, m < UInt16.size → (UInt16.ofNat m ≤ n ↔ m ≤ n.toNat)
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Iio : ∀ {α : Type u_1} [inst : LinearOrder α], IsPiSystem (Set.range Set.Iio)
-- Init.Data.Format.Basic
/-- A position where a newline may be inserted if the current group does not fit within the allotted
column width.
 -/
Std.Format.line : Std.Format
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.sphere.instContinuousMul : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜],
  ContinuousMul ↑(Metric.sphere 0 1)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The polynomial `X - r` has spectral value `‖ r ‖`.  -/
spectralValue_X_sub_C : ∀ {R : Type u_1} [inst : SeminormedRing R] [Nontrivial R] (r : R), spectralValue (Polynomial.X - Polynomial.C r) = ‖r‖
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_erase_eq_of_not_compare_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.minKey ⋯) = Ordering.eq → (t.erase k).minKey he = t.minKey ⋯
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.map_η_comp_η_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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η e.functor) h) =
    CategoryTheory.CategoryStruct.comp (e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h
-- Mathlib.Data.List.Induction
/-- A dependent recursion principle for nonempty lists. Useful for dealing with
operations like `List.head` which are not defined on the empty list.
Same as `List.recNeNil`, with a more convenient argument order.
 -/
List.recOnNeNil : {α : Type u_1} →
  {motive : (l : List α) → l ≠ [] → Sort u_2} →
    (l : List α) →
      (h : l ≠ []) →
        ((x : α) → motive [x] ⋯) →
          ((x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) → motive l h
-- Init.WF
PSigma.RevLex.right : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β},
  s b₁ b₂ → PSigma.RevLex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.continuous_range_of_finite : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} [Finite ι], Continuous Set.range
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.mulIsInitial_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  {I : C} (X : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.Limits.mulIsInitial X hI).hom = CategoryTheory.Limits.prod.snd
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app : ∀ (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Group.Center
Set.zero_mem_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : AddZeroClass M], 0 ∈ S.addCentralizer
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.ennrealOfReal : ∀ {p q : ℝ}, p.HolderConjugate q → (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.sum_filter_pairs_eq_sum_powersetCard_mem_filter_antidiagonal_sum : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : DecidableEq σ] [inst_2 : Fintype σ] (k : ℕ),
  ∀ a ∈ {a ∈ Finset.HasAntidiagonal.antidiagonal k | a.1 < k},
    ∀ (f : Finset σ × σ → MvPolynomial σ R),
      ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k with t.1.card = a.1, f t =
        ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j, f (A, j)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_antiperiod : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Periodic f c₁ → Function.Antiperiodic f c₂ → Function.Antiperiodic f (c₁ - c₂)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_ne_nil : ∀ {α : Type u} {x : α} {s : Stream'.Seq α}, Stream'.Seq.cons x s ≠ Stream'.Seq.nil
-- Mathlib.Algebra.Free
FreeSemigroup.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeSemigroup.map f = FreeSemigroup.lift (FreeSemigroup.of ∘ f)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instInfSet : {ι : Type u_1} → InfSet (AbstractSimplicialComplex ι)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonImportInfo : Lean.ToJson Lean.Lsp.ImportInfo
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableWithinAt.finsetProd`. -/
DifferentiableWithinAt.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) → DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i) s x
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instSMul : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} → {α : Type u_2} → [inst : SMul α ℝ] → [inst_1 : SMul α ℂ] → [IsScalarTower α ℝ ℂ] → SMul α (CuspForm Γ k)
-- Mathlib.Data.LawfulXor.Basic
isFixedPt_xor_right_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a b : α},
  Function.IsFixedPt (fun x => x ^^^ a) b ↔ a = 0
-- Mathlib.RingTheory.Polynomial.Dickson
/-- `dickson` is the `n`-th (generalised) Dickson polynomial of the `k`-th kind associated to the
element `a ∈ R`.  -/
Polynomial.dickson : {R : Type u_1} → [inst : CommRing R] → ℕ → R → ℕ → Polynomial R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Lean.DocString.Markdown
/-- Renders an action that produces an array of lines into a single Markdown string, appending any
accumulated footnotes after the main body.
 -/
Lean.Doc.MarkdownM.run' : Lean.Doc.MarkdownM (Array String) → Lean.CoreM String
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃)
  {Z : C} (h_1 : A₃ ⨿ B₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h)
        (CategoryTheory.CategoryStruct.comp g k))
      h_1
-- Mathlib.Order.Filter.Map
Filter.comap_neBot_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, (Filter.comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ Set.range m
-- Mathlib.Algebra.GroupWithZero.Action.TransferInstance
/-- Transfer `DistribMulAction` across an `Equiv`  -/
Equiv.distribMulAction : (M : Type u_1) →
  {A : Type u_3} →
    {B : Type u_4} →
      (e : A ≃ B) → [inst : Monoid M] → [inst_1 : AddMonoid B] → [DistribMulAction M B] → DistribMulAction M A
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_of_kernel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)],
  CategoryTheory.Limits.kernel.ι f = 0 → CategoryTheory.Mono f
-- Lean.Elab.DefView
Lean.Elab.DefKind.noConfusionType : Sort v✝ → Lean.Elab.DefKind → Lean.Elab.DefKind → Sort v✝
-- Aesop.Tree.Data
Aesop.Rapp.isSafe : Aesop.Rapp → Bool
-- Mathlib.Algebra.Ring.Identities
/-- Euler's four-square identity, see <https://en.wikipedia.org/wiki/Euler%27s_four-square_identity>.

This sign choice here corresponds to the signs obtained by multiplying two quaternions.
 -/
sum_four_sq_mul_sum_four_sq : ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R},
  (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2
-- Lean.Server.RequestCancellation
Lean.Server.CancellableT.checkCancelled : {m : Type → Type u_1} → [Monad m] → [MonadLiftT BaseIO m] → Lean.Server.CancellableT m Unit
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_1.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (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
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.add_div_le_sum_sq_div_card : ∀ {ι : Type u_2} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s t : Finset ι}
  {x : 𝕜},
  s ⊆ t →
    ∀ (f : ι → 𝕜) (d : 𝕜),
      0 ≤ x →
        x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card| →
          d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2 → d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleω₁δ a b c hab hbc).map φ).hom₂ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj c).map φ)
-- Mathlib.Data.Sym.Basic
Sym.attach_cons : ∀ {α : Type u_1} {n : ℕ} (x : α) (s : Sym α n), (x ::ₛ s).attach = ⟨x, ⋯⟩ ::ₛ Sym.map (fun x_1 => ⟨↑x_1, ⋯⟩) s.attach
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.ne_zero_of_injective : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} [Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂}, Function.Injective ⇑f → f ≠ 0
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams : Type
-- Mathlib.Data.Stream.Init
Stream'.tail_eq_drop : ∀ {α : Type u} (s : Stream' α), s.tail = Stream'.drop 1 s
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A set in a σ-finite space has positive measure if and only if its intersection with
some member of the countable family of finite measure spanning sets has positive measure.  -/
MeasureTheory.Measure.exists_measure_inter_spanningSets_pos : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
  (s : Set α), (∃ n, 0 < μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 0 < μ s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)}, k ∈ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size - 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul'.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M),
  p.smul' = { smul := fun c x => ⟨c • ↑x, ⋯⟩ }
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} (a : ENNReal), (a • μ).bind ⇑κ = a • μ.bind ⇑κ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rco : ∀ {m n fallback : ℤ} {i : ℕ}, (m...n).toList.getD i fallback = if i < (n - m).toNat then m + ↑i else fallback
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instLawfulHashable : LawfulHashable Std.Http.Header.Name
-- Mathlib.RingTheory.Bialgebra.Equiv
CoalgEquivClass.toCoalgEquiv.congr_simp : ∀ {F : Type u_5} {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B] [inst_8 : CoalgEquivClass F R A B] (f f_1 : F),
  f = f_1 → ↑f = ↑f_1
-- Mathlib.Data.Num.Basic
Num.instAdd : Add Num
-- Mathlib.Logic.Function.Iterate
/-- Iterate a function.  -/
Nat.iterate : {α : Sort u} → (α → α) → ℕ → α → α
-- Init.Data.UInt.Lemmas
UInt32.toUSize_eq_mod_4294967296_iff : ∀ (a : UInt32) (b : USize), a.toUSize = b % 4294967296 ↔ a = b.toUInt32
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ} (aig : Std.Sat.AIG α)
  (wn wr : ℕ) (q r : aig.RefVec w) (hle : old.decls.size ≤ aig.decls.size) (aig_1 : Std.Sat.AIG α) (wn_1 wr_1 : ℕ)
  (q_1 r_1 : aig_1.RefVec w) (hle_1 : old.decls.size ≤ aig_1.decls.size),
  ({ aig := aig, wn := wn, wr := wr, q := q, r := r, hle := hle } =
      { aig := aig_1, wn := wn_1, wr := wr_1, q := q_1, r := r_1, hle := hle_1 }) =
    (aig = aig_1 ∧ wn = wn_1 ∧ wr = wr_1 ∧ q ≍ q_1 ∧ r ≍ r_1)
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.iSup_adj : ∀ {ι : Sort u_1} {V : Type u_2} {a b : V} {f : ι → Digraph V}, (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b