mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (x : E),
  (↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf') x).1 = f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} {len : ℕ}
  (x : aig.RefVec (len * w)) (h : 0 < len),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go x h =
    if hlt : 1 < len then
      have res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer aig { w := w, len := len, oldLayer := x, h := ⋯, hlen := h };
      Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go res.vec ⋯
    else
      have hcast := ⋯;
      { aig := aig, vec := hcast ▸ x }
-- Mathlib.CategoryTheory.Opposites
/-- The opposite of a fully faithful functor is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → F.FullyFaithful → F.op.FullyFaithful
-- Aesop.Search.Queue
Aesop.FIFOQueue.init : Aesop.FIFOQueue
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inter_mulSupport : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s : Set α),
  ∏ᶠ (i : α) (_ : i ∈ s ∩ Function.mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `AlexandrovDiscrete.locallyPathConnectedSpace`. -/
AlexandrovDiscrete.locPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [AlexandrovDiscrete X], LocallyPathConnectedSpace X
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert_snd_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).2.impl = Std.DTreeMap.Internal.Impl.insertₘ a b t htb
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The trivial continuous homomorphism.  -/
ContinuousMonoidHom.instOne : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → One (A →ₜ* B)
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_inj : ∀ {α : Type u} {l l' : List α}, l.cyclicPermutations = l'.cyclicPermutations ↔ l = l'
-- Mathlib.Tactic.Ring.Common
_private.Mathlib.Tactic.Ring.Common.0.Mathlib.Tactic.Ring.Common.instMonadLiftOptionOptionTOfPure_mathlib : {m : Type u_2 → Type u_3} → [Pure m] → MonadLift Option (OptionT m)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.app_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) =
    CategoryTheory.CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
-- Mathlib.Algebra.Group.NatPowAssoc
npow_add : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (k n : ℕ) (x : M),
  x ^ (k + n) = x ^ k * x ^ n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R),
  PresheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pushforwardId R) (PresheafOfModules.pushforward φ) ≪≫
      (PresheafOfModules.pushforward φ).leftUnitor
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.strictAnti_iff_Icc : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), StrictAnti ⇑f ↔ StrictAntiOn (⇑f) (Set.Icc l (l + a))
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If `v` and `w` are two real absolute values on a field `F`, then `v` and `w` are equivalent if
and only if there exists a positive real constant `c` such that for all `x : R`, `(f x)^c = g x`.
 -/
AbsoluteValue.isEquiv_iff_exists_rpow_eq : ∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ}, v.IsEquiv w ↔ ∃ c, 0 < c ∧ (fun x => v x ^ c) = ⇑w
-- Std.Time.Zoned.Database.TzIf
/-- Represents a leap second record, including the transition time and the correction applied.
 -/
Std.Time.TimeZone.TZif.LeapSecond : Type
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `(s : S)` is in the image of `f`, then `C s` lifts.  -/
Polynomial.C'_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {s : S},
  s ∈ Set.range ⇑f → Polynomial.C s ∈ Polynomial.lifts f
-- Mathlib.Data.Finset.Prod
Finset.product_sdiff_diag : ∀ {α : Type u_1} (s : Finset α) [inst : DecidableEq α], s ×ˢ s \ s.diag = s.offDiag
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDistribMulAction : {α : Type u_1} →
  {l : Filter α} →
    {M : Type u_5} →
      {N : Type u_6} →
        [inst : Monoid M] → [inst_1 : AddMonoid N] → [DistribMulAction M N] → DistribMulAction M (l.Germ N)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_ringHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], ↑(RingEquiv.refl R) = RingHom.id R
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.exists_map_eq_of_map_le' : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (self : EsakiaHom α β) ⦃a : α⦄ ⦃b : β⦄, self.toFun a ≤ b → ∃ c, a ≤ c ∧ self.toFun c = b
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopy'_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) (i j : ι),
  (Homotopy.nullHomotopy' h).hom i j = dite (c.Rel j i) (h i j) fun x => 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.snd f₃)
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_sub_add_cancel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [inst : ProbabilityTheory.IsSFiniteKernel κ] {f g : α → β → ENNReal},
  Measurable (Function.uncurry f) →
    Measurable (Function.uncurry g) →
      (∀ (a : α), g a ≤ᵐ[κ a] f a) → (κ.withDensity fun a x => f a x - g a x) + κ.withDensity g = κ.withDensity f
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_inv_natural_right_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)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map g))
        h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₂).inv h)
-- Lean.Meta.Coe
/-- Try coercions and monad lifts to make sure `e` has type `expectedType`.

If `expectedType` is of the form `n β`, we try monad lifts and other extensions.

Extensions for monads.

