mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp_rat : ∀ (q : ℚ), IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I * ↑q)) q.den
-- Mathlib.SetTheory.Ordinal.Notation
/-- The ordinal represented by an ordinal notation.

This function is noncomputable because ordinal arithmetic is noncomputable. In computational
applications `NONote` can be used exclusively without reference to `Ordinal`, but this function
allows for correctness results to be stated.  -/
NONote.repr : NONote → Ordinal.{0}
-- Mathlib.LinearAlgebra.Orientation
AlternatingMap.constLinearEquivOfIsEmpty.congr_simp : ∀ {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid M''] [inst_2 : AddCommMonoid N''] [inst_3 : Module R' M''] [inst_4 : Module R' N'']
  [inst_5 : IsEmpty ι], AlternatingMap.constLinearEquivOfIsEmpty = AlternatingMap.constLinearEquivOfIsEmpty
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_EStateM : ∀ {ε σ α : Type u_1} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  ⦃Q.2.1 e⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.Analysis.Calculus.ContDiff.Basic
LinearIsometry.contDiff : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  (f : E →ₗᵢ[𝕜] F), ContDiff 𝕜 n ⇑f
-- Mathlib.Order.Partition.Finpartition
Finpartition.le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {b : α}, b ∈ P.parts → b ≤ a
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.not_ex_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)), ¬φ.ex.IsQF
-- Lean.Compiler.ExternAttr
Lean.instHashableExternEntry : Hashable Lean.ExternEntry
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.extract_gcd' : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  (f g : β → α), (∃ x ∈ s, f x ≠ 0) → (∀ b ∈ s, f b = s.gcd f * g b) → s.gcd g = 1
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_roo : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_roo._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLT = true)) t.toList
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.fst : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ},
  IsAddFreimanHom n (A ×ˢ B) A Prod.fst
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)}
  [MeasureTheory.IsProbabilityMeasure μ₀] {a : ℕ},
  (MeasureTheory.Measure.map (Preorder.frestrictLe a) (ProbabilityTheory.Kernel.trajMeasure μ₀ κ)).compProd (κ a) =
    MeasureTheory.Measure.map (fun x => (Preorder.frestrictLe a x, x (a + 1)))
      (ProbabilityTheory.Kernel.trajMeasure μ₀ κ)
-- Mathlib.LinearAlgebra.Complex.Module
/-- The imaginary part `ℑ a` of an element `a` of a star module over `ℂ`, as a linear map into the
self adjoint elements. In a general star module, we have a decomposition into the `selfAdjoint`
and `skewAdjoint` parts, but in a star module over `ℂ` we have
`realPart_add_I_smul_imaginaryPart`, which allows us to decompose into a linear combination of
`selfAdjoint`s.  -/
imaginaryPart : {A : Type u_1} →
  [inst : AddCommGroup A] →
    [inst_1 : Module ℂ A] → [inst_2 : StarAddMonoid A] → [inst_3 : StarModule ℂ A] → A →ₗ[ℝ] ↥(selfAdjoint A)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.RingTheory.Teichmuller
/-- An auxiliary sequence to define the Teichmüller map. The `(n + 1)`-st term is the `p^n`-th
power of an arbitrary lift in `R` of the `n`-th component from the perfection of `R ⧸ I`.  -/
Perfection.teichmullerAux : {p : ℕ} →
  [Fact (Nat.Prime p)] →
    {R : Type u_1} → [inst : CommRing R] → {I : Ideal R} → [CharP (R ⧸ I) p] → Perfection (R ⧸ I) p → ℕ → R
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.bijective_frobeniusAlgHom_pow : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [Finite L], Function.Bijective fun n => FiniteField.frobeniusAlgHom K L ^ ↑n
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.below.superset : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop}
  {s t : Set α} (a : Filter.CardinalGenerateSets g s) (a_1 : s ⊆ t),
  Filter.CardinalGenerateSets.below a → motive s a → Filter.CardinalGenerateSets.below ⋯
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_mono_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : LowerSet α} {t : LowerSet β},
  s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
-- Mathlib.Analysis.Complex.Basic
Complex.ofRealCLM_coe : ↑Complex.ofRealCLM = Complex.ofRealAm.toLinearMap
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_list_eq_max : ∀ (α : Type u) [Nonempty α], Cardinal.mk (List α) = max Cardinal.aleph0 (Cardinal.mk α)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.below.inner : ∀ {α : Type u} {β : α → Type v} {motive : (a : Std.DTreeMap.Internal.Impl α β) → a.Balanced → Prop} {sz : ℕ} {k : α}
  {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (a : l.Balanced) (a_1 : r.Balanced)
  (a_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) (a_3 : sz = l.size + 1 + r.size),
  Std.DTreeMap.Internal.Impl.Balanced.below a →
    motive l a →
      Std.DTreeMap.Internal.Impl.Balanced.below a_1 → motive r a_1 → Std.DTreeMap.Internal.Impl.Balanced.below ⋯
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instSDiff : {α : Type u_1} → {cmp : α → α → Ordering} → SDiff (RBTree.RBSet α cmp)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.exists_iSup_eq_of_isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_5} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.Opens.IsBasis (Set.range U) →
    ∀ (W : TopologicalSpace.Opens X), IsCompact W.carrier → ∃ κ, ∃ (_ : Finite κ), ∃ a, W = ⨆ k, U (a k)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainAlgHom_comp : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] [inst_5 : AddMonoid O]
  (f : M →+ N) (g : N →+ O),
  AddMonoidAlgebra.mapDomainAlgHom R A (g.comp f) =
    (AddMonoidAlgebra.mapDomainAlgHom R A g).comp (AddMonoidAlgebra.mapDomainAlgHom R A f)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
