mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) (φ : CategoryTheory.Aut A),
  (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a) φ =
    (CategoryTheory.ConcreteCategory.hom (F.map φ.hom)) a
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- The **Lefschetz principle**. A first-order sentence is modeled by the theory
of algebraically closed fields of characteristic zero if and only if it is modeled by
the theory of algebraically closed fields of characteristic `p` for infinitely many `p`.  -/
FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize : ∀ {φ : FirstOrder.Language.ring.Sentence},
  FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Infinite
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.head_coeffList : ∀ {R : Type u_1} [inst : Semiring R] (P : Polynomial R) (hP : P.coeffList ≠ []), P.coeffList.head hP = P.leadingCoeff
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearMap.linearIndepOn_iff_of_injOn : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {M' : Type u_5} {v : ι → M} [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'),
  Set.InjOn ⇑f ↑(Submodule.span R (v '' s)) → (LinearIndepOn R (⇑f ∘ v) s ↔ LinearIndepOn R v s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.constructor.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.constructor = 1
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.subset_of_mem : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y ∈ x → y ⊆ x
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.ext_of_ring_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {f g : R →ₗc[R] A}, f = g ↔ f 1 = g 1
-- Mathlib.Algebra.Group.Graph
MonoidHom.mgraph.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] (f : G →* H),
  f.mgraph = { carrier := {x | f x.1 = x.2}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformInv.eq_1 : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)),
  Real.Lp.fourierTransformInv f = (Real.Lp.fourierTransform f).compContinuous (-ContinuousMap.id V)
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- A parametrized family of permutations, induced by reflections. This corresponds to the
classical requirement that the symmetry attached to each root (later defined in
`RootPairing.reflection`) leave the whole set of roots stable: as explained above, we
formalize this stability by fixing the image of the roots through each reflection (whence the
permutation); and similarly for coroots.  -/
RootPairing.reflectionPerm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → ι ≃ ι
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.inv.match_1.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} [inst : (i : ι) → Group (G i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord G x x_1 → Sort u_3) (x : ι) (x_1 : G x) (h : x_1 ≠ 1)
  (h_1 : (x : ι) → (x_2 : G x) → (h : x_2 ≠ 1) → motive x x (Monoid.CoprodI.NeWord.singleton x_2 h))
  (h_2 :
    (x x_2 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord G x j) →
        (h : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord G k x_2) → motive x x_2 (w₁.append h w₂)),
  (match x, x, Monoid.CoprodI.NeWord.singleton x_1 h with
    | x, .(x), Monoid.CoprodI.NeWord.singleton x_2 h => h_1 x x_2 h
    | x, x_2, w₁.append h w₂ => h_2 x x_2 j k w₁ h w₂) =
    h_1 x x_1 h
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool} {k : α},
  (Std.ExtHashMap.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.NumberTheory.Height.Basic
/-- **Alias** of `Height.AdmissibleAbsValues.hasFiniteMulSupport`.

---

Only finitely many (nonarchimedean) absolute values are `≠ 1` for any nonzero `x : K`.  -/
Height.AdmissibleAbsValues.mulSupport_finite : ∀ {K : Type u_1} {inst : Field K} [self : Height.AdmissibleAbsValues K] {x : K},
  x ≠ 0 → Function.HasFiniteMulSupport fun v => ↑v x
-- Mathlib.Computability.Encoding
/-- A binary `Encoding` of `ℕ` in `Γ'`.  -/
Computability.encodingNatΓ' : Computability.Encoding ℕ Computability.Γ'
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.IsSymmetric 0
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_mulVec : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n'] (v : n' → α)
  (A : Fin m → n' → α) (w : n' → α),
  (Matrix.of (Matrix.vecCons v A)).mulVec w = Matrix.vecCons (v ⬝ᵥ w) ((Matrix.of A).mulVec w)
-- Mathlib.Order.PiLex
Pi.toLex_monotone : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι],
  Monotone ⇑toLex
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.smul_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r : ↑(R.obj.obj X)) (m m' : ↑(A.obj.obj X)),
  PresheafOfModules.Sheafify.smul α φ r (m + m') =
    PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r m'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey! k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fmod_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → (a * b).fmod (a * c) = a * b.fmod c
-- Mathlib.Data.Vector.Basic
List.Vector.tail_val : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ), ↑v.tail = (↑v).tail
-- Mathlib.CategoryTheory.Sites.Pullback
/-- The pullback functor `Sheaf J A ⥤ Sheaf K A` associated to a functor `G : C ⥤ D` in the
same direction as `G`.  -/
CategoryTheory.Functor.sheafPullback : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type u₁) →
            [inst_2 : CategoryTheory.Category.{v₁, u₁} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsContinuous J K] →
                    [(G.sheafPushforwardContinuous A J K).IsRightAdjoint] →
                      CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_congr : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ},
  X =ᵐ[μ] Y → ProbabilityTheory.mgf X μ t = ProbabilityTheory.mgf Y μ t
