mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Defs
one_le_inv_of_le_one : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α}, a ≤ 1 → 1 ≤ a⁻¹
-- Mathlib.Order.Std
/-- `min a b` is equivalent to `if a ≤ b then a else b`.  -/
LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMin : ∀ {α : Type u_1} (self : LinearOrder.OfStdArgs α), Std.LawfulOrderLeftLeaningMin α
-- Mathlib.Data.Finset.Sigma
Finset.sigmaLift_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i},
  (Finset.sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty
-- Mathlib.Util.Export
Lean.Export.Entry.defn : Lean.Name → Lean.Export.Entry
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.write.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a : Γ} {a_1 : Turing.TM1.Stmt Γ Λ σ} {a_2 : Γ}
  {a_3 : Turing.TM1.Stmt Γ Λ σ}, Turing.TM1to1.Λ'.write a a_1 = Turing.TM1to1.Λ'.write a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.id_apply : ∀ (M : AddMagmaCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Init.Data.List.MinMaxOn
List.minOn?_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α)
  (f : α → β), List.minOn? f (xs ++ ys) = Option.merge (minOn f) (List.minOn? f xs) (List.minOn? f ys)
-- Mathlib.Topology.VectorBundle.Basic
/-- Make a `VectorBundle` from a `VectorPrebundle`.  Concretely this means
that, given a `VectorPrebundle` structure for a sigma-type `E` -- which consists of a
number of "pretrivializations" identifying parts of `E` with product spaces `U × F` -- one
establishes that for the topology constructed on the sigma-type using
`VectorPrebundle.totalSpaceTopology`, these "pretrivializations" are actually
"trivializations" (i.e., homeomorphisms with respect to the constructed topology).  -/
VectorPrebundle.toVectorBundle : ∀ {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 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E), VectorBundle R F E
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preservesHomology : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesHomology], h.IsPreservedBy F
-- Init.Data.BitVec.Lemmas
BitVec.udiv_ne_zero_iff_ne_zero_and_le : ∀ {w : ℕ} {x y : BitVec w}, ¬x / y = 0#w ↔ y ≠ 0#w ∧ y ≤ x
-- Lean.Expr
Lean.Expr.isFalse : Lean.Expr → Bool
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.instIsScalarTowerTensorProduct_1 : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B], IsScalarTower A B (TensorProduct R S Ω[A⁄R])
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.symmₗ.eq_1 : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B),
  Bundle.Pretrivialization.symmₗ R e b = if hb : b ∈ e.baseSet then IsLinearMap.mk' (e.symm b) ⋯ else 0
-- Mathlib.Order.Lattice
AntitoneOn.map_sup : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [inst : LinearOrder α] [inst_1 : SemilatticeInf β],
  AntitoneOn f s → x ∈ s → y ∈ s → f (max x y) = f x ⊓ f y
-- Std.Internal.UV.System
/-- Gets the current working directory.
 -/
Std.Internal.UV.System.cwd : IO String
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.mk : Lean.ExprSet → Lean.FVarIdSet → Array Lean.FVarId → Lean.CollectFVars.State
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'_eq : ∀ (s : String), String.utf8ByteSize'✝ s = s.utf8ByteSize
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerms.mk.injEq : ∀ (numFixed : ℕ) (perms : Array Lean.Elab.FixedParamPerm) (revDeps : Array (Array (Array ℕ))) (numFixed_1 : ℕ)
  (perms_1 : Array Lean.Elab.FixedParamPerm) (revDeps_1 : Array (Array (Array ℕ))),
  ({ numFixed := numFixed, perms := perms, revDeps := revDeps } =
      { numFixed := numFixed_1, perms := perms_1, revDeps := revDeps_1 }) =
    (numFixed = numFixed_1 ∧ perms = perms_1 ∧ revDeps = revDeps_1)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
