mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.wittPolyProd.eq_1 : ∀ (p n : ℕ),
  WittVector.wittPolyProd p n =
    (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_lt_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) {c : NNReal},
  0 < c →
    autoParam (ContinuousOn f (spectrum 𝕜 a)) nnnorm_cfc_lt_iff._auto_1 →
      autoParam (p a) nnnorm_cfc_lt_iff._auto_3 → (‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π, ↑J
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, t.size ≤ (t.insertMany l).size
-- Init.Data.Range.Polymorphic.UInt
UInt32.succMany?_ofBitVec : ∀ {k : ℕ} {x : BitVec 32}, Std.PRange.succMany? k { toBitVec := x } = UInt32.ofBitVec <$> Std.PRange.succMany? k x
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_add_of_eq : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} {a b : R} {f g : Polynomial R},
  f.coeff n = a → g.coeff n = b → (f + g).coeff n = a + b
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a finite separable extension of exponential characteristic `q`, if `{ u_i }` is a
family of elements of `E` which is `F`-linearly independent, then `{ u_i ^ (q ^ n) }` is also
`F`-linearly independent for any natural number `n`. A special case of
`LinearIndependent.map_pow_expChar_pow_of_isSeparable`
and is an intermediate result used to prove it.  -/
_private.Mathlib.FieldTheory.PurelyInseparable.PerfectClosure.0.LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q n : ℕ) [hF : ExpChar F q]
  {ι : Type u_1} {v : ι → E} [FiniteDimensional F E] [Algebra.IsSeparable F E],
  LinearIndependent F v → LinearIndependent F fun x => v x ^ q ^ n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_2 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.mk.inj : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  {h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y}
  {h₀ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam}
  {h₁ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam}
  {rel :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
          (CategoryTheory.CategoryStruct.comp φ B.ι))
      SSet.RelativeMorphism.Homotopy.rel._autoParam}
  {h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y}
  {h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h_1 = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam}
  {h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h_1 = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam}
  {rel_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h_1 =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
          (CategoryTheory.CategoryStruct.comp φ B.ι))
      SSet.RelativeMorphism.Homotopy.rel._autoParam},
  { h := h, h₀ := h₀, h₁ := h₁, rel := rel } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1, rel := rel_1 } → h = h_1
-- Init.Data.Rat.Lemmas
Rat.ne_of_gt : ∀ {a b : ℚ}, a < b → b ≠ a
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (a : α) (s : Finset α) (t : α → Set β),
  ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.zero : ∀ (R : Type u_1) [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarAddMonoid R], IsStarProjection 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_mul_of_aestronglyMeasurable_right : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable g μ →
    MeasureTheory.Integrable (f * g) μ → MeasureTheory.Integrable f μ → μ[f * g | m] =ᵐ[μ] μ[f | m] * g
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instContinuousConstVAdd : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  ContinuousConstVAdd G (G ⧸ N)
-- Mathlib.Logic.Encodable.Basic
instEncodableULower : {α : Type u_1} → [inst : Encodable α] → Encodable (ULower α)
-- Mathlib.Data.Finset.Sups
Finset.infs_inter_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s₁ s₂ t : Finset α},
  (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Logic.Basic
xor_true : Xor True = Not
-- Mathlib.Data.Set.Card
Set.ncard_coe : ∀ {α : Type u_3} (s : Set α), Set.univ.ncard = s.ncard
-- Lean.Elab.Match
/-- Return true iff `e` is an explicit pattern variable provided by the user.  -/
Lean.Elab.Term.ToDepElimPattern.isExplicitPatternVar : Lean.Expr → Lean.Elab.Term.ToDepElimPattern.M Bool
-- Mathlib.Algebra.Ring.CharZero
neg_units_ne_self : ∀ {R : Type u_2} [inst : Ring R] [CharZero R] (u : Rˣ), -u ≠ u
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getKey? k (Std.Internal.List.insertEntry k v l) = some k
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.coe_trans_symm : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  ↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory CommGrpCat
-- Mathlib.RingTheory.Valuation.Basic
/-- An ordered monoid isomorphism `Γ₀ ≃ Γ'₀` induces an equivalence
`Valuation R Γ₀ ≃ Valuation R Γ'₀`.  -/
Valuation.congr : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
          [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] → (Γ₀ ≃*o Γ'₀) → Valuation R Γ₀ ≃ Valuation R Γ'₀
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.addMatcherInfo : Lean.Environment → Lean.Name → Lean.Meta.MatcherInfo → Lean.Environment
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listSum_map : ∀ {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ},
  (∀ x ∈ l, f x ≡ g x [MOD n]) → (List.map f l).sum ≡ (List.map g l).sum [MOD n]
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstSubInt : Lean.Expr → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.ematch : Lean.Meta.Grind.Origin → Lean.Expr → Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- If `f` splits with leading coeff `a` and degree `n`,
then `Res(f, g) = aⁿ * ∏ g(α)` where `α` runs through the roots of `f`.  -/
Polynomial.resultant_eq_prod_eval : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : Polynomial R) (n : ℕ),
  g.natDegree ≤ n →
    f.Splits →
      f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x => Polynomial.eval x g) f.roots).prod
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.nonOutput.injEq : ∀ (ticks ticks_1 : ℕ),
  (Lean.Server.FileWorker.Hover.RWState.nonOutput✝ ticks = Lean.Server.FileWorker.Hover.RWState.nonOutput✝ ticks_1) =
    (ticks = ticks_1)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_zero_lt_veblenWith_zero : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}},
  Order.IsNormal f → 0 < f 0 → (Ordinal.veblenWith f o₁ 0 < Ordinal.veblenWith f o₂ 0 ↔ o₁ < o₂)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_inv_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  (f : X ⟶ Y) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y g))
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The category of single and double intersections of the `U i` maps into the category
of open sets below some `U i`.
 -/
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      CategoryTheory.Functor (CategoryTheory.Pairwise ι) (TopCat.Presheaf.SheafCondition.OpensLeCover U)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.any_eq_true : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {p : (a : α) → β a → Bool},
  (↑m).WF → ((↑m).any p = true ↔ ∃ a, ∃ (h : m.contains a = true), p a (m.get a h) = true)