-- Mathlib.Order.KrullDimension
Order.coheight_add_one_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → Order.coheight a + 1 ≤ Order.coheight b
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instIsScalarTower : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : (i : ι) → SMul R (G i)] [∀ (i : ι), IsScalarTower R (G i) (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)],
  IsScalarTower R (DirectLimit G f) (DirectLimit G f)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {g h : Z ⟶ Y},
  CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f ↔ g = h
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.mapIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z),
  (CategoryTheory.Limits.biprod.mapIso f g).inv = CategoryTheory.Limits.biprod.map f.inv g.inv
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.inv_zero_eqC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α c] (b : ℤ),
  (b % ↑c == 0) = true → (Lean.Grind.CommRing.denoteInt b)⁻¹ = 0
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `i, j, k`th short complex associated to the alternating constant complex on `φ, ψ : A ⟶ A`
is `A --φ--> A --ψ--> A` when `i ~ j, j ~ k` and `j` is even.  -/
HomologicalComplex.alternatingConstScIsoOdd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) →
            (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) →
              {c : ComplexShape ℕ} →
                [inst_2 : DecidableRel c.Rel] →
                  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) →
                    {i j k : ℕ} →
                      c.Rel i j →
                        c.Rel j k →
                          Odd j →
                            ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k ≅
                              { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd })
-- Mathlib.Topology.Category.TopCommRingCat
/-- This prevents `TopCommRingCat.of R` being printed as `{ α := R, ... }` by
`delabStructureInstance`.  -/
TopCommRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.coe_cliqueFinset : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] (n : ℕ),
  ↑(G.cliqueFinset n) = G.cliqueSet n
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMapM_eq_toIter_filterMapM_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [inst_2 : MonadAttach m] {f : β → m (Option γ)}, Std.Iter.filterMapM f it = Std.IterM.filterMapM f it.toIterM
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulUpwardEnumerableLENat : Std.PRange.LawfulUpwardEnumerableLE ℕ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The most general lemma stating that `x ↦ fderivWithin 𝕜 (f x) t (g x)` is `C^n`
at a point within a set.
To show that `x ↦ D_yf(x,y)g(x)` (taken within `t`) is `C^m` at `x₀` within `s`, we require that
* `f` is `C^n` at `(x₀, g(x₀))` within `(s ∪ {x₀}) × t` for `n ≥ m+1`.
* `g` is `C^m` at `x₀` within `s`;
* Derivatives are unique at `g(x)` within `t` for `x` sufficiently close to `x₀` within `s ∪ {x₀}`;
* `t` is a neighborhood of `g(x₀)` within `g '' s`;  -/
ContDiffWithinAt.fderivWithin'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x₀ : E} {m n : WithTop ℕ∞} {f : E → F → G}
  {g : E → F} {t : Set F},
  ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀) →
    ContDiffWithinAt 𝕜 m g s x₀ →
      (∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x)) →
        m + 1 ≤ n → t ∈ nhdsWithin (g x₀) (g '' s) → ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.map_singletonSubgraph : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V},
  SimpleGraph.Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.instBEqDirection : BEq Std.Http.Protocol.H1.Direction
-- Mathlib.Data.FunLike.Group
FunLike.addLeftCancelSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F]
  [inst_2 : AddLeftCancelSemigroup β] [inst_3 : IsAddApply F α β],
  FunLike.addLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup (fun f => ⇑f) ⋯ ⋯
-- Mathlib.Tactic.Choose
/-- Combine two statuses, keeping a success from either side
or merging the failures.  -/
Mathlib.Tactic.Choose.ElimStatus.merge : Mathlib.Tactic.Choose.ElimStatus → Mathlib.Tactic.Choose.ElimStatus → Mathlib.Tactic.Choose.ElimStatus
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.ind : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), AffineIndependent k ⇑b
-- Std.Internal.Parsec.ByteArray
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.skipBytes.go : ByteArray → ℕ → ByteArray.Iterator → Std.Internal.Parsec.ParseResult Unit ByteArray.Iterator
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.IsFiniteType.mk : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {p : M.LocalGeneratorsData},
  autoParam (∀ (i : p.I), (p.generators i).IsFiniteType)
      SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType._autoParam →
    p.IsFiniteType
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `AffineIsometry.intrinsicClosure_image`. -/
AffineIsometry.image_intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P), intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.map f₁ f₂) f₃)
      (CategoryTheory.Limits.coprod.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X₁ X₂ X₃).hom
      (CategoryTheory.Limits.coprod.map f₁ (CategoryTheory.Limits.coprod.map f₂ f₃))