LinearIsometry.map_starProjection' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E')
  (p : Submodule 𝕜 E) [inst_5 : p.HasOrthogonalProjection] [inst_6 : (Submodule.map (↑f) p).HasOrthogonalProjection]
  (x : E), f (p.starProjection x) = (Submodule.map (↑f) p).starProjection (f x)
-- Init.Data.String.Basic
String.get' : (s : String) → (p : String.Pos.Raw) → ¬String.Pos.Raw.atEnd s p = true → Char
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.GroupFilterBasis.hasMem : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace R] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → Membership (Set M) (ModuleFilterBasis R M)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.UInt8.utf8ByteSize_eq_utf8ByteSize_parseFirstByte : ∀ {c : UInt8} {h : c.IsUTF8FirstByte},
  c.utf8ByteSize h = ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ (ByteArray.utf8DecodeChar?.parseFirstByte c)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H] (X : C) {Z : H}
  (h : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X)
      (CategoryTheory.CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
        { base := L.obj X, fiber := CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)) })
      h
-- Mathlib.Algebra.Module.PUnit
PUnit.instIsScalarTowerOfSMul : ∀ {R : Type u_1} {S : Type u_2} [inst : SMul R S], IsScalarTower R S PUnit.{u_3 + 1}
-- Lean.LocalContext
/-- Batched version of `Lean.LocalContext.findFromUserName?`.
Finds the visible local declarations for each of the given `userNames` up to a certain `start`
index exclusively, if any.
 -/
Lean.LocalContext.findFromUserNames : {α : Type} → Lean.LocalContext → Std.HashMap Lean.Name α → optParam ℕ 0 → Array Lean.LocalDecl
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Constructor for `SSet.Edge.CompStruct`.  -/
SSet.Edge.CompStruct.mk : {X : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {e₁₂ : SSet.Edge x₁ x₂} →
        {e₀₂ : SSet.Edge x₀ x₂} →
          (simplex : X.obj (Opposite.op { len := 2 })) →
            autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 2)) simplex = e₀₁.edge)
                _auto_90✝ →
              autoParam
                  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) simplex = e₁₂.edge)
                  _auto_92✝ →
                autoParam
                    ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) simplex = e₀₂.edge)
                    _auto_94✝ →
                  e₀₁.CompStruct e₁₂ e₀₂
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- In a commutative Hopf algebra, the antipode squares to the identity.
 -/