isOpen_extChartAt_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), IsOpen (extChartAt I x).source
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_alg : ∀ {K : Type u_1} [inst : RCLike K] (x : ℝ), ↑x = x • 1
-- Mathlib.Data.Fin.SuccPred
Fin.lt_succ_castPred : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n), a < (a.castPred ha).succ
-- Init.Data.SInt.Basic
/-- The number of distinct values representable by `Int8`, that is, `2^8 = 256`.  -/
Int8.size : ℕ
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.Result.mk.inj : ∀ {α : Type} {filtered : Option ProofWidgets.Html} {unfiltered : ProofWidgets.Html} {key : α}
  {pattern : ProofWidgets.Html} {filtered_1 : Option ProofWidgets.Html} {unfiltered_1 : ProofWidgets.Html} {key_1 : α}
  {pattern_1 : ProofWidgets.Html},
  { filtered := filtered, unfiltered := unfiltered, key := key, pattern := pattern } =
      { filtered := filtered_1, unfiltered := unfiltered_1, key := key_1, pattern := pattern_1 } →
    filtered = filtered_1 ∧ unfiltered = unfiltered_1 ∧ key = key_1 ∧ pattern = pattern_1
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.σ_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.isRegular_pairing_iff : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.pairing.IsRegular ↔ h.IsRegular
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubmonoid_fixedPoints_gc : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubmonoid M)
    ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Mono f] → Inhabited (CategoryTheory.Limits.MonoFactorisation f)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticWith.default : {α : Type} → [Inhabited α] → Lean.Lsp.DiagnosticWith α
-- Mathlib.Algebra.Star.LinearMap
TensorProduct.intrinsicStar_map : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : CommSemiring R]
  [inst_1 : StarRing R] [inst_2 : AddCommMonoid E] [inst_3 : StarAddMonoid E] [inst_4 : Module R E]
  [inst_5 : StarModule R E] [inst_6 : AddCommMonoid F] [inst_7 : StarAddMonoid F] [inst_8 : Module R F]
  [inst_9 : StarModule R F] [inst_10 : AddCommMonoid G] [inst_11 : StarAddMonoid G] [inst_12 : Module R G]
  [inst_13 : StarModule R G] [inst_14 : AddCommMonoid H] [inst_15 : StarAddMonoid H] [inst_16 : Module R H]
  [inst_17 : StarModule R H] (f : WithConv (E →ₗ[R] F)) (g : WithConv (G →ₗ[R] H)),
  star (WithConv.toConv (TensorProduct.map f.ofConv g.ofConv)) =
    WithConv.toConv (TensorProduct.map (star f).ofConv (star g).ofConv)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.esymm_to_weight : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] (k : ℕ),
  ↑k * MvPolynomial.esymm σ R k =
    (-1) ^ k *
      ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k with t.1.card = k, MvPolynomial.NewtonIdentities.weight✝ σ R k t
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- Except possibly for `t`, the neighbours of `s` in `G.replaceVertex s t` are its neighbours in
`G`.  -/
SimpleGraph.adj_replaceVertex_iff_of_ne_left : ∀ {V : Type u_1} (G : SimpleGraph V) (s : V) {t : V} [inst : DecidableEq V] {w : V},
  w ≠ t → ((G.replaceVertex s t).Adj s w ↔ G.Adj s w)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_ofSliceTo_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  q ≤ String.Slice.Pos.ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h ≤ p
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
AddMonoidAlgebra.smul_eq : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : VAdd G P] [inst_1 : IsLeftCancelVAdd G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V)
  (p : P) (hp : optParam ((↑f.coeff.support).vaddAntidiagonal (Function.support x) p).Finite ⋯),
  (f • x) p = ∑ gh ∈ Finset.VAddAntidiagonal p hp, f.coeff gh.1 • x gh.2
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The map `X.obj Δ ⟶ Z` obtained by providing a family of morphisms on all the
terms of decomposition given by a splitting `s : Splitting X`  -/
CategoryTheory.SimplicialObject.Splitting.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        {Z : C} →
          (Δ : SimplexCategoryᵒᵖ) →
            ((A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) → s.N (Opposite.unop A.fst).len ⟶ Z) →
              (X.obj Δ ⟶ Z)