-- Mathlib.Analysis.Complex.Circle
Circle.starRingEnd_addChar : ∀ {e : AddChar ℝ Circle} (x : ℝ), (starRingEnd ℂ) ↑(e x) = ↑(e (-x))
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero : ∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  (f : Module.End R M), ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (Polynomial.aeval f) p = 0
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.inl_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  Monotone ⇑(MonoidHom.inl α β)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.associator_naturality : ∀ {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂)
  (f₃ : X₃.Hom Y₃),
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    (((f₁.tensor f₂).tensor f₃).comp (CategoryTheory.FreeMonoidalCategory.Hom.α_hom Y₁ Y₂ Y₃))
    ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X₁ X₂ X₃).comp (f₁.tensor (f₂.tensor f₃)))
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_apply_lt : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0] (n : ℕ)
  (hn : n < l.length), l.toFinsupp n = l[n]
-- Mathlib.Topology.DenseEmbedding
Dense.extend_unique : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T2Space β] {g : α → β} (hs : Dense s), (∀ (x : ↑s), g ↑x = f x) → Continuous g → hs.extend f = g
-- Mathlib.Order.Lattice
inf_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ b = b ⊓ a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.ofSeq_surjective : Function.Surjective Hyperreal.ofSeq
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Iio x) x ≤ derivWithin f (Set.Ioi x) x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLECancellable_of_ne_top : ∀ {α : Type u} [inst : Add α] {x : WithTop α} [inst_1 : LE α] [AddLeftReflectLE α], x ≠ ⊤ → AddLECancellable x
-- Mathlib.Algebra.Homology.Localization
/-- The localizer morphism which expresses that `F.mapHomologicalComplex c` preserves
quasi-isomorphisms.  -/
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism : {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] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : F.Additive] →
                        [F.PreservesHomology] →
                          CategoryTheory.LocalizerMorphism (HomologicalComplex.quasiIso C c)
                            (HomologicalComplex.quasiIso D c)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.mk.inj : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} {inst : NormedField 𝕜}
  {inst_1 : SeminormedAddCommGroup V} {inst_2 : NormedSpace 𝕜 V} {inst_3 : PseudoMetricSpace P}
  {inst_4 : NormedAddTorsor V P} {inst_5 : SeminormedAddCommGroup V₂} {inst_6 : NormedSpace 𝕜 V₂}
  {inst_7 : PseudoMetricSpace P₂} {inst_8 : NormedAddTorsor V₂ P₂} {toAffineEquiv : P ≃ᵃ[𝕜] P₂}
  {norm_map : ∀ (x : V), ‖toAffineEquiv.linear x‖ = ‖x‖} {toAffineEquiv_1 : P ≃ᵃ[𝕜] P₂}
  {norm_map_1 : ∀ (x : V), ‖toAffineEquiv_1.linear x‖ = ‖x‖},
  { toAffineEquiv := toAffineEquiv, norm_map := norm_map } =
      { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 } →
    toAffineEquiv = toAffineEquiv_1
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.monoidObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J MonCat) → (j : J) → Monoid ↑(F.obj j)
-- Aesop.Script.Step
Aesop.Script.Step.tactic : Aesop.Script.Step → Aesop.Script.Tactic
-- Mathlib.Topology.UniformSpace.AbsoluteValue
AbsoluteValue.hasBasis_uniformity : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜] {R : Type u_2}
  [inst_3 : CommRing R] (abv : AbsoluteValue R 𝕜),
  (uniformity R).HasBasis (fun x => 0 < x) fun ε => {p | abv (p.2 - p.1) < ε}
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.TreeMap.Raw.maxKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Option α
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if type of `t` is definitionally equal to `α`
 -/
Lean.Meta.Grind.hasType : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.RelClasses
isTrans_lt : ∀ {α : Type u} [inst : Preorder α], IsTrans α LT.lt
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOver_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X A : C), ((CategoryTheory.toOver X).obj A).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd A X
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedAddCancelMonoid` under a strictly monotone map.  -/
StrictMono.isOrderedAddCancelMonoid : ∀ {α : Type u} {β : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] (f : β → α),
  StrictMono f → (∀ (x y : β), f (x + y) = f x + f y) → IsOrderedCancelAddMonoid β
-- Init.GrindInstances.Ring.UInt
UInt8.intCast_neg : ∀ (x : ℤ), ↑(-x) = -↑x
-- Mathlib.Order.SetAccumulate
Set.accumulate_succ : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), Set.accumulate u (n + 1) = Set.accumulate u n ∪ u (n + 1)
-- Init.Prelude
instDecidableEqFin : (n : ℕ) → DecidableEq (Fin n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_two_pi_mul_I : Complex.exp (2 * ↑Real.pi * Complex.I) = 1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instZero.eq_1 : ∀ {α : Type u}, FreeAddGroup.instZero = { zero := FreeAddGroup.mk [] }
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.left_hom_inv_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (e : X ⟶ Y) [inst_3 : CategoryTheory.IsIso e],
  CategoryTheory.CategoryStruct.comp (L.map e.left)
      (CategoryTheory.CategoryStruct.comp Y.hom (R.map (CategoryTheory.inv e.right))) =
    X.hom
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedDivisionRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'},
  MDiffAt[s] p z → p z ≠ 0 → MDiffAt[s] p⁻¹ z