1. Try to unify `n` and `m`. If it succeeds, then we use
  ```
  coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
  ```
  `n` must be a `Monad` to use this one.

2. If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
  ```
  liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
  ```
  Note that `n` may not be a `Monad` in this case. This happens quite a bit in code such as
  ```
  def g (x : Nat) : IO Nat := do
    IO.println x
    pure x

  def f {m} [MonadLiftT IO m] : m Nat :=
    g 10

  ```

3. If there is a monad lift from `m` to `n` and a coercion from `α` to `β`, we use
  ```
  liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β
  ```

Note that approach 3 does not subsume 1 because it is only applicable if there is a coercion from `α` to `β` for all values in `α`.
This is not the case for example for `pure $ x > 0` when the expected type is `IO Bool`. The given type is `IO Prop`, and
we only have a coercion from decidable propositions.  Approach 1 works because it constructs the coercion `CoeT (m Prop) (pure $ x > 0) (m Bool)`
using the instance `pureCoeDepProp`.

Note that, approach 2 is more powerful than `tryCoe`.
Recall that type class resolution never assigns metavariables created by other modules.
Now, consider the following scenario
```lean
def g (x : Nat) : IO Nat := ...
deg h (x : Nat) : StateT Nat IO Nat := do
v ← g x;
IO.Println v;
...
```
Let's assume there is no other occurrence of `v` in `h`.
Thus, we have that the expected of `g x` is `StateT Nat IO ?α`,
and the given type is `IO Nat`. So, even if we add a coercion.
```
instance {α m n} [MonadLiftT m n] {α} : Coe (m α) (n α) := ...
```
It is not applicable because TC would have to assign `?α := Nat`.
On the other hand, TC can easily solve `[MonadLiftT IO (StateT Nat IO)]`
since this goal does not contain any metavariables. And then, we
convert `g x` into `liftM $ g x`.
 -/
Lean.Meta.coerceMonadLift? : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Environment
Lean.PersistentEnvExtension.name : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → Lean.Name
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_of_seq : ∀ {α : Type u_1} {f : Filter α}, (∃ x, f = ⨅ i, Filter.principal (x i)) → f.IsCountablyGenerated
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- The cover associated to an affine cover.  -/
AlgebraicGeometry.Scheme.AffineCover.cover : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.AffineCover P X → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
-- Mathlib.Data.List.Permutation
List.perm_of_mem_permutations : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ ∈ l₂.permutations → l₁.Perm l₂
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Increase the universe level of a profunctor by one. This enables dot notation `P.ulift1`,
which is not possible with `Profunctor.ulift`.  -/
CategoryTheory.Profunctor.ulift1 : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D → CategoryTheory.Profunctor.{w + 1, v₁, v₂, u₁, u₂} C D
-- Batteries.Data.BinomialHeap.Basic
/-- The children of the minimum element.  -/
Batteries.BinomialHeap.Imp.FindMin.node : {α : Type u_1} → Batteries.BinomialHeap.Imp.FindMin α → Batteries.BinomialHeap.Imp.HeapNode α
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_7 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)) (k : ℕ)
  (a : Lean.Grind.Linarith.Expr),
  x = Lean.Grind.Linarith.Expr.natMul k a →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_7 k a
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instLawfulBEq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] [inst_1 : (k : α) → BEq (β k)]
  [∀ (k : α), LawfulBEq (β k)], LawfulBEq (Std.ExtDHashMap α β)
-- Mathlib.AlgebraicGeometry.Spec
/-- Spec, as a contravariant functor from commutative rings to locally ringed spaces.
 -/
AlgebraicGeometry.Spec.toLocallyRingedSpace : CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function taking values in a complete lattice
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.  -/
Monotone.iSup_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  [OrderTop γ] {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.ball_mem_nhds : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, 0 < r → Euclidean.ball x r ∈ nhds x
-- Init.Data.List.Scan.Lemmas
List.scanlM_eq_scanrM_reverse : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [inst : Monad m] {f : β → α → m β},
  List.scanlM f init as = List.reverse <$> List.scanrM (flip f) init as.reverse
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α}
  (hl : Std.Internal.List.DistinctKeys l)
  {h : Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true},
  Std.Internal.List.getValue k (List.filter (fun p => f p.fst p.snd) l) h = Std.Internal.List.getValue k l ⋯