-- Mathlib.Algebra.Group.ULift
ULift.pow : {α : Type u} → {β : Type v} → [Pow α β] → Pow (ULift.{u_1, u} α) β
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_lsub_iff : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}),
  iSup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList_ofList : ∀ {α : Type u} (l : List α), l ∈ (↑l).toList
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_iff_ne : ∀ {α : Type u_1} {s t : Multiset α}, Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
-- Mathlib.Order.Interval.Finset.Nat
Nat.range_eq_Icc_zero_sub_one : ∀ (n : ℕ), n ≠ 0 → Finset.range n = Finset.Icc 0 (n - 1)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.instId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (CategoryTheory.Functor.id C).IsTriangulated
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.instAddCancelCommMonoid : {α : Type u} → [CancelCommMonoid α] → AddCancelCommMonoid (Additive α)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_mk : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (s : Subsemiring L)
  (hK : ∀ (x : K), (algebraMap K L) x ∈ s)
  (hi :
    ∀ x ∈ { toSubsemiring := s, algebraMap_mem' := hK }.carrier,
      x⁻¹ ∈ { toSubsemiring := s, algebraMap_mem' := hK }.carrier)
  (x : L), x ∈ { toSubsemiring := s, algebraMap_mem' := hK, inv_mem' := hi } ↔ x ∈ s
-- Aesop.Tree.Data
Aesop.Rapp.appliedRule : Aesop.Rapp → Aesop.RegularRule
-- Mathlib.Data.Multiset.Bind
Multiset.join_cons : ∀ {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)), (s ::ₘ S).join = s + S.join
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.algebraMap_image : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A],
  SpectrumRestricts a f → ⇑(algebraMap R S) '' spectrum R a = spectrum S a
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.Scheme.component_nontrivial : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens) [Nonempty ↥↑U], Nontrivial ↑(X.presheaf.obj (Opposite.op U))
-- Mathlib.Algebra.Order.Field.Basic
div_le_self : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 ≤ a → 1 ≤ b → a / b ≤ a
-- Mathlib.Data.Setoid.Basic
/-- If `f` has a computable right-inverse, then the quotient by its kernel is equivalent to its
domain.  -/
Setoid.quotientKerEquivOfRightInverse : {α : Type u_1} → {β : Type u_2} → (f : α → β) → (g : β → α) → Function.RightInverse g f → Quotient (Setoid.ker f) ≃ β
-- Mathlib.LinearAlgebra.FreeModule.Finite.Basic
Module.Finite.matrix : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Module.Free R M] [Module.Finite R M] [Finite ι₁] [Finite ι₂], Module.Finite R (Matrix ι₁ ι₂ M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W'.negY Q * P 2 → P 1 = W'.negY P
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_add_right_eq_map : ∀ {m n : ℤ}, (m...=m + n).toArray = Array.map (fun x => x + m) (0...=n).toArray
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_push_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : ℕ → α → β} {ys : Vector β n} {xs : Vector α (n + 1)} {b : β},
  Vector.mapIdx f xs = ys.push b ↔ ∃ a zs, xs = zs.push a ∧ Vector.mapIdx f zs = ys ∧ f n a = b
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_Except_eq : ∀ {ε : Type u_1} {α : Type u_2} {p : α → Prop} {x : Except ε α}, SatisfiesM p x ↔ ∀ (a : α), x = Except.ok a → p a
-- Mathlib.Algebra.DirectSum.Internal
/-- The canonical algebra isomorphism between `⨁ i, A i` and `R`.  -/
DirectSum.coeAlgHom : {ι : Type u_1} →
  {S : Type u_3} →
    {R : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring S] →
            [inst_3 : Semiring R] →
              [inst_4 : Algebra S R] →
                (A : ι → Submodule S R) → [inst_5 : SetLike.GradedMonoid A] → (DirectSum ι fun i => ↥(A i)) →ₐ[S] R
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn.go : {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
      (t : Lean.Lsp.Ipc.ModuleHierarchy) →
        ((t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t) →
              motive_1 t ×' t.below
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral
of their sum. The other inequality needs one of these functions to be (a.e.-)measurable.  -/
MeasureTheory.le_lintegral_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
  ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ
-- Mathlib.FieldTheory.PrimitiveElement
Field.isAlgebraic_of_adjoin_eq_adjoin : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} {m n : ℕ},
  m ≠ n → F⟮α ^ m⟯ = F⟮α ^ n⟯ → IsAlgebraic F α
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.MonoidalClosed.linearHomEquiv_symm_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A ⟹ C),
  (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquiv A B C).symm f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).flip
