mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_const_smul_right`. -/
Asymptotics.IsTheta.const_smul_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
  c ≠ 0 → f =Θ[l] g' → f =Θ[l] fun x => c • g' x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φQ = f
-- Mathlib.Data.Analysis.Topology
instInhabitedRealizer : {α : Type u_1} → {σ : Type u_3} → (F : Ctop α σ) → Inhabited (Ctop.Realizer α)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `zero_apply`. -/
SchwartzMap.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_injective : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid P]
  [inst_3 : Module R M] [inst_4 : Module R P] (f : M →ₗ[R] P),
  Function.Injective ⇑f → ∀ [IsArtinian R P], IsArtinian R M
-- Mathlib.Topology.Algebra.Order.Field
inv_atTop₀ : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.atTop⁻¹ = nhdsWithin 0 (Set.Ioi 0)
-- Init.Control.Lawful.Basic
Id.run_map : ∀ {α β : Type u_1} (x : Id α) (f : α → β), (f <$> x).run = f x.run
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv : {α : Type u_2} → {β : Type u_3} → [SDiv α β] → SDiv (Set α) (Set β)
-- Mathlib.Order.Interval.Set.Defs
/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$.  -/
Set.Iio : {α : Type u_1} → [Preorder α] → α → Set α
-- Mathlib.Algebra.Azumaya.Basic
/-- The following diagram commutes:
```
          e ⊗ eᵒᵖ
A ⊗ Aᵐᵒᵖ  ------------> B ⊗ Bᵐᵒᵖ
  |                        |
  |                        |
  | mulLeftRight R A       | mulLeftRight R B
  |                        |
  V                        V
End R A   ------------> End R B
          e.conj