CategoryTheory.HopfObj.antipode_antipode : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp (β_ A A).hom CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul →
    CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode CategoryTheory.HopfObj.antipode =
      CategoryTheory.CategoryStruct.id A
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.id c) d =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Init.Data.List.Erase
List.eraseP_cons_of_pos : ∀ {α : Type u_1} {a : α} {l : List α} {p : α → Bool}, p a = true → List.eraseP p (a :: l) = l
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain'_apply : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ}
  (hh' : Function.LeftInverse h' h) (f : Π₀ (i : ι), β i) (k : κ), (DFinsupp.comapDomain' h hh' f) k = f (h k)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasColimit F.rightOp], CategoryTheory.Limits.HasLimit F
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point `Φ` on a site `(C, J)`, this is the skyscraper presheaf functor
`A ⥤ Cᵒᵖ ⥤ A`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] → CategoryTheory.Functor A (CategoryTheory.Functor Cᵒᵖ A)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRatUnits_postcondition : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  let assignments := (f.insertRatUnits units).1.assignments;
  have hsize := ⋯;
  have ratUnits := (f.insertRatUnits units).1.ratUnits;
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize
-- Mathlib.CategoryTheory.Elements
/-- The equivalence `F.elementsᵒᵖ ≌ (yoneda, F)` is compatible with the forgetful functors.  -/
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.comp
          (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda F) ≅
        (CategoryTheory.CategoryOfElements.π F).leftOp
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_lt_one : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, ↑n < 1 ↔ n = 0
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_tmul_counit_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] CoalgebraStruct.counit (repr.right i) = a ⊗ₜ[R] 1
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_div_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableMul G] [MeasurableInv G] {f : G → F} [μ.IsInvInvariant] [μ.IsMulLeftInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (g / t)) μ
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B), ⇑↑f = ⇑f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_one_iff : ∀ {x : ℂ}, Complex.cos x = 1 ↔ ∃ k, ↑k * (2 * ↑Real.pi) = x
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet) (z : F), ↑e.symm (b, z) = ⟨b, (Bundle.Trivialization.continuousLinearEquivAt R e b hb).symm z⟩
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
summable_star_iff : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α}, Summable (fun b => star (f b)) L ↔ Summable f L
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_neg_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)), (-o).volumeForm = -o.volumeForm
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_add_emod_self_left : ∀ (a b c : ℤ), (a * b + c) % a = c % a
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- If two valuations `v` and `w` are equivalent then `WithVal v` and `WithVal w` are
isomorphic as uniform spaces.  -/
Valuation.IsEquiv.uniformEquiv : {R : Type u_4} →
  {Γ₀ : Type u_5} →
    {Γ₀' : Type u_6} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
          [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] →
            {v : Valuation R Γ₀} → {w : Valuation R Γ₀'} → v.IsEquiv w → WithVal v ≃ᵤ WithVal w
-- Batteries.Data.String.Lemmas
String.splitToList_of_valid : ∀ (s : String) (p : Char → Bool), s.splitToList p = List.map String.ofList (List.splitOnP p s.toList)
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_eq_bot_of_subsingleton : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  Module.supportDim R M = ⊥
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (a : α) (as : List α)
  (b : β) (bs : List β) (acc : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_1 : List β) → (acc : Array γ) → motive x x_1 acc),
  (match a :: as, b :: bs, acc with
    | a :: as, b :: bs, acc => h_1 a as b bs acc
    | x, x_1, acc => h_2 x x_1 acc) =
    h_1 a as b bs acc
-- Mathlib.Topology.AlexandrovDiscrete
/-- The intersection of a family of open sets is an open set. Use `isOpen_sInter` in the root
namespace instead.  -/
AlexandrovDiscrete.isOpen_sInter : ∀ {α : Type u_1} {inst : TopologicalSpace α} [self : AlexandrovDiscrete α] (S : Set (Set α)),
  (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
-- Aesop.Forward.State
Aesop.Hyp.instHashable : Hashable Aesop.Hyp
-- Mathlib.Data.Int.Lemmas
/-- Like `Int.ediv_emod_unique`, but permitting negative `b`.  -/
Int.ediv_emod_unique'' : ∀ {a b r q : ℤ}, b ≠ 0 → (a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|)
-- Mathlib.Data.Set.Sups
/-- `s ⊻ t` is the set of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`.  -/
Set.hasSups : {α : Type u_2} → [SemilatticeSup α] → HasSups (Set α)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F] [T2Space F],
  DifferentiableAt 𝕜 f x → UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_mul : ∀ {a b c : ENNReal}, (0 < b → b < a → c ≠ ⊤) → (a - b) * c = a * c - b * c
-- Mathlib.Data.Fin.VecNotation
/-- `vecAppend ho u v` appends two vectors of lengths `m` and `n` to produce
one of length `o = m + n`. This is a variant of `Fin.append` with an additional `ho` argument,
which provides control of definitional equality for the vector length.

This turns out to be helpful when providing simp lemmas to reduce `![a, b, c] n`, and also means
that `vecAppend ho u v 0` is valid. `Fin.append u v 0` is not valid in this case because there is
no `Zero (Fin (m + n))` instance.  -/
Matrix.vecAppend : {m n : ℕ} → {α : Type u_1} → {o : ℕ} → o = m + n → (Fin m → α) → (Fin n → α) → Fin o → α
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.postcomp_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (H : CategoryTheory.SimplicialObject.Homotopy f g) {Y' : CategoryTheory.SimplicialObject C} (p : Y ⟶ Y') {n : ℕ}
  (i : Fin (n + 1)),
  (H.postcomp p).h i = CategoryTheory.CategoryStruct.comp (H.h i) (p.app (Opposite.op { len := n + 1 }))
-- Mathlib.GroupTheory.Congruence.Defs
addConGen.eq_1 : ∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen r = { r := AddConGen.Rel r, iseqv := ⋯, add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.lift_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (hP.lift h k w) fst = h
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f)
          CategoryTheory.AddMonObj.add))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)
-- Init.Data.SInt.Lemmas
Int16.toUInt16_neg : ∀ (a : Int16), (-a).toUInt16 = -a.toUInt16
-- Lean.Hygiene
Lean.NameSanitizerState.mk : Lean.Options → Lean.NameMap ℕ → Lean.NameMap Lean.Name → Lean.NameSanitizerState
-- Mathlib.Algebra.CubicDiscriminant
Cubic.discr_eq_prod_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → φ P.discr = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
-- Init.Data.Array.Erase
Array.size_eraseP : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (xs.eraseP p).size = if xs.any p = true then xs.size - 1 else xs.size
-- Mathlib.FieldTheory.KummerPolynomial
ne_zero_of_irreducible_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K}, Irreducible (Polynomial.X ^ n - Polynomial.C a) → n ≠ 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.mul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => f x * a
-- Mathlib.Data.Set.Countable
Set.Countable.preimage : ∀ {α : Type u} {β : Type v} {s : Set β}, s.Countable → ∀ {f : α → β}, Function.Injective f → (f ⁻¹' s).Countable