mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Atoms
IsAtom.le_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → b ≠ ⊥ → (b ≤ a ↔ b = a)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCoeSortType.eq_1 : AddCommMonCat.instCoeSortType = { coe := AddCommMonCat.carrier }
-- Mathlib.Order.Category.Semilat
SemilatSupCat_dual_comp_forget_to_partOrd : SemilatSupCat.dual.comp (CategoryTheory.forget₂ SemilatInfCat PartOrd) =
  (CategoryTheory.forget₂ SemilatSupCat PartOrd).comp PartOrd.dual
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The forward direction of the homeomorphism
between the cube $I^N$ and $I × I^{N\setminus\{j\}}$.  -/
Cube.splitAt : {N : Type u_1} → [DecidableEq N] → (i : N) → (N → ↑unitInterval) ≃ₜ ↑unitInterval × ({ j // j ≠ i } → ↑unitInterval)
-- Mathlib.Algebra.Category.ModuleCat.Simple
/-- Any `k`-algebra module which is 1-dimensional over `k` is simple.  -/
simple_of_finrank_eq_one : ∀ {R : Type u_1} [inst : Ring R] {k : Type u_3} [inst_1 : Field k] [inst_2 : Algebra k R] {V : ModuleCat R},
  Module.finrank k ↑V = 1 → CategoryTheory.Simple V
-- Lean.Meta.MethodSpecs
/-- rewrite rules to apply  -/
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.thms : Lean.MethodSpecsInfo✝ → Array Lean.MethodSpecTheorem✝
-- Init.Data.BitVec.Lemmas
BitVec.zero_concat_true : ∀ {w : ℕ}, (0#w).concat true = 1#(w + 1)
-- Mathlib.Probability.Independence.Process.Basic
/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
$(X_{s_1}, ..., X_{s_p})$.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.IndepFun.indepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} {𝓨 : S → Type u_5}
  [inst : MeasurableSpace 𝓧] [inst_1 : (i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i},
  AEMeasurable X P →
    (∀ (i : S), AEMeasurable (Y i) P) →
      (∀ (I : Finset S), ProbabilityTheory.IndepFun X (fun ω i => Y (↑i) ω) P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P], ProbabilityTheory.IndepFun X (fun ω i => Y i ω) P
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.min : {α : Type u} →
  (self : Std.Packages.LinearOrderOfOrdArgs α) →
    let this := self.ord;
    Min α
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_comp_comp : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] {Tₗ : Type u_12} {Tₗ' : Type u_13} [inst_13 : AddCommMonoid Tₗ]
  [inst_14 : AddCommMonoid Tₗ'] [inst_15 : Module R₁ Tₗ] [inst_16 : Module R₂ Tₗ'] [inst_17 : SMulCommClass R₂ R₁ Pₗ]
  (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N) (h : Tₗ →ₗ[R₁] Qₗ) (h' : Tₗ' →ₗ[R₂] Qₗ'),
  f.compl₁₂ (g ∘ₗ h) (g' ∘ₗ h') = (f.compl₁₂ g g').compl₁₂ h h'
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- An object `X` in a category is a *zero object* if for every object `Y`
there is a unique morphism `to : X → Y` and a unique morphism `from : Y → X`.

This is a characteristic predicate for `HasZeroObject`.  -/
CategoryTheory.Limits.IsZero : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Prop
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod_inj : ∀ {n : ℕ} [inst : NeZero n] {x y : ZMod n}, AddChar.zmod n x = AddChar.zmod n y ↔ x = y
-- Mathlib.GroupTheory.Torsion
/-- Finite groups are torsion groups.  -/
isMulTorsion_of_finite : ∀ {G : Type u_1} [inst : Group G] [Finite G], IsMulTorsion G
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_smul_eq_sum : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module A M]
  [inst_4 : Module ℚ M] {a : A} {m : M} {k : ℕ},
  a ^ k • m = 0 → IsNilpotent a → IsNilpotent.exp a • m = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i • m
-- Batteries.Control.ForInStep.Basic
/-- This is similar to a monadic `bind` operator, except that the two type parameters have to be
the same, which prevents putting a monad instance on `ForInStepT m α := m (ForInStep α)`.
 -/
ForInStep.bindM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → m (ForInStep α) → (α → m (ForInStep α)) → m (ForInStep α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.tacticMatrix_simp : Lean.ParserDescr
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_naturality_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} {a : M}
  (f : CategoryTheory.ShiftedHom X Y a) {F G : CategoryTheory.Functor C D} (e : F ≅ G) [inst_5 : F.CommShift M]
  [inst_6 : G.CommShift M] [CategoryTheory.NatTrans.CommShift e.hom M],
  (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (e.hom.app X)).comp
      ((f.map G).comp (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y)) ⋯) ⋯ =
    f.map F
-- Init.Data.Option.Instances
/-- Executes a monadic action on an optional value if it is present, or does nothing if there is no
value.

Examples:
```lean example
#eval ((some 5).forM set : StateM Nat Unit).run 0
```
```output
((), 5)
```
```lean example
#eval (none.forM (fun x : Nat => set x) : StateM Nat Unit).run 0
```
```output
((), 0)
```
 -/
Option.forM : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Pure m] → Option α → (α → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Mathlib.Order.Partition.Finpartition
/-- Adds `b` to a finpartition of `a` to make a finpartition of `a ⊔ b`.  -/
Finpartition.extend : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [IsModularLattice α] →
        [DecidableEq α] → {a b c : α} → Finpartition a → b ≠ ⊥ → Disjoint a b → a ⊔ b = c → Finpartition c
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁δ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (X : C),
  (t.ω₁δ a b c hab hbc).app X =
    CategoryTheory.CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C 1).map
          ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj X))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X)))
          ((CategoryTheory.shiftFunctor C 1).map
            ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X))))))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- The element `t := g ^ d / f ^ e` such that `A_{(fg)} = A_{(f)}[1/t]`.  -/