-- Mathlib.Topology.Category.Sequential
Sequential.instCoeSortType : CoeSort Sequential (Type u_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.toPartialEquiv_injective : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective fun f => f.toPartialEquiv
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.containsKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Std.Internal.List.containsKey k l
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.asIdeal : {R : Type u_1} → [inst : CommSemiring R] → MaximalSpectrum R → Ideal R
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Submodule.mem_projectivization_iff_submodule_le : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s : Submodule K V) (x : Projectivization K V), x ∈ Submodule.projectivization s ↔ x.submodule ≤ s
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.M : Type → Type
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom =
    X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯
-- Mathlib.Algebra.Group.Units.Hom
/-- `MonoidHom.toHomUnits` as a `MulEquiv`.  -/
MonoidHom.toHomUnitsMulEquiv : {G : Type u_1} → {M : Type u_2} → [inst : Group G] → [inst_1 : CommMonoid M] → (G →* M) ≃* (G →* Mˣ)
-- Mathlib.Data.Set.Prod
Set.pi_eq_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι}, i ∈ s → t i = ∅ → s.pi t = ∅
-- Init.Tactics
/-- Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvTraceMacro : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.mk.inj : ∀ {α : Type u} {next next_1 : Option α}, { next := next } = { next := next_1 } → next = next_1
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `not_antisymmRel_of_gt`. -/
LT.lt.not_antisymmRel_symm : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → ¬AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.step.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  (var : σ) (stk : (k : K) → List (Γ k)), Turing.TM2.step M { l := none, var := var, stk := stk } = none
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- If `f` is a continuous bilinear map taking values in the space of continuous alternating maps,
then evaluation of the twice uncurried `f` on a tuple of vectors `v`
can be represented as a sum of

$$
f(v_i, v_j; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}, \dots, v_{n+1}) -
f(v_j, v_i; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}, \dots, v_{n+1})
$$

over all `(i j : Fin (n + 2))`, `i < j`, taken with appropriate signs.
Here $\hat{v_i}$ and $\hat{v_j}$ mean that these vectors are removed from the tuple.

We use pairs of `i j : Fin (n + 1)`, `i ≤ j`,
to encode pairs `(i.castSucc : Fin (n + 2), j.succ : Fin (n + 2))`,
so the power of `-1` is off by one compared to the informal texts.

In particular, if `f` is symmetric in the first two arguments,
then the resulting alternating map is zero,
see `alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric` below.
 -/
ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply : ∀ {𝕜 : 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 : ℕ}
  (f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v : Fin (n + 2) → E),
  (ContinuousAlternatingMap.alternatizeUncurryFin (ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F ∘SL f)) v =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.eval_iterate_derivative_eq_iff_of_bounded : ∀ {n : ℕ} {P : Polynomial ℝ} {k : ℕ},
  0 < k →
    k ≤ n →
      ∀ {x : ℝ},
        1 ≤ x →
          P.degree ≤ ↑n →
            (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
              (Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) =
                  Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ ↑n)) ↔
                P = Polynomial.Chebyshev.T ℝ ↑n)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_getD_default : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.get! a = m.getD a default
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_neg : ∀ (x : NNReal) (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_map : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {S₁ : Type u_5} {S₂ : Type u_6} [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : S₁ →+* S₂) (p : MvPowerSeries σ R),
  (MvPowerSeries.map g) ((MvPowerSeries.map f) p) = (MvPowerSeries.map (g.comp f)) p
-- Mathlib.Data.Bool.Basic
Bool.eq_false_of_not_eq_true : ∀ {b : Bool}, ¬b = true → b = false
-- Mathlib.RingTheory.Polynomial.DegreeLT
/-- An isomorphism between `R[X]_(m + n)` and `R[X]_m × R[X]_n` given by the fact that the bases are
both indexed by `Fin (m + n)`.  -/
Polynomial.degreeLT.addLinearEquiv : (R : Type u_1) →
  [inst : Semiring R] →
    (m n : ℕ) → ↥(Polynomial.degreeLT R (m + n)) ≃ₗ[R] ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsSelfAdjoint.norm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsSelfAdjoint a → IsSelfAdjoint b → a * b = 0 → ‖a - b‖ = max ‖a‖ ‖b‖
-- Mathlib.Order.CompleteLattice.Basic
Pi.infSet.eq_1 : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → InfSet (β i)], Pi.infSet = { sInf := fun s i => ⨅ f, ↑f i }