mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.addX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x₁ x₂ ℓ : R),
  W'.addX x₁ x₂ ℓ = ℓ ^ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : α → β},
  Measurable f → ∀ {s : Set β}, MeasurableSet s → (v.map f) s = v (f ⁻¹' s)
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.Location.wildcard.sizeOf_spec : sizeOf Lean.Elab.Tactic.Location.wildcard = 1
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_self_eq_zero_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s : Finset α}, s.addEnergy s = 0 ↔ s = ∅
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Two open partial homeomorphisms are equal when they have equal `toFun`, `invFun` and `source`.
It is not sufficient to have equal `toFun` and `source`, as this only determines `invFun` on
the target. This would only be true for a weaker notion of equality, arguably the right one,
called `EqOnSource`.  -/
OpenPartialHomeomorph.ext : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y),
  (∀ (x : X), ↑e x = ↑e' x) → (∀ (x : Y), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'
-- Init.Data.Array.Lemmas
Array.getElem?_push_size : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x)[xs.size]? = some x
-- Mathlib.Data.W.Constructions
WType.Listα.nil.sizeOf_spec : ∀ {γ : Type u} [inst : SizeOf γ], sizeOf WType.Listα.nil = 1
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.lt_of_natCast_lt_natCast : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℕ), ↑a < ↑b → a < b
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- **Alias** of `AddMonoidHom.finsetSum_apply`.

---

See also `Finset.sum_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N`  -/
AddMonoidHom.finset_sum_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : ι → M →+ N)
  (s : Finset ι) (b : M), (∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b
-- Init.Data.Array.Find
Array.find?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, Array.find? p #[a] = if p a = true then some a else none
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find?_decide_get_eq_find : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ i, p i),
  (Fin.find? fun x => decide (p x)).get ⋯ = Fin.find p h
-- Mathlib.Algebra.Category.Ring.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommSemiRingCat.Hom.Simps.hom : (R S : CommSemiRingCat) → R.Hom S → ↑R →+* ↑S
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β] (f : α ≃* β)
  (h : ∀ {a b : α}, f.toFun a ≤ f.toFun b ↔ a ≤ b), ⇑{ toMulEquiv := f, map_le_map_iff' := h } = ⇑f
-- Mathlib.RingTheory.Length
instFiniteDimensionalOrderSubmoduleOfIsArtinianOfIsNoetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M], FiniteDimensionalOrder (Submodule R M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.ofHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.AddMonObj A] [inst_3 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsAddMonHom f], CategoryTheory.AddMon.ofHom f = { hom := f, isAddMonHom_hom := inst_4 }
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenexImpRight.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 x_2 : L.BoundedFormula α x),
  x_1.toPrenexImpRight x_2 =
    match x, x_1, x_2 with
    | n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum =>
      ((FirstOrder.Language.BoundedFormula.liftAt 1 n φ).toPrenexImpRight ψ).ex
    | n, φ, ψ.all => ((FirstOrder.Language.BoundedFormula.liftAt 1 n φ).toPrenexImpRight ψ).all
    | _n, φ, ψ => φ.imp ψ
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- The `SlashInvariantForm` corresponding to `Function.const _ x`.  -/
SlashInvariantForm.const : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetOne] → ℂ → SlashInvariantForm Γ 0
-- Mathlib.Order.Minimal
Set.minimal_iff_forall_ssubset : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, t ⊂ s → ¬P t
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.pow_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f i) → MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn (f ^ n) g s
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_nnreal_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : NNReal), c ≠ 0 → MeasureTheory.llr μ (c • ν) =ᵐ[μ] fun x => MeasureTheory.llr μ ν x - Real.log ↑c
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.existsInv.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.existsInv = 1
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_mem_Ico' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (b : α), toIcoMod hp 0 b ∈ Set.Ico 0 p
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {n : ℕ} {var : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17} {n_1 : ℕ}
  {var_1 : Lean.FVarId} {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17},
  Lean.Compiler.LCNF.LetValue.reset n var h = Lean.Compiler.LCNF.LetValue.reset n_1 var_1 h_1 → n = n_1 ∧ var = var_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.pop k f q with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_3 k f q
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.collectDependencies : Lean.Meta.Match.MkMatcherInput → Lean.MetaM Lean.FVarIdSet
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.inter : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α}, MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ ∩ s₂)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.valuesArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.valuesArray = t₂.valuesArray
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
/-- To check that `f` is zero at `c`, it suffices for `f ∣[k] g` to be zero at `∞` for any
single `g` with `g • ∞ = c`.  -/
OnePoint.isZeroAt_iff : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ},
  g • OnePoint.infty = c → (c.IsZeroAt f k ↔ UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k g f))
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r_pos : ∀ (z : UpperHalfPlane), 0 < EisensteinSeries.r z
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- If `j` is initial in the index category, then the map `limit.π F j` is an isomorphism.
 -/
