mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {t : Finset α} {b : α},
  Finset.image (fun x => x * b) t = t.preimage (fun x => x * b⁻¹) ⋯
-- Std.Data.HashSet.Basic
/-- Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.HashSet.ofArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.HashSet α
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence between indexed sets of vertices v₁ and v₂.
Use `open scoped Congruent` to access the `v₁ ≅ v₂` notation.  -/
Congruent : {ι : Type u_1} →
  {P₁ : Type u_3} → {P₂ : Type u_4} → [PseudoEMetricSpace P₁] → [PseudoEMetricSpace P₂] → (ι → P₁) → (ι → P₂) → Prop
-- Init.Simproc
/-- Auxiliary attribute for simplification procedures.
 -/
Lean.Parser.Attr.simprocAttr : Lean.ParserDescr
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.erase : {γ : Type} →
  Lean.KeyedDeclsAttribute.ExtensionState γ →
    Lean.Name → Lean.Name → Lean.CoreM (Lean.KeyedDeclsAttribute.ExtensionState γ)
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed form of the inverse conjugation definition.  -/
CategoryTheory.unit_conjugateEquiv_symm : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : R₁ ⟶ R₂) (c : C),
  CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (α.app (L₁.obj c)) =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app c)
      (R₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app c))
-- Mathlib.GroupTheory.GroupAction.Jordan
Equiv.Perm.isPretransitive_of_isCycle_mem : ∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  g.IsCycle →
    g ∈ G →
      MulAction.IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(SubMulAction.ofFixingSubgroup (↥G) (↑g.support)ᶜ)
-- Mathlib.NumberTheory.MulChar.Basic
/-- The `n`th power of a quadratic character is itself, when `n` is odd.  -/
MulChar.IsQuadratic.pow_odd : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {χ : MulChar R R'},
  χ.IsQuadratic → ∀ {n : ℕ}, Odd n → χ ^ n = χ
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.eq_inf : @AlgebraicGeometry.IsFinite = @AlgebraicGeometry.IsIntegralHom ⊓ @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.Order.Hom.Bounded
TopHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ] (f : TopHom β γ)
  (g : TopHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_top' := ⋯ }
-- Mathlib.CategoryTheory.Elements
_private.Mathlib.CategoryTheory.Elements.0.CategoryTheory.NatTrans.mapElements.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor C (Type u_1)}
  (motive : F.Elements → Sort u_4) (X : C) (x : F.obj X) (h_1 : (X : C) → (x : F.obj X) → motive ⟨X, x⟩),
  (match ⟨X, x⟩ with
    | ⟨X, x⟩ => h_1 X x) =
    h_1 X x
-- Lean.Elab.DocString
/-- The internal state used by docstring elaboration  -/
Lean.Doc.InternalState : Type
-- Init.Data.SInt.Lemmas
Int32.lt_of_lt_of_le : ∀ {a b c : Int32}, a < b → b ≤ c → a < c
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.seq_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {l : Filter ι},
  TendstoUniformlyOn F f l s →
    ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sign_of_cycleType' : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α),
  Equiv.Perm.sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod
-- Mathlib.RingTheory.Localization.Basic
/-- If `x` in a `R' = S⁻¹ R`-module `M'`, then for a submodule `N'` of `M'`,
`s • x ∈ N'` if and only if `x ∈ N'` for some `s` in S.  -/
IsLocalization.smul_mem_iff : ∀ {R : Type u_4} [inst : CommSemiring R] {S : Submonoid R} {R' : Type u_5} [inst_1 : CommSemiring R']
  [inst_2 : Algebra R R'] [IsLocalization S R'] {M' : Type u_6} [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M']
  [inst_6 : Module R M'] [IsScalarTower R R' M'] {N' : Submodule R' M'} {x : M'} {s : ↥S}, s • x ∈ N' ↔ x ∈ N'
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.iInf_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {ι : Type u_2} (I : ι → TwoSidedIdeal R),
  (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_ite_eq : ∀ {G : Type u_7} [inst : CommGroup G] {A : Type u_8} [inst_1 : DecidableEq A] (l : List A) (f g : A → G) (a : A),
  (List.map (fun x => if x = a then f x else g x) l).prod = (f a / g a) ^ List.count a l * (List.map g l).prod
-- Std.Sync.Channel
Std.CloseableChannel.Error.closed.sizeOf_spec : sizeOf Std.CloseableChannel.Error.closed = 1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instAddCommGroup.eq_1 : ∀ (A : Type u_2) (E : Type u_6) [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E],
  ContinuousAddMonoidHom.instAddCommGroup A E =
    { toAddMonoid := inferInstance.toAddMonoid, neg := fun f => (ContinuousAddMonoidHom.neg E).comp f,
      sub := fun f g => { toAddMonoidHom := subAddMonoidHom, continuous_toFun := ⋯ }.comp (f.prod g), zsmul := zsmulRec,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯ }
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instSMulCommClass : ∀ (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [inst : SMul K V] [inst_1 : SMul K' V]
  [SMulCommClass K K' V], SMulCommClass K K' (WithLp p V)
-- Mathlib.Data.PNat.Basic
PNat.add_one : ∀ (a : ℕ+), a + 1 = (↑a).succPNat
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isPrime_span_singleton_of_prime : ∀ {α : Type u} [inst : CommSemiring α] {p : α}, Prime p → (Ideal.span {p}).IsPrime
-- Init.Data.Vector.Lemmas
Vector.lawfulBEq_iff : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [NeZero n], LawfulBEq (Vector α n) ↔ LawfulBEq α
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (X : B),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.id B).obj X = X
-- Mathlib.Topology.Path
Path.trans_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_4} [inst_1 : TopologicalSpace ι] {a b c : ι → X}
  (γ₁ : (t : ι) → Path (a t) (b t)),
  Continuous ↿γ₁ → ∀ (γ₂ : (t : ι) → Path (b t) (c t)), Continuous ↿γ₂ → Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
-- Mathlib.Data.List.Basic
List.filter_comm : ∀ {α : Type u} (p q : α → Bool) (l : List α), List.filter p (List.filter q l) = List.filter q (List.filter p l)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_emod : ∀ (a b n : ℤ), a * b % n = a % n * (b % n) % n
-- Mathlib.Topology.Homotopy.Product
/-- Composition and products commute.
This is `Path.trans_pi_eq_pi_trans` descended to path homotopy classes.  -/
Path.Homotopic.comp_pi_eq_pi_comp : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs cs : (i : ι) → X i}
  (γ₀ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) (γ₁ : (i : ι) → Path.Homotopic.Quotient (bs i) (cs i)),
  (Path.Homotopic.pi γ₀).trans (Path.Homotopic.pi γ₁) = Path.Homotopic.pi fun i => (γ₀ i).trans (γ₁ i)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_one_le : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → seminormFromConst' c f 1 ≤ 1
-- Init.Data.Vector.Find
Vector.isSome_findSome? : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → Option β},
  (Vector.findSome? f xs).isSome = xs.any fun x => (f x).isSome
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [inst_6 : Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ}
  {f : (out : β) → out ∈ it.toList → γ → m (ForInStep γ)},
  forIn' it.toList init f = forIn' it init fun out h acc => f out ⋯ acc
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerHemicontinuousWithinAt_iff_frequently`. -/
LowerHemicontinuousWithinAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  LowerHemicontinuousWithinAt f s x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
-- Mathlib.Data.FunLike.Graded
Graded.map_mem : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : FunLike F A B] [GradedFunLike F 𝒜 ℬ] (f : F) {i : ι} {x : A},
  x ∈ 𝒜 i → f x ∈ ℬ i
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_smul_eq_iff_minimalPeriod_dvd : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] {a : G} {b : α} {n : ℤ},
  a ^ n • b = b ↔ ↑(Function.minimalPeriod (fun x => a • x) b) ∣ n
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.contentRegular_exists_compact : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G),
  μ.ContentRegular →
    ∀ (K : TopologicalSpace.Compacts G) {ε : NNReal}, ε ≠ 0 → ∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_intro_l : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop) (x y : l),
  Lean.Order.PartialOrder.rel (Lean.Order.meet x (Lean.Order.CompleteLattice.ofProp p)) y =
    (p → Lean.Order.PartialOrder.rel x y)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {f : M → G} [ContMDiffInv₀ I n G] {a : M}, ContMDiffAt I' I n f a → f a ≠ 0 → ContMDiffAt I' I n (fun x => (f x)⁻¹) a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.pentagon : ∀ {B : Type u} [inst : Quiver B] {a b c d e : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d)
  (i : CategoryTheory.FreeBicategory.Hom d e),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_right i (CategoryTheory.FreeBicategory.Hom₂.associator f g h)).vcomp
      ((CategoryTheory.FreeBicategory.Hom₂.associator f (g.comp h) i).vcomp
        (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.associator g h i))))
    ((CategoryTheory.FreeBicategory.Hom₂.associator (f.comp g) h i).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.associator f g (h.comp i)))
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.map_ofFixingSubgroupUnion.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s t : Set α),
  SubMulAction.map_ofFixingSubgroupUnion M s t = { toFun := fun x => ⟨⟨↑x, ⋯⟩, ⋯⟩, map_smul' := ⋯ }
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.neg_modEq_neg`. -/
AddCommGroup.ModEq.of_neg : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, -a ≡ -b [PMOD p] → a ≡ b [PMOD p]
-- Mathlib.Order.Booleanisation
/-- The difference operator on `Booleanisation α` is as follows: For `a b : α`,
* `a \ b` is `a \ b`
* `a \ bᶜ` is `a ⊓ b`
* `aᶜ \ b` is `(a ⊔ b)ᶜ`
* `aᶜ \ bᶜ` is `b \ a`  -/
Booleanisation.instSDiff : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → SDiff (Booleanisation α)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.add_zero_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
  (h.add n 0).inv.app X = CategoryTheory.CategoryStruct.comp (h.zero.hom.app ((h.F n).obj X)) (CategoryTheory.eqToHom ⋯)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  Std.ExtDHashMap.Const.get! (m₁.union m₂) k = Std.ExtDHashMap.Const.getD m₂ k (Std.ExtDHashMap.Const.get! m₁ k)
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.mk.injEq : ∀ (array : ByteArray) (idx : ℕ) (array_1 : ByteArray) (idx_1 : ℕ),
  ({ array := array, idx := idx } = { array := array_1, idx := idx_1 }) = (array = array_1 ∧ idx = idx_1)
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that right-unbounded ranges \(i.e., for a bound `a`,
`a...*`, `a<...*` and `*...*`\) are always finite.
This is a prerequisite for many functions and instances, such as
`Rci.toList` or `ForIn'`.
 -/
Std.Rxi.IsAlwaysFinite : (α : Type u) → [Std.PRange.UpwardEnumerable α] → Prop
-- Mathlib.Computability.Encoding
/-- A decoding function from `List Bool` to `Bool`.  -/
Computability.decodeBool : List Bool → Bool
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
_private.Mathlib.GroupTheory.SpecificGroups.Cyclic.0.card_orderOf_eq_totient_aux₁ : ∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | a ^ n = 1}.card ≤ n) →
    ∀ {d : ℕ}, d ∣ Fintype.card α → 0 < {a | orderOf a = d}.card → {a | orderOf a = d}.card = d.totient
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.ker_quotient_lift : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {I : Ideal R} [inst_2 : I.IsTwoSided] (f : R →+* S)
  (H : I ≤ RingHom.ker f), RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)