-- Mathlib.Order.OrderDual
OrderDual.toDual_inj : ∀ {α : Type u_1} {a b : α}, OrderDual.toDual a = OrderDual.toDual b ↔ a = b
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.compare_val : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Ord α] (a b : AddUnits α), compare ↑a ↑b = compare a b
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
factorization.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] (n : α), factorization n = Multiset.toFinsupp (UniqueFactorizationMonoid.normalizedFactors n)
-- Batteries.Data.String.Lemmas
String.atEnd_of_valid : ∀ (cs cs' : List Char),
  String.Pos.Raw.atEnd (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } = true ↔ cs' = []
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.ord_preAleph : ∀ (o : Ordinal.{u_1}), (Cardinal.preAleph o).ord = Ordinal.preOmega o
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_neg_mul_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A} (x : ℝ),
  autoParam (IsStrictlyPositive a) CFC.rpow_neg_mul_rpow._auto_1 → a ^ (-x) * a ^ x = 1
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- The natural map from `SL(n, R)` to `PGL(n, R)` by composing the maps from `SL` to `GL` and the
quotient map from `GL` to `PGL`.  -/
Matrix.SpecialLinearGroup.toPGL : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing R] → Matrix.SpecialLinearGroup n R →* Matrix.ProjGenLinGroup n R
-- Lean.LocalContext
/-- Set the kind of the given fvar.
 -/
Lean.LocalContext.setKind : Lean.LocalContext → Lean.FVarId → Lean.LocalDeclKind → Lean.LocalContext
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax'_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)],
  (CategoryTheory.Pseudofunctor.mkOfLax' F).toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `⁅H, F⁆`-relations.  -/
CartanMatrix.Relations.HF : (R : Type u) → {B : Type v} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.instAddHomFunctor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive D] → {F G : CategoryTheory.Functor C D} → Add (F ⟶ G)
-- Lean.Elab.DocString
Lean.Doc.instToMessageDataDocArg : Lean.ToMessageData Lean.Doc.DocArg
-- Init.Core
Decidable.byContradiction : ∀ {p : Prop} [dec : Decidable p], (¬p → False) → p
-- Init.Data.BitVec.Lemmas
/-- `rotateLeft` is defined in terms of left and right shifts.  -/
BitVec.rotateLeft_def : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, x.rotateLeft r = x <<< (r % w) ||| x >>> (w - r % w)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsert_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.containsThenInsert k v).2 = m.insert k v
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_orElse_ExceptT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (x : ExceptT ε m α) (h : Unit → ExceptT ε m α),
  Lean.Order.PartialOrder.rel
    (Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun x => Std.Internal.Do.wp (h ()) post epost) epost.tail))
    (Std.Internal.Do.wp (OrElse.orElse x h) post epost)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.mk.inj : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1} {inner inner_1 : Std.ExtTreeMap α Unit cmp},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instIsSeparable : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] {T : Type u_3}
  [inst_3 : Field T] (v : AbsoluteValue R S) [inst_4 : Algebra R T] [Algebra.IsSeparable R T],
  Algebra.IsSeparable (WithAbs v) T
-- Mathlib.Data.Nat.Factorization.PrimePow
/-- The canonical equivalence between pairs `(p, k)` with `p` a prime and `k : ℕ`
and the set of prime powers given by `(p, k) ↦ p^(k+1)`.  -/
Nat.Primes.prodNatEquiv : Nat.Primes × ℕ ≃ { n // IsPrimePow n }
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_5.eq_3 : ∀ (motive : ℕ → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → Sort u_1) (n : ℕ) (p : Bool)
  (g : Lean.MVarId) (goals : List Lean.MVarId) (stk : List (List Lean.MVarId)) (acc : Array Lean.MVarId)
  (h_1 : (x : ℕ) → (p : Bool) → (acc : Array Lean.MVarId) → motive x p [] [] acc)
  (h_2 :
    (n : ℕ) →
      (p : Bool) →
        (goals : List Lean.MVarId) →
          (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p [] (goals :: stk) acc)
  (h_3 :
    (n : ℕ) →
      (p : Bool) →
        (g : Lean.MVarId) →
          (goals : List Lean.MVarId) →
            (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p (g :: goals) stk acc),
  (match n, p, g :: goals, stk, acc with
    | x, p, [], [], acc => h_1 x p acc
    | n, p, [], goals :: stk, acc => h_2 n p goals stk acc
    | n, p, g :: goals, stk, acc => h_3 n p g goals stk acc) =
    h_3 n p g goals stk acc
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_eq_of_norm_add_lt_left : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]}, ‖z1 + z2‖ < ‖z1‖ → ‖z1‖ = ‖z2‖
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.mk : Lean.Lsp.WorkDoneProgressParams →
  Lean.Lsp.PartialResultParams → Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.DocumentColorParams
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (t : Set Y) (h : ⇑e '' s = t), (e.toPartialHomeomorphOfImageEq s t h).source = s
-- Mathlib.Analysis.Complex.Circle
Real.probChar_ne_one : Real.probChar ≠ 1