CategoryTheory.Limits.isIso_π_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasLimit F], CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_map_image_iff : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} {f : α ↪ β},
  (SimpleGraph.map (⇑f) G).IsClique (⇑f '' s) ↔ G.IsClique s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β),
  Std.Internal.List.getValueD a l fallback = (Std.Internal.List.getValue? a l).getD fallback
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteGrp.Hom.mk.inj : ∀ {A B : ProfiniteGrp.{u}} {hom' hom'_1 : ↑A.toProfinite.toTop →ₜ* ↑B.toProfinite.toTop},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_iff_injective_get_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsPath ↔ Function.Injective fun x => p.support.get x
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_target_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M},
  MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
        (↑(extChartAt I x) x)
-- Mathlib.Algebra.Module.LinearMap.DivisionRing
/-- **Alias** of the reverse direction of `LinearMap.surjective_iff_ne_zero`. -/
LinearMap.surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : DivisionSemiring R] [inst_2 : Module R M]
  {f : M →ₗ[R] R}, f ≠ 0 → Function.Surjective ⇑f
-- Batteries.Data.AssocList
Batteries.AssocList.toList_mapVal : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) (l : Batteries.AssocList α β),
  (Batteries.AssocList.mapVal f l).toList =
    List.map
      (fun x =>
        match x with
        | (a, b) => (a, f a b))
      l.toList
-- Mathlib.Computability.Reduce
manyOneEquiv_up : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, ManyOneEquiv (p ∘ ULower.up) p
-- Mathlib.Algebra.Category.Grp.Limits
/-- A functor `F : J ⥤ AddGrpCat.{u}` has a limit iff
`(F ⋙ forget AddGrpCat).sections` is `u`-small.  -/
AddGrpCat.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, (Std.ExtDHashMap.Const.modify m k f).size = m.size
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- The underlying family of points.

Do NOT use directly. Use the coercion instead.  -/
AffineBasis.toFun : {ι : Type u₁} →
  {k : Type u₂} →
    {V : Type u₃} →
      {P : Type u₄} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → ι → P
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_setWidth : ∀ {n : ℕ} (m : ℕ) (x : BitVec n) (i : ℕ), (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Makes the identity isomorphism from a proof two subfields of a multiplicative
monoid are equal.  -/
RingEquiv.subfieldCongr : {K : Type u} → [inst : DivisionRing K] → {s t : Subfield K} → s = t → ↥s ≃+* ↥t
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.instZero : {R : Type u_1} → [inst : NonUnitalRing R] → Zero (RingSeminorm R)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprTransferEncoding.repr : Std.Http.Header.TransferEncoding → ℕ → Std.Format
-- Mathlib.Data.Nat.Factorization.Defs
/-- We introduce the notations `ordProj[p] n` for the largest power of the prime `p` that
divides `n` and `ordCompl[p] n` for the complementary part. The `ord` naming comes from
the $p$-adic order/valuation of a number, and `proj` and `compl` are for the projection and
complementary projection. The term `n.factorization p` is the $p$-adic order itself.
For example, `ordProj[2] n` is the even part of `n` and `ordCompl[2] n` is the odd part.  -/
Nat.«termOrdCompl[_]_» : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.compare_comp_eq_compare : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α)
  (γ : Type uγ) [inst_1 : TopologicalSpace γ] [T3Space γ] {f : α → γ},
  Continuous f →
    (∀ (a : pkg.space), Filter.Tendsto f (Filter.comap pkg.coe (nhds a)) (nhds (⋯.extend f a))) →
      ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
-- Mathlib.CategoryTheory.EffectiveEpi.Extensive
CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.FinitaryPreExtensive D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts F] [F.PreservesEffectiveEpis],
  F.PreservesFiniteEffectiveEpiFamilies
-- Mathlib.Control.Bifunctor
Bifunctor.id_fst : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β),
  Bifunctor.fst id x = x