-- Mathlib.Topology.Order
continuous_iSup_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β},
  Continuous f ↔ ∀ (i : ι), Continuous f
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isCompact_nnreal : ∀ {A : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] (a : A) [CompactSpace ↑(spectrum ℝ a)],
  IsCompact (spectrum NNReal a)
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.eq_singleton_of_mem : ∀ {α : Type u} {s : Set α}, s.Subsingleton → ∀ {x : α}, x ∈ s → s = {x}
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_zero_iff : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β] (f : F), ⇑f = 0 ↔ f = 0
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.Functor.Linear k (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given representations `A, B` and a type `α`, this is the natural representation isomorphism
`(α →₀ A) ⊗ B ≅ (A ⊗ B) →₀ α` sending `single x a ⊗ₜ b ↦ single x (a ⊗ₜ b)`.  -/
Rep.finsuppTensorLeft : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (A B : Rep.{u, u, v} k G) →
          (α : Type u) →
            [DecidableEq α] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.finsupp α A) B ≅
                Rep.finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Init.Data.SInt.Lemmas
ISize.toInt_toInt32 : ∀ (x : ISize), x.toInt32.toInt = x.toInt.bmod (2 ^ 32)
-- Mathlib.Analysis.Complex.Basic
Complex.instNormedAlgebraOfReal : {R : Type u_1} → [inst : NormedField R] → [NormedAlgebra R ℝ] → NormedAlgebra R ℂ
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- If all edge weights (given by a function on vertices) are positive, so is the path weight.  -/
Quiver.Path.weightOfEPs_pos : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {w : V → V → R}, (∀ (i j : V), 0 < w i j) → ∀ {i j : V} (p : Quiver.Path i j), 0 < Quiver.Path.weightOfEPs w p
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isZeroAt_iff_forall_SL2Z : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range →
    (c.IsZeroAt f k ↔
      ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
        (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c →
          UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k γ f))
