mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If `f` is continuous at `a` and differentiable on `Ioi a`, then `f` is continuous on
`Ici a`.  -/
_private.Mathlib.Analysis.Calculus.DerivativeTest.0.continuousOn_Ici : ∀ {f : ℝ → ℝ} {a : ℝ}, ContinuousAt f a → DifferentiableOn ℝ f (Set.Ioi a) → ContinuousOn f (Set.Ici a)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  {x y : M},
  DividedPowerAlgebra.dp R n (x + y) =
    ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, DividedPowerAlgebra.dp R k.1 x * DividedPowerAlgebra.dp R k.2 y
-- Mathlib.Order.BourbakiWitt
NonemptyChain.mk.inj : ∀ {α : Type u_4} {inst : LE α} {carrier : Set α} {Nonempty' : carrier.Nonempty}
  {isChain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier} {carrier_1 : Set α} {Nonempty'_1 : carrier_1.Nonempty}
  {isChain'_1 : IsChain (fun x1 x2 => x1 ≤ x2) carrier_1},
  { carrier := carrier, Nonempty' := Nonempty', isChain' := isChain' } =
      { carrier := carrier_1, Nonempty' := Nonempty'_1, isChain' := isChain'_1 } →
    carrier = carrier_1
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : RightCancelSemigroup α],
  MulOpposite.instLeftCancelSemigroup = { toSemigroup := MulOpposite.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_of_frequently_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : ConditionallyCompleteLattice α] {f : Filter ι} {u : ι → α} {a : α},
  (∃ᶠ (i : ι) in f, u i ≤ a) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_of_frequently_le._auto_1 →
      Filter.liminf u f ≤ a
-- Lean.Parser.Do
Lean.Parser.Term.doSeqBracketed.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C × C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalCategory.tensor C) X Y =
    CategoryTheory.MonoidalCategory.tensorδ X.1 X.2 Y.1 Y.2
-- Mathlib.Data.Int.Order.Lemmas
Int.abs_le_sqrt_iff_sq_le : ∀ {a b : ℤ}, 0 ≤ b → (|a| ≤ Int.sqrt b ↔ a ^ 2 ≤ b)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U)
  (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (P.map (p.map f).op)
      (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp V P) =
    CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P
-- Mathlib.Data.List.Lattice
_private.Mathlib.Data.List.Lattice.0.List.bagInter.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂),
  (match [], x with
    | [], x => h_1 x
    | x, [] => h_2 x
    | a :: l₁, l₂ => h_3 a l₁ l₂) =
    h_1 x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.supportsStmt_read : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ)
  {S : Finset (Turing.TM1to1.Λ' Γ Λ σ)} {f : Γ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ},
  (∀ (a : Γ), Turing.TM1.SupportsStmt S (f a)) → Turing.TM1.SupportsStmt S (Turing.TM1to1.read dec f)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_eq_zero_iff : ∀ {α : Type u_1} {M : Matroid α}, M.eRank = 0 ↔ M = Matroid.loopyOn M.E
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- A variant of `PiTensorProduct.tmulEquiv` with the result indexed by `Fin (n + m)`.  -/
TensorPower.mulEquiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {n m : ℕ} → TensorProduct R (TensorPower R n M) (TensorPower R m M) ≃ₗ[R] TensorPower R (n + m) M
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of seminormed groups, using the sup norm.  -/
Prod.seminormedAddGroup : {E : Type u_2} → {F : Type u_3} → [SeminormedAddGroup E] → [SeminormedAddGroup F] → SeminormedAddGroup (E × F)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- If elements `p,q` of `FreeAddMonoid (R × Π i, s i)` lift elements `x,y` of `⨂[R] i, s i`
respectively, then `p + q` lifts `x + y`.
 -/
PiTensorProduct.lifts_add : ∀ {ι : 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)] {x y : PiTensorProduct R fun i => s i}
  {p q : FreeAddMonoid (R × ((i : ι) → s i))}, p ∈ x.lifts → q ∈ y.lifts → p + q ∈ (x + y).lifts
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {f : β k → β k}, (↑(m.modify k f)).isEmpty = (↑m).isEmpty
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_mirror : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → u ≠ 0 → w ≠ 0 → (Polynomial.trinomial k m n u v w).mirror = Polynomial.trinomial k (n - m + k) n w v u
-- Mathlib.Algebra.Quaternion
/-- Coercion `R → ℍ[R,c₁,c₂,c₃]`.  -/
QuaternionAlgebra.coe : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → R → QuaternionAlgebra R c₁ c₂ c₃
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two finite and free modules are isomorphic if they have the same (finite) rank.  -/
LinearEquiv.ofFinrankEq : {R : Type u} →
  (M : Type v) →
    (M' : Type v') →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [Module.Free R M] →
              [inst_4 : AddCommMonoid M'] →
                [inst_5 : Module R M'] →
                  [Module.Free R M'] →
                    [StrongRankCondition R] →
                      [Module.Finite R M] → [Module.Finite R M'] → Module.finrank R M = Module.finrank R M' → M ≃ₗ[R] M'
-- ImportGraph.Imports.Redundant
/-- Return the redundant imports (i.e. those transitively implied by another import)
amongst a candidate list of imports.
 -/
Lean.Environment.findRedundantImports : Lean.Environment → Array Lean.Name → Lean.NameSet
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.isOrdered.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Option α → Sort u_2) →
    (l r : Option α) →
      ((l r : α) → motive (some l) (some r)) →
        ((x x_1 : Option α) → (∀ (l r : α), x = some l → x_1 = some r → False) → motive x x_1) → motive l r
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Typeclass for substructures `s` such that `s ∪ s⁻¹ = G`.  -/
HasMemOrInvMem : {S : Type u_3} → {G : Type u_4} → [Inv G] → [SetLike S G] → S → Prop
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instZero : {𝕜 : Type u_1} → [inst : Zero 𝕜] → [inst_1 : PseudoMetricSpace 𝕜] → Zero ↑(Metric.closedBall 0 1)
-- Mathlib.Data.Holor
Holor.unitVec.eq_1 : ∀ {α : Type} [inst : Monoid α] [inst_1 : AddMonoid α] (d j : ℕ) (ti : HolorIndex [d]),
  Holor.unitVec d j ti = if ↑ti = [j] then 1 else 0
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_eq_ofNat : ∀ (n : ℕ) {h : n < UInt8.size}, UInt8.ofNatLT n h = UInt8.ofNat n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt}
  (α : ModuleCat.of (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM) ⟶ N) {X : Cᵒᵖ} (x : ↑(M.obj X)),
  (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.ModuleColimit.homEquiv hcR hcM) α).app X)) x =
    (CategoryTheory.ConcreteCategory.hom α) ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x)
