mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'_inv_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv
      (CategoryTheory.CategoryStruct.comp (K.homologyι j) h) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι
      (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h)
-- Init.Data.SInt.Lemmas
Int16.div_zero : ∀ {a : Int16}, a / 0 = 0
-- Mathlib.Algebra.Order.Module.Pointwise
bddBelow_smul_iff_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  {s : Set β} {a : α}, a < 0 → (BddBelow (a • s) ↔ BddAbove s)
-- Init.Data.List.Nat.TakeDrop
List.getLast_drop : ∀ {α : Type u_1} {i : ℕ} {l : List α} (h : List.drop i l ≠ []), (List.drop i l).getLast h = l.getLast ⋯
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.mul_ι_mul_ι_of_isOrtho : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q) {a b : M},
  QuadraticMap.IsOrtho Q a b →
    x * (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -(x * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.fun_prop_of_mem_aeSeqSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α},
  x ∈ aeSeqSet hf p → p x fun n => f n x
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousOn.zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f s → ∀ (z : ℤ), ContinuousOn (z • f) s
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_left_inj : ∀ {a b d : ℤ}, d ∣ a → d ∣ b → (a / d = b / d ↔ a = b)
-- Mathlib.Analysis.Normed.Module.Basic
eventually_nhds_norm_smul_sub_lt : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (c : 𝕜) (x : E) {ε : ℝ}, 0 < ε → ∀ᶠ (y : E) in nhds x, ‖c • (y - x)‖ < ε
-- Mathlib.Algebra.Ring.BooleanRing
Bool.add_eq_xor : ∀ (b c : Bool), b + c = (b ^^ c)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.midpoint_mem_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), midpoint ℝ p₁ p₂ ∈ AffineSubspace.perpBisector p₁ p₂
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.changeOrigin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x y : E},
  HasFiniteFPowerSeriesOnBall f p x n r →
    ↑‖y‖₊ < r → HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ↑‖y‖₊)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSemilatticeInfOpenNormalAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (OpenNormalAddSubgroup G)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_iff_mem_essImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) (F : CategoryTheory.Sheaf J D),
  CategoryTheory.Sheaf.IsConstant J F ↔ L.essImage F
-- Mathlib.Data.Vector.Basic
/-- The `toList` of a `Vector` after a `scanl` is the `List.scanl`
of the `toList` of the original `Vector`.
 -/
List.Vector.toList_scanl : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n),
  (List.Vector.scanl f b v).toList = List.scanl f b v.toList
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.toLieHom_comp : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {B : Type w} {C : Type w₁}
  [inst_3 : Ring B] [inst_4 : Ring C] [inst_5 : Algebra R B] [inst_6 : Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C),
  (g.comp f).toLieHom = g.toLieHom.comp f.toLieHom
-- Mathlib.Logic.ExistsUnique
existsUnique_iff_exists : ∀ {α : Sort u_1} [Subsingleton α] {p : α → Prop}, (∃! x, p x) ↔ ∃ x, p x
-- Mathlib.Analysis.Polynomial.Order
Polynomial.eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos : ∀ {P : Polynomial ℝ} {x : ℝ}, (∀ (y : ℝ), P.IsRoot y → y < x) → P.leadingCoeff ≤ 0 → Polynomial.eval x P < 0
-- Mathlib.CategoryTheory.Functor.Flat
/-- If `F : C ⥤ D` is a representably flat functor between small categories, then the functor
`Lan F.op` that takes presheaves over `C` to presheaves over `D` preserves finite limits.
 -/