-- Std.Time.Format.Modifier
Std.Time.instReprDayPeriod : Repr Std.Time.DayPeriod
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
/-- The morphisms between the levels of the standard resolutions of `X` and `Y` induced by a
continuous group homomorphism `φ : H →ₜ* G` and a morphism `f : res φ X ⟶ Y`, given by
`F ↦ f ∘ F ∘ φ`.  -/
ContinuousCohomology.resolutionMap : {k : Type u} →
  {G H : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              [inst_5 : Group H] →
                [inst_6 : TopologicalSpace H] →
                  [inst_7 : IsTopologicalGroup H] →
                    {X : TopRep k G} →
                      {Y : TopRep k H} →
                        (φ : H →ₜ* G) →
                          (TopRep.res (↑φ) X ⟶ Y) → (i : ℕ) → TopRep.res (↑φ) (X.resolutionX i) ⟶ Y.resolutionX i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.union_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_ne_self_iff : ∀ {θ : Real.Angle}, -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `a` such that `a = 0` identifies to the identity functor.  -/
CategoryTheory.shiftFunctorZero' : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (a : A) → a = 0 → (CategoryTheory.shiftFunctor C a ≅ CategoryTheory.Functor.id C)
-- Std.Http.Data.URI.Basic
Std.Http.URI.Authority.mk.sizeOf_spec : ∀ (userInfo : Option Std.Http.URI.UserInfo) (host : Std.Http.URI.Host) (port : Std.Http.URI.Port),
  sizeOf { userInfo := userInfo, host := host, port := port } = 1 + sizeOf userInfo + sizeOf host + sizeOf port
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedCommGroup E],
  OrderDual.seminormedCommGroup =
    { toNorm := OrderDual.toNorm, toCommGroup := OrderDual.instCommGroup,
      toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g}
  (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Mono f], CategoryTheory.Mono c.inr
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.const : ∀ {c : ℝ}, Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed c
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.frequently_atBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α],
  (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b
-- Mathlib.ModelTheory.DirectLimit
/-- The universal property of the direct limit: maps from the components to another module
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.  -/
FirstOrder.Language.DirectLimit.lift : (L : FirstOrder.Language) →
  (ι : Type v) →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [inst_2 : IsDirectedOrder ι] →
              [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                [inst_4 : Nonempty ι] →
                  {P : Type u₁} →
                    [inst_5 : L.Structure P] →
                      (g : (i : ι) → L.Embedding (G i) P) →
                        (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                          L.Embedding (FirstOrder.Language.DirectLimit G f) P
-- Mathlib.RingTheory.Binomial
/-- A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
suitable factorials. We define this notion as a mixin for additive commutative monoids with natural
number powers, but retain the ring name. We introduce `Ring.multichoose` as the uniquely defined
quotient.  -/
BinomialRing : (R : Type u_1) → [AddCommMonoid R] → [Pow R ℕ] → Type u_1
-- Mathlib.Data.Finset.Sort
Finset.sort_val : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], s.val.sort r = s.sort r
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.Limits.IsCokernel.cokernelIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (l : Y ⟶ Z) {s : CategoryTheory.Limits.CokernelCofork f} (hs : CategoryTheory.Limits.IsColimit s)
  (i : s.pt ≅ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) i.hom = l),
  CategoryTheory.Limits.IsCokernel.cokernelIso f l hs i h = hs.ofIsoColimit (CategoryTheory.Limits.Cocone.ext i ⋯)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.EIO.mapTaskCostly : {α : Type u_1} → {ε β : Type} → (α → EIO ε β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask (Except ε β))
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoAt_midπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ),
  i + 1 ≤ n₀ + ↑q → QuasiIsoAt (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q) i