```
 -/
IsAzumaya.mulLeftRight_comp_congr : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B),
  (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) =
    (↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorZero_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C B).inv.app X)
      ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).inv.app X)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.SmallObject.πObj I κ f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.SmallObject.iteration I κ).obj (CategoryTheory.Arrow.mk f)).hom
      (CategoryTheory.inv
        (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app (CategoryTheory.Arrow.mk f))))
-- Init.Data.BitVec.Bitblast
/-- `extractLsb'` commutes with multiplication.  -/
BitVec.extractLsb'_mul : ∀ {w len : ℕ} {x y : BitVec w},
  len ≤ w → BitVec.extractLsb' 0 len (x * y) = BitVec.extractLsb' 0 len x * BitVec.extractLsb' 0 len y
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, f.NeBot → g.NeBot → (f -ᵥ g).NeBot
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_pos_iff : ∀ (n : Int64), 0 < n.toNatClampNeg ↔ 0 < n
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.orientation_reindex : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} [inst_5 : Fintype ι]
  [inst_6 : DecidableEq ι] [inst_7 : Fintype ι'] [inst_8 : DecidableEq ι'] (e : Module.Basis ι R M) (eι : ι ≃ ι'),
  (e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation
-- Mathlib.Order.Partition.Basic
Partition.eq_partOf_of_mem : ∀ {α : Type u_1} {x : α} {u t : Set α} {P : Partition u}, t ∈ P → x ∈ t → t = P.partOf x
-- Mathlib.Algebra.Polynomial.Homogenize
/-- Summing a function over the coefficients of the homogenization of a polynomial `p`
(of degree `p.natDegree`) gives the same result as summing over the coefficients of `p`.  -/
Polynomial.finsuppSum_homogenize_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] (p : Polynomial R) {f : R → M},
  ((p.homogenize p.natDegree).coeff.sum fun x c => f c) = p.sum fun x c => f c
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_foldrM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → β → m β) (init : β) (xs : Array α)
  (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.foldrM (f x) init xs start stop
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point is the only point in all the Monge planes from any
one vertex.  -/
Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P (n + 2)} {i₁ : Fin (n + 3)} {p : P},
  (∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂) → p = s.mongePoint
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.dualEquiv_inverse : NonemptyFinLinOrd.dualEquiv.inverse = NonemptyFinLinOrd.dual
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Mon C} → (hom : M.X ⟶ N.X) → [isMonHom_hom : CategoryTheory.IsMonHom hom] → M.Hom N
-- Init.Data.BitVec.Lemmas
BitVec.toInt_shiftLeft : ∀ {w n : ℕ} {x : BitVec w}, (x <<< n).toInt = (↑(x.toNat <<< n)).bmod (2 ^ w)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.w_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (φ : f ⟶ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right φ) h) =
    CategoryTheory.CategoryStruct.comp g.hom h
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J_squared : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  Matrix.J l R * Matrix.J l R = -1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Cofork f g}
  (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (k : t.pt ⟶ Z),
  ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_zero_succ : ∀ (k : ℕ), Nat.stirlingFirst 0 k.succ = 0
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a` (version for `a : ℕ`).  -/
jacobiSym.mod_right' : ∀ (a : ℕ) {b : ℕ}, Odd b → jacobiSym (↑a) b = jacobiSym (↑a) (b % (4 * a))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_1 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' x =
    Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.main (fun x => some Turing.PartrecToTM2.Γ'.cons)
      (Turing.PartrecToTM2.Λ'.ret x)
-- Mathlib.Topology.Connected.LocallyPathConnected
PathConnectedSpace.of_locallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] [ConnectedSpace X], PathConnectedSpace X
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_copy : ∀ {R : Type u_2} {A : Type u_3} [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] (S : StarSubalgebra R A) (s : Set A)
  (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.id_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (X : CategoryTheory.DifferentialObject S C),
  (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj
-- Lean.MetavarContext
Lean.DependsOn.State.mk.injEq : ∀ (visited : Lean.ExprSet) (mctx : Lean.MetavarContext) (visited_1 : Lean.ExprSet) (mctx_1 : Lean.MetavarContext),
  ({ visited := visited, mctx := mctx } = { visited := visited_1, mctx := mctx_1 }) =
    (visited = visited_1 ∧ mctx = mctx_1)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toList_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {f : α → Bool},
  m.WF → (Std.HashSet.Raw.filter f m).toList.Perm (List.filter f m.toList)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] (x y : ↑(Set.Ico 0 1)),
  ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.instStarHomClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B],
  StarHomClass (A →⋆* B) A B
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- a map `I₁ × I₂₃ → J`  -/
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.q : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} → (self : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) → I₁ × self.I₂₃ → J
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_positions : ∀ {s : String.Slice}, s.positions.toList = String.Slice.Model.positionsFrom s.startPos
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_image_finset_iff_exists_fun' : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {x : M} {s : Finset α}, x ∈ Submodule.span R (v '' ↑s) ↔ ∃ c, ∑ i ∈ s, c i • v i = x
-- Mathlib.Algebra.Ring.Equiv
/-- Splits the indices of ring `∀ (i : ι), Y i` along the predicate `p`. This is
`Equiv.piEquivPiSubtypeProd` as a `RingEquiv`.  -/
RingEquiv.piEquivPiSubtypeProd : {ι : Type u_7} →
  (p : ι → Prop) →
    [DecidablePred p] →
      (Y : ι → Type u_8) →
        [inst : (i : ι) → NonUnitalNonAssocSemiring (Y i)] →
          ((i : ι) → Y i) ≃+* ((i : { x // p x }) → Y ↑i) × ((i : { x // ¬p x }) → Y ↑i)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- A 1-form `ω` is *curve integrable* along a path `γ`,
if the function `curveIntegralFun ω γ t = ω (γ t) (γ' t)` is integrable on `[0, 1]`.

The actual definition uses `Path.extend γ`,
because both interval integrals and derivatives expect globally defined functions.
 -/
CurveIntegrable : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → {a b : E} → (E → E →L[𝕜] F) → Path a b → Prop
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (fun x => x.addNat m) (Finset.Ioo i j) = Finset.Ioo (i.addNat m) (j.addNat m)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoApp.inv.hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_submodule_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (N ⊓ s).FG
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_norm_rpow_of_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {p q : ℝ},
      0 ≤ p →
        0 ≤ q →
          p ≤ q → MeasureTheory.Integrable (fun x => ‖f x‖ ^ q) μ → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableLocallyUniformly_iff_hasSumLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], SummableLocallyUniformly f ↔ HasSumLocallyUniformly f fun x => ∑' (i : ι), f i x
-- Init.Tactics
/-- Searches environment for definitions or theorems that can solve the goal using `exact`
with conditions resolved by `solve_by_elim`.

The optional `using` clause provides identifiers in the local context that must be
used by `exact?` when closing the goal.  This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.

Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
Use `-star` to disable fallback to star-indexed lemmas (like `Empty.elim`, `And.left`).
Use `+all` to collect all successful lemmas instead of stopping at the first.
 -/
Lean.Parser.Tactic.exact? : Lean.ParserDescr
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.closure.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (s : Set M), SemigroupIdeal.closure s = SubMulAction.closure M s
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.summable_of_locally_summable_norm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [CompleteSpace E] {ι : Type u_3} {F : ι → C(X, E)},
  (∀ (K : TopologicalSpace.Compacts X), Summable fun i => ‖ContinuousMap.restrict (↑K) (F i)‖) → Summable F
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions `F n` is
(eventually) uniformly bounded by a constant and converges (eventually) pointwise to a
function `f`, then the integrals of `F n` with respect to a finite measure `μ` converge
to the integral of `f`.  -/
MeasureTheory.tendsto_setToFun_filter_of_norm_le_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} {l : Filter ι}
  [l.IsCountablyGenerated] {F_1 : ι → α → E} [MeasureTheory.IsFiniteMeasure μ] {f : α → E},
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F_1 n) μ) →
    (∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F_1 n ω‖ ≤ C) →
      (∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun n => F_1 n ω) l (nhds (f ω))) →
        Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (F_1 n)) l (nhds (MeasureTheory.setToFun μ T hT f))