CategoryTheory.lan_preservesFiniteLimits_of_flat : ∀ {C D : Type u₁} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D] (E : Type u₂)
  [inst_2 : CategoryTheory.Category.{u₁, u₂} E] {FE : E → E → Type u_1} {CE : E → Type u₁}
  [inst_3 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [inst_4 : CategoryTheory.ConcreteCategory E FE]
  [CategoryTheory.Limits.HasLimits E] [inst_6 : CategoryTheory.Limits.HasColimits E]
  [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] (F : CategoryTheory.Functor C D)
  [CategoryTheory.RepresentablyFlat F], CategoryTheory.Limits.PreservesFiniteLimits F.op.lan
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instRepr : {rel : ℤ → ℤ → Prop} → {m n : ℤ} → Repr (Std.Time.Internal.Bounded rel m n)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The modified `n`-th cyclotomic polynomial with coefficients in `R`, it is the usual cyclotomic
polynomial if there is a primitive `n`-th root of unity in `R`.  -/
Polynomial.cyclotomic' : ℕ → (R : Type u_2) → [inst : CommRing R] → [IsDomain R] → Polynomial R
-- Mathlib.Topology.Constructions
continuous_codRestrict_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y}
  (hs : ∀ (a : X), f a ∈ s), Continuous (Set.codRestrict f s hs) ↔ Continuous f
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.eq_of_lt_of_lt : ∀ {m a b : ℕ}, a ≡ b [MOD m] → a < m → b < m → a = b
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of the linear map associated to a matrix is the linear map associated to the
conjugate transpose of that matrix.  -/
Matrix.toEuclideanLin_conjTranspose_eq_adjoint : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {m : Type u_5} {n : Type u_6} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (A : Matrix m n 𝕜),
  Matrix.toEuclideanLin A.conjTranspose = LinearMap.adjoint (Matrix.toEuclideanLin A)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.target : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {m : ℕ} → aig.ArbitraryShiftTarget m → aig.RefVec m
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.map_ι_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape}
  {d : CategoryTheory.Limits.MultispanIndex J C} (c : CategoryTheory.Limits.Multicofork d)
  (F : CategoryTheory.Functor C D) (x : CategoryTheory.Limits.WalkingMultispan J),
  (c.map F).ι.app x =
    match x with
    | CategoryTheory.Limits.WalkingMultispan.left a =>
      CategoryTheory.CategoryStruct.comp (F.map (d.fst a)) (F.map (c.π (J.fst a)))
    | CategoryTheory.Limits.WalkingMultispan.right a => F.map (c.π a)
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
/-- If `α` is a type, and `R` is a semiring, then `FreeNonUnitalNonAssocAlgebra R α` is the free
non-unital non-associative `R`-algebra generated by `α`.
This is an `R`-algebra equipped with a function
`FreeNonUnitalNonAssocAlgebra.of R : α → FreeNonUnitalNonAssocAlgebra R α` which has
the following universal property: if `A` is any `R`-algebra, and `f : α → A` is any function,
then this function is the composite of `FreeNonUnitalNonAssocAlgebra.of R`
and a unique non-unital `R`-algebra homomorphism
`FreeNonUnitalNonAssocAlgebra.lift R f : FreeNonUnitalNonAssocAlgebra R α →ₙₐ[R] A`.

A typical element of `FreeNonUnitalNonAssocAlgebra R α` is an `R`-linear combination of
nonempty formal (non-commutative, non-associative) products of elements of `α`.
For example if `x` and `y` are terms of type `α` and
`a`, `b` are terms of type `R` then `(3 * a * a) • (x * (y * x)) + (2 * b + 1) • (y * x)` is a
"typical" element of `FreeNonUnitalNonAssocAlgebra R α`.
 -/