-- Mathlib.Data.List.Basic
List.subset_singleton_iff : ∀ {α : Type u} {a : α} {L : List α}, L ⊆ [a] ↔ ∃ n, L = List.replicate n a
-- Mathlib.Algebra.Notation.Prod
Prod.instDiv : {G : Type u_8} → {H : Type u_9} → [Div G] → [Div H] → Div (G × H)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.analyticOnNhd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiff 𝕜 ⊤ f → AnalyticOnNhd 𝕜 f s
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier : CategoryTheory.HasForget₂ ProfiniteGrp.{u_1} GrpCat
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.destruct_congr : ∀ {α : Type u} {s t : Stream'.WSeq α},
  s ~ʷ t → Computation.LiftRel (Stream'.WSeq.BisimO fun x1 x2 => x1 ~ʷ x2) s.destruct t.destruct
-- Mathlib.Data.Int.Cast.Basic
Int.cast_one : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑1 = 1
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.𝔾ₘ_toPowerSeries : ∀ {R : Type u_1} [inst : CommRing R],
  FormalGroup.𝔾ₘ.toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1 + MvPowerSeries.X 0 * MvPowerSeries.X 1
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.eval_sub : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} (f : σ → R),
  (MvPolynomial.eval f) (p - q) = (MvPolynomial.eval f) p - (MvPolynomial.eval f) q
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.nonempty_support_optionEquivLeft : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] {f : MvPolynomial (Option σ) R},
  f ≠ 0 → ((MvPolynomial.optionEquivLeft R σ) f).support.Nonempty
-- Mathlib.CategoryTheory.Adjunction.Parametrized
/-- Alternative constructor for parametrized adjunctions, for which
the compatibility is stated in terms of `Adjunction.homEquiv`.  -/
CategoryTheory.ParametrizedAdjunction.mk' : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)) →
                  autoParam
                      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
                        ((adj X₁).homEquiv X₂ X₃) (CategoryTheory.CategoryStruct.comp ((F.map f).app X₂) g) =
                          CategoryTheory.CategoryStruct.comp (((adj Y₁).homEquiv X₂ X₃) g) ((G.map f.op).app X₃))
                      CategoryTheory.ParametrizedAdjunction.mk'._auto_1 →
                    (F ⊣₂ G)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
value `sin ((n + 1) * θ) / sin θ`.  -/
Polynomial.Chebyshev.U_complex_cos : ∀ (θ : ℂ) (n : ℤ),
  Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.U ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableVAdd₂ M X],
  Measurable f → Measurable g → Measurable (f +ᵥ g)
-- Mathlib.Logic.Basic
ite_ne_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, (if P then a else b) ≠ b ↔ P ∧ a ≠ b
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mk : {X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toPartialHomeomorph : PartialHomeomorph X Y) →
          IsOpen toPartialHomeomorph.source → IsOpen toPartialHomeomorph.target → OpenPartialHomeomorph X Y
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.mem_dualCoannihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {Φ : Submodule R (Module.Dual R M)} (x : M), x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0
-- Mathlib.Topology.DenseEmbedding
isClosed_property3 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → β → β → Prop},
  DenseRange e →
    IsClosed {q | p q.1 q.2.1 q.2.2} → (∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)) → ∀ (b₁ b₂ b₃ : β), p b₁ b₂ b₃
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_nonpos_iff : ∀ {x : ℝ}, Real.sinh x ≤ 0 ↔ x ≤ 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A product over `s.subtype p` equals one over `{x ∈ s | p x}`.  -/
Finset.prod_subtype_eq_prod_filter : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (f : ι → M) {p : ι → Prop}
  [inst_1 : DecidablePred p], ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.mulActionFiber_isPretransitive : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X),
  MulAction.IsPretransitive G ↑(f ⁻¹' {x})
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Standard formula, computing the Laplacian from the standard orthonormal basis of a real inner
product space.
 -/
InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F) {s : Set E} {e : E},
  UniqueDiffOn ℝ s →
    e ∈ s →
      InnerProductSpace.laplacianWithin f s e =
        ∑ i, (iteratedFDerivWithin ℝ 2 f s e) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]
-- Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Algebra.Transcendental.rank_eq_cardinalMk : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.Transcendental F E],
  Module.rank F E = Cardinal.mk E
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Context.mk.sizeOf_spec : ∀ (cfg : Mathlib.Tactic.DepRewrite.Config) (p x h : Lean.Expr) (Δ : Array (Lean.FVarId × Lean.Expr))
  (δ : Std.HashSet Lean.FVarId) (pHeadIdx : Lean.HeadIndex) (pNumArgs : ℕ),
  sizeOf { cfg := cfg, p := p, x := x, h := h, Δ := Δ, δ := δ, pHeadIdx := pHeadIdx, pNumArgs := pNumArgs } =
    1 + sizeOf cfg + sizeOf p + sizeOf x + sizeOf h + sizeOf Δ + sizeOf δ + sizeOf pHeadIdx + sizeOf pNumArgs