-- Mathlib.Data.ZMod.Basic
ZMod.instSubsingletonModule : ∀ (n : ℕ) (M : Type u_1) [inst : AddCommMonoid M], Subsingleton (Module (ZMod n) M)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.iSup_normal : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (H : ι → Subgroup G) [∀ (i : ι), (H i).Normal], (⨆ i, H i).Normal
-- Init.Data.Slice.Operations
/-- The iterator of a slice `s` of type `Slice γ` emits exactly `SliceSize.size s` elements.  -/
Std.Slice.LawfulSliceSize.lawful : ∀ {α β : Type u_1} {γ : Type u} {inst : Std.Slice.SliceSize γ} {inst_1 : Std.ToIterator (Std.Slice γ) Id α β}
  {inst_2 : Std.Iterator α Id β} [self : Std.Slice.LawfulSliceSize γ] (s : Std.Slice γ),
  Std.Slice.SliceSize.size s = (Std.ToIterator.iter s).length
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablySeparated.mk : ∀ {α : Type u_3} [inst : MeasurableSpace α],
  HasCountableSeparatingOn α MeasurableSet Set.univ → MeasurableSpace.CountablySeparated α
-- Init.SizeOf
List.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf [] = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_neg : ∀ (θ : Real.Angle), (-θ).sign = -θ.sign
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_eval₂ : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {τ : Type u_3} {x : τ → S}
  [inst_1 : CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R),
  (MvPolynomial.eval x) (MvPolynomial.eval₂ f g p) =
    MvPolynomial.eval₂ ((MvPolynomial.eval x).comp f) (fun s => (MvPolynomial.eval x) (g s)) p
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn : n + a = n')
  (a_1 : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'),
  (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn).symm a_1 = a_1.leftUnshift n hn
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrRangeEquiv_apply_coe_fst : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarAddMonoid R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Star A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A] (a : A),
  (↑((Unitization.inrRangeEquiv R A) a)).toProd.1 = 0
-- Init.Data.List.Lemmas
List.head_of_head?_eq_some : ∀ {α : Type u_1} {l : List α} {x : α} (hx : l.head? = some x), l.head ⋯ = x
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.volume_apply : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι),
  MeasureTheory.volume.toBoxAdditive I = ∏ i, (I.upper i - I.lower i)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.IsPrincipal.principal : ∀ {R : Type u_1} {M : Type u_4} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} (S : Submodule R M)
  [self : S.IsPrincipal], ∃ a, S = R ∙ a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x y : ↥(Rep.Hom.hom A.norm).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x =
      (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
-- Init.Data.Array.Lemmas
Array.getElem_set : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h' : i < xs.size) {v : α} {j : ℕ} (h : j < (xs.set i v h').size),
  (xs.set i v h')[j] = if i = j then v else xs[j]
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Mul α] [inst_1 : SMul R α] [SMulCommClass R α α]
  (r : R) (w : m → α) (v : n → α), Matrix.vecMulVec w (r • v) = r • Matrix.vecMulVec w v
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_add : ∀ (m n : ℕ), ↑m + ↑n = ↑(m + n)
-- Lean.Meta.NatTable
_private.Lean.Meta.NatTable.0.Lean.mkNatLookupTable.go : Lean.Expr →
  Lean.Expr →
    (es : Array Lean.Expr) →
      Lean.Level →
        (start stop : ℕ) →
          autoParam (start < stop) Lean.mkNatLookupTable._auto_1✝ →
            autoParam (stop ≤ es.size) Lean.mkNatLookupTable._auto_3✝ → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Properties
/-- A scheme `X` is reduced if all `𝒪ₓ(U)` are reduced.  -/
AlgebraicGeometry.IsReduced : AlgebraicGeometry.Scheme → Prop
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ),
  AlgebraicTopology.DoldKan.N₂Γ₂.hom.app ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj K) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app K)
      (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- Every object is a module over a monoid object via the trivial action.  -/
CategoryTheory.Mod.trivialAction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (M : CategoryTheory.Mon C) → C → CategoryTheory.Mod C M.X
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_iSup : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {ι : Sort u_9} (f : M →ₛₗ[σ₁₂] M₂) (p : ι → Submodule R M),
  Submodule.map f (⨆ i, p i) = ⨆ i, Submodule.map f (p i)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_zero' : ∀ {x : ℝ}, √x = 0 ↔ x ≤ 0
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.card_S_lt_card_T : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) [inst_2 : DecidableEq α]
  [inst_3 : DecidableEq β],
  Fintype.card α < Fintype.card β →
    0 < Fintype.card α →
      (Finset.Icc
            (fun i =>
              ∑ j,
                ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                  -(A i j)⁻)
            fun i =>
            ∑ j,
              ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                (A i j)⁺).card <
        (Finset.Icc 0 fun x =>
            ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊).card