FreeNonUnitalNonAssocAlgebra : (R : Type u_1) → Type u_2 → [Semiring R] → Type (max u_1 u_2)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mk.injEq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarRing A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A] (toSubalgebra : Subalgebra R A)
  (star_mem' : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier) (toSubalgebra_1 : Subalgebra R A)
  (star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra_1.carrier → star a ∈ toSubalgebra_1.carrier),
  ({ toSubalgebra := toSubalgebra, star_mem' := star_mem' } =
      { toSubalgebra := toSubalgebra_1, star_mem' := star_mem'_1 }) =
    (toSubalgebra = toSubalgebra_1)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The distance on the disjoint union indeed defines a metric space. All the distance properties
follow from our choice of the distance. The harder work is to show that the uniform structure
defined by the distance coincides with the disjoint union uniform structure.  -/
Metric.metricSpaceSum : {X : Type u} → {Y : Type v} → [MetricSpace X] → [MetricSpace Y] → MetricSpace (X ⊕ Y)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_comap_singleton_of_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsIntegral → ∀ (x : PrimeSpectrum S), IsClosed {x} → IsClosed {PrimeSpectrum.comap f x}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGet!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.get! t₁ k = Std.DTreeMap.Raw.Const.get! t₂ k
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.offsetOfPosAux.eq_def : ∀ (s : String) (pos i : String.Pos.Raw) (offset : ℕ),
  String.Pos.Raw.offsetOfPosAux s pos i offset =
    if i ≥ pos then offset
    else
      if h : String.Pos.Raw.atEnd s i = true then offset
      else
        have this := ⋯;
        String.Pos.Raw.offsetOfPosAux s pos (String.Pos.Raw.next s i) (offset + 1)
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_empty : ∀ {α : Type u_1} {β : Type u_2} {u v : α}, Graph.banana u v ∅ = Graph.noEdge {u, v} β
-- Mathlib.Order.RelClasses
/-- **Alias** of `Std.Refl.swap`. -/
IsRefl.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Refl r], Std.Refl (Function.swap r)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.toParam : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Bool → Lean.Compiler.LCNF.Param pu
-- Mathlib.Data.Set.Function
Set.RightInvOn.congr_left : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {f₁' f₂' : β → α},
  Set.RightInvOn f₁' f t → Set.EqOn f₁' f₂' t → Set.RightInvOn f₂' f t
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_leftInverse : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic),
  Function.LeftInverse ⇑(AdjoinRoot.mk g) ⇑(AdjoinRoot.modByMonicHom hg)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.compl_sup : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] (s : Finset ι) (f : ι → α), (s.sup f)ᶜ = s.inf fun i => (f i)ᶜ
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.range_sdiff_image`.

---

Alias of `Set.image_compl_eq_range_sdiff_image`.  -/
Set.range_diff_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), Set.range f \ f '' s = f '' sᶜ
-- Mathlib.MeasureTheory.Measure.AddContent
/-- **Alias** of `MeasureTheory.le_addContent_sdiff`. -/
MeasureTheory.le_addContent_diff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (m : MeasureTheory.AddContent ENNReal C),
  MeasureTheory.IsSetRing C → s ∈ C → t ∈ C → m s - m t ≤ m (s \ t)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- If the characteristic functions `charFun` of two finite measures `μ` and `ν` on
a complete second-countable inner product space coincide, then `μ = ν`.  -/
MeasureTheory.Measure.ext_of_charFun : ∀ {E : Type u_3} [inst : MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.charFun μ = MeasureTheory.charFun ν → μ = ν
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Limits.IsZero S.L₃.X₂ → CategoryTheory.Epi S.δ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Given a functor `F` and a collection of limit cones for each diagram `X ↦ F X k`, we can stitch
them together to give a cone for the diagram `F`.
`combinedIsLimit` shows that the new cone is limiting, and `evalCombined` shows it is
(essentially) made up of the original cones.
 -/
CategoryTheory.Limits.combineCones : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              ((k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) → CategoryTheory.Limits.Cone F
-- Mathlib.Probability.StrongLaw
/-- `Xᵢ` satisfies the strong law of large numbers along all integers. This follows from the
corresponding fact along the sequences `c^n`, and the fact that any integer can be sandwiched
between `c^n` and `c^(n+1)` with comparably small error if `c` is close enough to `1`
(which is formalized in `tendsto_div_of_monotone_of_tendsto_div_floor_pow`).  -/
ProbabilityTheory.strong_law_aux7 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ᵐ (ω : Ω),
            Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (a : Ω), X 0 a))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Eta rule for structured arrows.  -/
CategoryTheory.StructuredArrow.eta : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            (f : CategoryTheory.StructuredArrow S T) → f ≅ CategoryTheory.StructuredArrow.mk f.hom
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitMono f},
  x = y ↔ x.retraction = y.retraction
-- Init.Data.BitVec.Lemmas
BitVec.toFin_neg : ∀ {n : ℕ} (x : BitVec n), (-x).toFin = Fin.ofNat (2 ^ n) (2 ^ n - x.toNat)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0)
  (hg : CategoryTheory.CategoryStruct.comp g (K.d q q') = 0),
  CochainComplex.HomComplex.Cocycle.fromSingleMk (f - g) h q' hq' ⋯ =
    CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf -
      CochainComplex.HomComplex.Cocycle.fromSingleMk g h q' hq' hg
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.weightSpace.eq_1 : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (χ : L → R),
  LieModule.weightSpace M χ = { toSubmodule := ⨅ x, ((LieModule.toEnd R L M) x).eigenspace (χ x), lie_mem := ⋯ }
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_nsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddGroup α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (x - n • c) = (-1) ^ n • f x
-- Mathlib.Data.Set.Image
Set.preimage_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univ
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_closure_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {x : R},
  x ∈ NonUnitalSubring.closure s ↔ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- `⊤`, coerced to a set, is the whole set of points.  -/
AffineSubspace.top_coe : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], ↑⊤ = Set.univ
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformlyOn f g s → IsCompact s → HasProdUniformlyOn f g s
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ),
  ↑(v.valuationOfNeZeroToFun x) = (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x
-- Std.Http.Protocol.H1
/-- Converts raw parsed header name/value strings into typed header representations.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.typedHeader? : String → String → Option (Std.Http.Header.Name × Std.Http.Header.Value)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : τ → S) (h : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
  (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₁ h) φ) =
    (MvPolynomial.eval₂Hom f fun i => (MvPolynomial.eval₂Hom f g) (h i)) φ
-- Lean.OriginalConstKind
_private.Lean.OriginalConstKind.0.Lean.privateConstKindsExt : Lean.MapDeclarationExtension Lean.ConstantKind
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_ciSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ᶠ (y : α) in nhdsWithin x s, BddAbove (Set.range fun i => f i y)) →
    (∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
-- Std.Data.DTreeMap.Iterator
Std.DTreeMap.keysIter_toList : ∀ {α : Type u_1} {β : α → Type u_1} {cmp : α → α → Ordering} (m : Std.DTreeMap α β cmp), m.keysIter.toList = m.keys
-- Mathlib.Order.Max
IsTop.lt_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsTop a → b ≠ a → b < a
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.smul_mem_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {a : G₀}, a ≠ 0 → ∀ (S : Subgroup G) (x : G), a • x ∈ a • S ↔ x ∈ S
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ker.eq_1 : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), f.ker = f.toAddMonoidHom.ker
-- Init.Data.Int.Bitwise.Basic
/-- Bitwise left shift, usually accessed via the `<<<` operator.

Examples:
* `1 <<< 2 = 4`
* `1 <<< 3 = 8`
* `0 <<< 3 = 0`
* `0xf1 <<< 4 = 0xf10`
* `(-1) <<< 3 = -8`
 -/
Int.shiftLeft : ℤ → ℕ → ℤ
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimit_inv_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x : (j : J) × ↑(F.obj j)),
  (GrpCat.FilteredColimits.G.mk F x)⁻¹ = GrpCat.FilteredColimits.G.mk F ⟨x.fst, x.snd⁻¹⟩
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.mk : {α : Type} → IO.Promise Bool → Option (Std.Async.Waiter (Option α)) → Std.Broadcast.Consumer✝ α
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `B` is an `n`-th cyclotomic extension of `A`, then `zeta n A B` is a primitive root of
unity in `B`.  -/
IsCyclotomicExtension.zeta : (n : ℕ) →
  [NeZero n] →
    (A : Type w) →
      (B : Type z) →
        [inst : CommRing A] → [inst_1 : CommRing B] → [inst_2 : Algebra A B] → [IsCyclotomicExtension {n} A B] → B
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌈(b - v) / r⌉ - ⌈(a - v) / r⌉` numbers congruent to `v` mod `r` in `[a, b)`,
if `a ≤ b`. `Nat` version of `Int.Ico_filter_modEq_card`.  -/
Nat.Ico_filter_modEq_card : ∀ (a b : ℕ) {r : ℕ},
  0 < r → ∀ (v : ℕ), ↑{x ∈ Finset.Ico a b | x ≡ v [MOD r]}.card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Degeneracy maps for a simplicial object.  -/
CategoryTheory.SimplicialObject.σ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := n + 1 }))
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mono_measure' : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ ν : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X],
  MeasureTheory.LocallyIntegrableOn f s μ → ν.restrict s ≤ μ.restrict s → MeasureTheory.LocallyIntegrableOn f s ν
-- Mathlib.Data.W.Basic
WType.depth_pos : ∀ {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] (t : WType β), 0 < t.depth
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Return the user-facing name of the premise, relative to the current namespace.  -/
Mathlib.Tactic.ClickSuggestions.Premise.unresolveName : Mathlib.Tactic.ClickSuggestions.Premise → Lean.MetaM Lean.Name