HomogeneousLocalization.Away.isLocalizationElem : {A : Type u_2} →
  {σ : Type u_3} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [GradedRing 𝒜] → {e d : ℕ} → {f : A} → f ∈ 𝒜 d → {g : A} → g ∈ 𝒜 e → HomogeneousLocalization.Away 𝒜 f
-- Mathlib.NumberTheory.LucasLehmer
/-- The order of `ω` in the unit group is exactly `2^p`.  -/
LucasLehmer.order_ω : ∀ (p' : ℕ), lucasLehmerResidue (p' + 2) = 0 → orderOf (LucasLehmer.ωUnit (p' + 2)) = 2 ^ (p' + 2)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The type of morphisms in `CommMonCat`.  -/
CommMonCat.Hom : CommMonCat → CommMonCat → Type u
-- Mathlib.Topology.Category.TopPair
TopPair.inclAdjProj₁_unit_app : ∀ (X : TopCat), TopPair.inclAdjProj₁.unit.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y Z : CategoryTheory.Over X),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd Y.hom Z.hom) Z.hom
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.digits_two_eq_bits : ∀ (n : ℕ), Nat.digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.mkKey : Lean.Expr → Lean.Meta.CanonM UInt64
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCocone_pt : ∀ {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 : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.coneLeftOpOfCocone c).pt = Opposite.unop c.pt
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  (MeasureTheory.Lp.simpleFunc.toSimpleFunc f).toLp ⋯ = f
-- Mathlib.Probability.Independence.Conditional
/-- A family of measurable space structures (i.e. of σ-algebras) is conditionally independent given
`m'` with respect to a measure `μ` (typically defined on a finer σ-algebra) if the family of sets of
measurable sets they define is independent. `m : ι → MeasurableSpace Ω` is conditionally independent
given `m'` with respect to measure `μ` if for any finite set of indices `s = {i_1, ..., i_n}`, for
any sets `f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then
`μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧ `.
See `ProbabilityTheory.iCondIndep_iff`.  -/
ProbabilityTheory.iCondIndep : {Ω : Type u_1} →
  {ι : Type u_2} →
    (m' : MeasurableSpace Ω) →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          m' ≤ mΩ →
            (ι → MeasurableSpace Ω) →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iCondIndep._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.diff_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}, m₁.diff m₂ = m₁ \ m₂
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
MonoidHom.tendsto_coe_cofinite_of_discrete : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Type u_2}
  [inst_4 : Group H] {f : H →* G},
  Function.Injective ⇑f → IsDiscrete ↑f.range → Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.findMin = t.findMax
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldl_eq_foldl_toProd : ∀ {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ},
  List.foldl (fun a b => f a b.fst b.snd) init l =
    List.foldl (fun a b => f a b.1 b.2) init (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionSemiHomClass.toMonoidHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} {inst : Monoid M} {inst_1 : Monoid N} {inst_2 : Monoid A}
  {inst_3 : Monoid B} {inst_4 : MulDistribMulAction M A} {inst_5 : MulDistribMulAction N B} {inst_6 : FunLike F A B}
  [self : MulDistribMulActionSemiHomClass F φ A B], MonoidHomClass F A B
-- Mathlib.CategoryTheory.Join.Final
CategoryTheory.Join.instInitialInclLeftOfIsConnected : ∀ (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] [CategoryTheory.IsConnected C],
  (CategoryTheory.Join.inclLeft C D).Initial
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableEqOrdinal : DecidableEq Std.Time.Minute.Ordinal
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.mk.injEq : ∀ (exception : Lean.Exception) (state : Lean.Elab.Tactic.SavedState) (exception_1 : Lean.Exception)
  (state_1 : Lean.Elab.Tactic.SavedState),
  ({ exception := exception, state := state } = { exception := exception_1, state := state_1 }) =
    (exception = exception_1 ∧ state = state_1)
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.ranges_flatten : ∀ (l : List ℕ), l.ranges.flatten = List.range l.sum
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis : ∀ {R : Type u_4} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι],
  B.Nondegenerate →
    ∀ (b : Module.Basis ι S M),
      B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.to_implicitFunctionOfComplemented : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  HasStrictFDerivAt (HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f a)) (↑f').ker.subtypeL 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_map : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂]
  [inst_12 : Module R₂ N₂] [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] [inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N),
  (TensorProduct.map f₂ g₂) ((TensorProduct.map f₁ g₁) x) = (TensorProduct.map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁)) x
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.zero_addConvolution : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E'), DiscreteConvolution.addConvolution L 0 f = 0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  s.totalVariation.MutuallySingular μ ↔
    s.toJordanDecomposition.posPart.MutuallySingular μ ∧ s.toJordanDecomposition.negPart.MutuallySingular μ
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformAddGroup β] [IsRightUniformAddGroup β]`
instead of the more typical (and equivalent) `[IsUniformAddGroup β]` because this is used
in the proof of said equivalence.  -/
tendsto_addConj_nhds_zero : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β],
  Filter.Tendsto (fun gx => gx.1 + gx.2 + -gx.1) (Filter.comap Prod.snd (nhds 0)) (nhds 0)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
  (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
    ∀ [inst_3 : CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C],
      (∀ (G : CategoryTheory.Functor ℕᵒᵖ C),
          (∀ (n : ℕ), CategoryTheory.EffectiveEpi (G.map (CategoryTheory.homOfLE ⋯).op)) →
            CategoryTheory.EffectiveEpi (CategoryTheory.Limits.limit.π G (Opposite.op 0))) →
        CategoryTheory.Sheaf.IsLocallySurjective (c.π.app (Opposite.op 0))
-- Std.Do.WP.SimpLemmas
Option.orElse.eq_2 : ∀ {α : Type u_1} (x : Unit → Option α), none.orElse x = x ()
-- Mathlib.CategoryTheory.Sites.Over
/-- **Alias** of `RelIso.map_rel_iff`. -/
CategoryTheory.Sieve.overEquiv_le_overEquiv_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a b : α}, s (f a) (f b) ↔ r a b
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) (a : α), MeasurableSet {a} → p.toMeasure {a} = p a
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules.
Then there is a function from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))`
defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.  -/
PiTensorProduct.piTensorHomMapFun₂ : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              {t' : ι → Type u_12} →
                [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                  [inst_4 : (i : ι) → Module R (t i)] →
                    [inst_5 : (i : ι) → AddCommMonoid (t' i)] →
                      [inst_6 : (i : ι) → Module R (t' i)] →
                        (PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i) →
                          (PiTensorProduct R fun i => s i) →ₗ[R]
                            (PiTensorProduct R fun i => t i) →ₗ[R] PiTensorProduct R fun i => t' i
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Cotangent.map_sub_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f g : P.Hom P'),
  Algebra.Extension.Cotangent.map f - Algebra.Extension.Cotangent.map g = f.sub g ∘ₗ P.cotangentComplex
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_cos : Measurable Complex.cos
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.add` -/
DifferentiableAt.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → DifferentiableAt 𝕜 (fun i => f i + g i) x
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : ℕ},
  IsRelPrime x y → IsRelPrime (x ^ m) (y ^ n)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  s ∈ nhds x → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracket I V W x
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative ring.  -/
ModuleCat.instCommRingCarrierTensorUnit : {R : Type u} → [inst : CommRing R] → CommRing ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_5) {Z : C}
  (h : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.d (CategoryTheory.CategoryStruct.id i₀) f₁ (CategoryTheory.CategoryStruct.id i₁) f₂
        (CategoryTheory.CategoryStruct.id i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (CategoryTheory.CategoryStruct.comp (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom h) =
    CategoryTheory.CategoryStruct.comp (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂ n₁ n₂ hn₂) h)
-- Lean.MetavarContext
Lean.MetavarKind.isSyntheticOpaque : Lean.MetavarKind → Bool
-- Mathlib.Topology.Order.LowerUpperTopology
/-- A recursor for `WithLower`. Use as `induction x`.  -/
Topology.WithLower.rec : {α : Type u_1} →
  {motive : Topology.WithLower α → Sort u_3} →
    ((a : α) → motive (Topology.WithLower.toLower a)) → (a : Topology.WithLower α) → motive a
-- Mathlib.Algebra.Order.Monovary
monovaryOn_iff_forall_mul_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.reflTransGen_le_of_le`. -/
Relation.reflTransGen_of_isTrans_reflexive : ∀ {α : Type u_1} {r r' : α → α → Prop} [Std.Refl r] [IsTrans α r], r' ≤ r → Relation.ReflTransGen r' ≤ r
-- Lean.Parser.Command
Lean.Parser.Command.declValEqns : Lean.Parser.Parser
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_addCommute : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (y : β),
  (∀ x ∈ s, AddCommute y (f x)) → AddCommute y (s.noncommSum f comm)
-- Mathlib.Algebra.Lie.Abelian
LieModule.ker.eq_1 : ∀ (R : Type u) (L : Type v) (M : Type w) [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],
  LieModule.ker R L M = (LieModule.toEnd R L M).ker