-- Mathlib.Topology.Order.LiminfLimsup
/-- An antitone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsInf` to the `Filter.limsup` of the image if the function is continuous at the `limsInf`
(and the filter is bounded from below and frequently bounded from above).  -/
Antitone.map_limsInf_of_continuousAt : ∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [OrderTopology S]
  {F : Filter R} [F.NeBot] {f : R → S},
  Antitone f →
    ContinuousAt f F.limsInf →
      autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) F) Antitone.map_limsInf_of_continuousAt._auto_1 →
        autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) F) Antitone.map_limsInf_of_continuousAt._auto_3 →
          f F.limsInf = Filter.limsup f F
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.maxValueSealed.eq_1 : ISize.maxValueSealed✝ = ISize.maxValue
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.SpecialLinearGroup.toPGL_ker : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Matrix.SpecialLinearGroup.toPGL.ker = Subgroup.center (Matrix.SpecialLinearGroup n R)
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.mk.injEq : ∀ {T : Type u_2} (finset : Finset T) (point : T) (radius : ℕ) (finset_1 : Finset T) (point_1 : T) (radius_1 : ℕ),
  ({ finset := finset, point := point, radius := radius } =
      { finset := finset_1, point := point_1, radius := radius_1 }) =
    (finset = finset_1 ∧ point = point_1 ∧ radius = radius_1)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasTwoOutOfThreeProperty], W.IsStableUnderComposition
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Render one section of rewrite results.  -/
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.renderRewrites.renderSection : Lean.Lsp.Range →
  Lean.Server.FileWorker.EditableDocument →
    Bool →
      Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind →
        Lean.MetaM (Option ProofWidgets.Html)
-- Aesop.Tree.Traversal
Aesop.TreeRef.mvarCluster : Aesop.MVarClusterRef → Aesop.TreeRef
-- Mathlib.Data.List.Nodup
List.nodup_iff_injective_getElem : ∀ {α : Type u} {l : List α}, l.Nodup ↔ Function.Injective fun i => l[↑i]
-- Init.Data.SInt.Lemmas
ISize.neg_mul_neg : ∀ (a b : ISize), -a * -b = a * b
-- Mathlib.Algebra.Group.Hom.Defs
IsDedekindFiniteAddMonoid.of_injective : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F),
  Function.Injective ⇑f → ∀ [IsDedekindFiniteAddMonoid N], IsDedekindFiniteAddMonoid M
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_mul : ∀ {p q : ℝ}, 0 ≤ p → (p * q).toNNReal = p.toNNReal * q.toNNReal
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsProper
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.mul : ∀ {R : Type u_1} [inst : CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R},
  p.IsPrimitive → q.IsPrimitive → (p * q).IsPrimitive
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutex.mk.inj : ∀ {α : Type} {ref : IO.Ref α} {mutex : Std.BaseSharedMutex} {ref_1 : IO.Ref α} {mutex_1 : Std.BaseSharedMutex},
  { ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 } → ref = ref_1 ∧ mutex = mutex_1
-- Mathlib.Data.Multiset.Defs
Multiset.quot_mk_to_coe' : ∀ {α : Type u_1} (l : List α), Quot.mk (fun x1 x2 => x1 ≈ x2) l = ↑l
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {T : CategoryTheory.Monad C} {c c' : CategoryTheory.Kleisli T}
  {x y : c.Hom c'}, x.of = y.of → x = y
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- The identity `1` is the rotation by `0`.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.one : {n : ℕ} → DihedralGroup n
-- Mathlib.Control.Traversable.Equiv
/-- If the `Traversable t'` instance has the properties that `map`,
`map_const`, and `traverse` are equal to the ones that come from
carrying the traversable functor structure from `t` over the
equivalences, then the fact that `t` is a lawful traversable functor
carries over as well.  -/
Equiv.isLawfulTraversable' : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t]
  [inst_2 : Traversable t'],
  (∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f) →
    (∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f) →
      (∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
          traverse f = Equiv.traverse eqv f) →
        LawfulTraversable t'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_add_int_mul_two_pi : ∀ (x : ℂ) (n : ℤ), Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryGT? k = t₂.getEntryGT? k
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : MulZeroOneClass α]
  [inst_1 : MulZeroOneClass β] [inst_2 : FunLike F α β] [toMonoidHomClass : MonoidHomClass F α β]
  [toZeroHomClass : ZeroHomClass F α β], MonoidWithZeroHomClass F α β
-- Mathlib.NumberTheory.SelbergSieve
/-- The remainder term in the approximation A_d = ν (d) X + R_d. This is the degree to which `nu`
fails to approximate the proportion of the weight that is a multiple of `d`.  -/
BoundingSieve.rem : {s : BoundingSieve} → ℕ → ℝ
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_comp_equiv : ∀ {α : Type u_2} {m : Type u_5} {n : Type u_6} [inst : DecidableEq n] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (σ : n ≃ m) (i : m) (x : α), Pi.single i x ∘ ⇑σ = Pi.single (σ.symm i) x
-- Mathlib.Geometry.Manifold.Instances.Sphere
mfderiv_coe_sphere_injective : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), Function.Injective ⇑(mfderiv% Subtype.val v)
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.dvd : ∀ {n m : ℕ}, IsPrimePow n → m ∣ n → m ≠ 1 → IsPrimePow m
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_sub_right : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i) (f j - f k) μ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rci.isEmpty.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (x : Std.Rci α), x.isEmpty = false
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instIsScalarTower_2 : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {P : Type u_5} [inst_3 : SMul P R] [inst_4 : SMul P T] [inst_5 : SMul R T]
  [IsScalarTower P R T], IsScalarTower P (WithAbs v) T
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4StarOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C],
  (∀ (α : Type w), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C) →
    CategoryTheory.AB4StarOfSize.{w, v, u} C
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_lt_one_eq_self_of_isOpen : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → IsOpen s → {x | gauge s x < 1} = s
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_natCast : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ] [inst_3 : Module R S]
  (x : S) (n : ℕ), (↑n).smeval x = n • x ^ 0
-- Mathlib.Order.Preorder.Finite
Finset.exists_maximal : ∀ {α : Type u_2} [inst : LE α] [IsTrans α LE.le] {s : Finset α}, s.Nonempty → ∃ i, Maximal (fun x => x ∈ s) i