-- Mathlib.Topology.Connected.LocallyPathConnected
pathComponentIn_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X} [LocallyPathConnectedSpace X],
  F ∈ nhds x → pathComponentIn F x ∈ nhds x
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioc_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ioc a b, f (Fin.cast h i)
-- Mathlib.RingTheory.Polynomial.Selmer
Polynomial.trinomial.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (k m n : ℕ) (u v w : R),
  Polynomial.trinomial k m n u v w =
    Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.derivableRef : IO.Ref Lean.NameSet
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.etale_le_weaklyEtale : @AlgebraicGeometry.Etale ≤ @AlgebraicGeometry.WeaklyEtale
-- Mathlib.NumberTheory.FermatPsp
/-- For all positive bases, there exist infinitely many **Fermat pseudoprimes** to that base.
Given in this form: for all numbers `b ≥ 1` and `m`, there exists a pseudoprime `n` to base `b` such
that `m ≤ n`. This form is similar to `Nat.exists_infinite_primes`.
 -/
Nat.exists_infinite_pseudoprimes : ∀ {b : ℕ}, 1 ≤ b → ∀ (m : ℕ), ∃ n, n.FermatPsp b ∧ m ≤ n
-- Mathlib.Order.Defs.PartialOrder
instTransLE : {α : Type u_1} → [inst : Preorder α] → Trans LE.le LE.le LE.le
-- Mathlib.Order.SuccPred.Limit
/-- A predecessor limit is a value that isn't maximal and isn't covered by any other.