-- Mathlib.Analysis.Normed.Group.Quotient
/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
and `‖m‖ < ‖x‖ + ε`.  -/
QuotientGroup.exists_norm_mk_lt : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {ε : ℝ} (x : M ⧸ S),
  0 < ε → ∃ m, ↑m = x ∧ ‖m‖ < ‖x‖ + ε
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.sub_congr : ∀ {R : Type u_2} [inst : CommRing R] {a a' b b' c : R}, a = a' → b = b' → a' - b' = c → a - b = c
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp_i_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₂ A)),
  (ModuleCat.Hom.hom (groupHomology.shortComplexH2 B).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x) =
    (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap)
      ((Finsupp.lmapDomain (↑A) k (Prod.map ⇑f ⇑f))
        ((ModuleCat.Hom.hom (groupHomology.shortComplexH2 A).g).ker.subtype x))
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.modify.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α × RBTree.RBNode.Path α → Sort u_2) (snd : RBTree.RBNode.Path α)
  (h_1 : (snd : RBTree.RBNode.Path α) → motive (RBTree.RBNode.nil, snd))
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (x : α) → (b : RBTree.RBNode α) → (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a x b, path)),
  (match (RBTree.RBNode.nil, snd) with
    | (RBTree.RBNode.nil, snd) => h_1 snd
    | (RBTree.RBNode.node c a x b, path) => h_2 c a x b path) =
    h_1 snd
-- Mathlib.CategoryTheory.Limits.Cones
/-- To give an isomorphism between cocones, it suffices to give an
isomorphism between their vertices which commutes with the cone maps.  -/
CategoryTheory.Limits.Cocone.extInv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cocone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv)
                  CategoryTheory.Limits.Cocone.extInv._auto_1 →
                (c ≅ c')
-- Init.Data.List.Lemmas
List.mem_insert_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ List.insert a l
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousAt.div_const : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} [inst_3 : TopologicalSpace α] {a : α}, ContinuousAt f a → ∀ (y : G₀), ContinuousAt (fun x => f x / y) a
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → (t₁ ∩ t₂).WF
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_smul : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g : E → ℂ},
  Function.HasTemperateGrowth g →
    ∀ (c : ℂ), TemperedDistribution.smulLeftCLM F (c • g) = c • TemperedDistribution.smulLeftCLM F g
-- Mathlib.Topology.ContinuousMap.Polynomial
iccHomeoI.congr_simp : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b), iccHomeoI a b h = iccHomeoI a b h
-- Mathlib.Topology.Algebra.Group.Quotient
/-- The quotient of a topological group `G` by a closed subgroup `N` is T1.

When `G` is normal, this implies (because `G ⧸ N` is a topological group) that the quotient is T3
(see `QuotientGroup.instT3Space`).

Back to the general case, we will show later that the quotient is in fact T2
since `N` acts on `G` properly.  -/
QuotientGroup.instT1Space : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G}
  [hN : IsClosed ↑N], T1Space (G ⧸ N)
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.Config.mk : Bool → Mathlib.Tactic.Algebraize.Config
-- Batteries.Data.BinomialHeap.Lemmas
_private.Batteries.Data.BinomialHeap.Lemmas.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (h_1 : Unit → motive Batteries.BinomialHeap.Imp.Heap.nil)
  (h_2 :
    (rank : ℕ) →
      (val : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)),
  (match Batteries.BinomialHeap.Imp.Heap.nil with
    | Batteries.BinomialHeap.Imp.Heap.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.Heap.cons rank val c s => h_2 rank val c s) =
    h_1 ()
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given any `Finset` of objects `{X, ...}` and
indexed collection of `Finset`s of morphisms `{f, ...}` in `C`,
there exists an object `S`, with a morphism `T X : X ⟶ S` from each `X`,
such that the triangles commute: `f ≫ T Y = T X`, for `f : X ⟶ Y` in the `Finset`.
 -/
CategoryTheory.IsFiltered.sup_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))),
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp f (T mY) = T mX
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.epi_homMk : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U.left ⟶ V.left}
  [CategoryTheory.Epi f] (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom),
  CategoryTheory.Epi (CategoryTheory.Over.homMk f w)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.edist_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P),
  edist (e x) (e y) = edist x y
-- Mathlib.Algebra.Group.Prod
/-- Given additive magmas `A`, `B`, the natural projection homomorphism
from `A × B` to `A`  -/
AddHom.fst : (M : Type u_3) → (N : Type u_4) → [inst : Add M] → [inst_1 : Add N] → M × N →ₙ+ M
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity.0.«term_~ᵤ_» : Lean.TrailingParserDescr