It's so named because in a predecessor order, a predecessor limit can't be the predecessor of
anything larger.

Use `IsPredPrelimit` if you want to include the case of a maximal element.  -/
Order.IsPredLimit : {α : Type u_1} → [Preorder α] → α → Prop
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.natDenominator_dvd_iff : ∀ {S : Type u_2} [inst : CommRing S] {n : ℕ} {x : S}, Algebra.natDenominator x ∣ n ↔ IsIntegral ℤ (n • x)
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂)
  (sq₁₃ : G.PullbackObjObj f₁ f₃),
  CategoryTheory.HasLiftingProperty sq₁₂.ι f₃ ↔ CategoryTheory.HasLiftingProperty f₂ sq₁₃.π
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.List.alternatingSum.match_1.eq_1 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (h_1 : Unit → motive []) (h_2 : (g : G) → motive [g])
  (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match [] with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_1 ()
-- Mathlib.Data.Matrix.Basic
Matrix.transpose_list_prod : ∀ {m : Type u_2} {α : Type u_11} [inst : CommSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (l : List (Matrix m m α)), l.prod.transpose = (List.map Matrix.transpose l).reverse.prod
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Ioc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a < b → IsConnected (Set.Ioc a b)
-- Mathlib.Order.InitialSeg
PrincipalSeg.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s]
  {f g : PrincipalSeg r s}, (∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x) → f = g
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The type of blocks for a group action containing a given element is a bounded order.  -/
MulAction.BlockMem.instBoundedOrder : (G : Type u_1) →
  [inst : Group G] → {X : Type u_2} → [inst_1 : MulAction G X] → (a : X) → BoundedOrder (MulAction.BlockMem G a)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_false : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : False → M), ∑ᶠ (i : False), f i = 0
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittOne.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittOne p = wittStructureInt p 1
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instReprState : Repr Std.Http.Protocol.H1.Writer.State
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f : α → G}
  [MeasurableSub G], Measurable f → ∀ (c : G), Measurable fun x => c - f x
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- the induced functor on the constructed localized categories is an equivalence  -/
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsLocalizedEquivalence], (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.discreteTopology_iff_of_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {H : AddSubgroup G} [H.FiniteIndex], DiscreteTopology ↥H ↔ DiscreteTopology G
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone is a limit cone exactly if
there is a unique cone morphism from any other cone.
 -/
CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t ≅ (s : CategoryTheory.Limits.Cone F) → Unique (s ⟶ t)
-- Mathlib.Data.List.AList
AList.instInhabited : {α : Type u} → {β : α → Type v} → Inhabited (AList β)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_smul : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M),
  fₗ (c • x) = c • fₗ x
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instSub : {α : Type u_2} → [Sub α] → Sub (Filter α)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order_eq_zero_iff : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, p ≠ 0 → (p.order = 0 ↔ p 0 ≠ 0)
-- Batteries.Data.List.Basic
List.takeList.eq_1 : ∀ {α : Type u_1} (x : List α), x.takeList [] = ([], x)
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instIsStableUnderBaseChangePrecoverage : TopCat.precoverage.IsStableUnderBaseChange
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mk'.sizeOf_spec : ∀ {p : ℕ} {R : Type u_1} [inst : SizeOf R] (coeff : ℕ → R), sizeOf { coeff := coeff } = 1
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` is a nontrivial multiplicative character on a finite field `F`, then `J(1,χ) = -1`.  -/
jacobiSum_one_nontrivial : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R] [IsDomain R]
  {χ : MulChar F R}, χ ≠ 1 → jacobiSum 1 χ = -1
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instLocallyCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [LocallyCompactSpace α], LocallyCompactSpace (TopologicalSpace.Compacts α)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.ext : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e₁ e₂ : M ≃ₗ⁅R,L⁆ N), (∀ (m : M), e₁ m = e₂ m) → e₁ = e₂
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsNeg : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.AllZero → ¬li.FirstNonzeroIsNeg
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- Given an homotopy between morphisms of cochain complexes indexed by `ℤ`,
this is the corresponding homotopy between morphisms of cochain complexes
in the opposite category.  -/
CochainComplex.homotopyOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {f g : K ⟶ L} →
          Homotopy f g →
            Homotopy ((CochainComplex.opEquivalence C).functor.map f.op)
              ((CochainComplex.opEquivalence C).functor.map g.op)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux.eq_1 : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommSemiring K] [inst_1 : CommSemiring L]
  [inst_2 : CommSemiring M] (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : PerfectRing M p]
  [inst_5 : IsPRadical i p] (x : L),
  PerfectRing.liftAux i j p x = (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2)
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.skewSwap_symm_apply : ∀ {R : Type u} {M : Type v} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (x : N × M), (LinearEquiv.skewSwap R M N).symm x = (x.2, -x.1)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.mod_two_pow_succ : ∀ (x i : ℕ), x % 2 ^ (i + 1) = 2 ^ i * (x.testBit i).toNat + x % 2 ^ i
-- Mathlib.RingTheory.Teichmuller
Perfection.mk_comp_teichmuller' : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R],
  ⇑(Ideal.Quotient.mk I) ∘ ⇑(Perfection.teichmuller p I) = ⇑(Perfection.coeff (R ⧸ I) p 0)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeNF.of_j_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R} [W.IsShortNF], W.IsCharThreeNF
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_apply_eq : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) {x : S}
  {y : R}, e.symm x = y ↔ x = e y
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.cancel_factors_eq : ∀ {α : Type u_1} [inst : Field α] {a b ad bd a' b' gcd : α},
  ad * a = a' → bd * b = b' → ad ≠ 0 → bd ≠ 0 → gcd ≠ 0 → (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0
-- Lean.Data.DeclarationRange
Lean.instToExprDeclarationRanges : Lean.ToExpr Lean.DeclarationRanges
-- Std.Http.Internal.IndexMultiMap
/-- Creates a multimap from a list of key-value pairs.
 -/
Std.Internal.IndexMultiMap.ofList : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → List (α × β) → Std.Internal.IndexMultiMap α β
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instHasColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasColimits (CategoryTheory.CosimplicialObject C)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.add : ∀ {x y : ℝ*}, x.Infinitesimal → y.Infinitesimal → (x + y).Infinitesimal
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Ici_eq_Ici_iInf : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R},
  ⨅ i, f i ∈ Set.range f → ⋃ i, Set.Ici (f i) = Set.Ici (⨅ i, f i)
-- Mathlib.Topology.Homotopy.Path
/-- Given a path `p`, we can define a `Homotopy p p` by `F (t, x) = p x`.
 -/
Path.Homotopy.refl : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → (p : Path x₀ x₁) → p.Homotopy p
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- When `η` is an s-finite kernel, `borelMarkovFromReal Ω η` is an s-finite kernel.  -/
ProbabilityTheory.Kernel.instIsSFiniteKernelBorelMarkovFromReal : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (η : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsSFiniteKernel η],
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.tendsto_coe : ∀ {α : Type u} {f : Filter α} {m : α → NNReal} {a : NNReal},
  Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_hom_snd_assoc : ∀ (X Y : TopCat) {Z : TopCat} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodSnd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Init.Data.List.Lemmas
List.getElem_eq_iff : ∀ {α : Type u_1} {x : α} {l : List α} {i : ℕ} (h : i < l.length), l[i] = x ↔ l[i]? = some x
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkColGe.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coe_unop : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I : TwoSidedIdeal Rᵐᵒᵖ}, ↑I.unop = MulOpposite.op ⁻¹' ↑I
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.op_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), h.op.i = h.p.op