mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1
/-- The timestamp for the `Date` header.
 -/
Std.Http.Protocol.H1.Machine.instant : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Option Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) h
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_add_right_eq_map : ∀ {m n : ℕ}, (m<...m + 1 + n).toArray = Array.map (fun x => x + m + 1) (0...n).toArray
-- Mathlib.Algebra.Group.Action.Units
Units.coe_inv_smul : ∀ {M : Type u_6} {N : Type u_7} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulDistribMulAction M N] (m : M)
  (u : Nˣ), ↑(m • u)⁻¹ = m • ↑u⁻¹
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictFDerivAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getKey? k (Std.Internal.List.insertListConst l toInsert) = Std.Internal.List.getKey? k l
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasCokernel f]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.HasCokernel (G.map f)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurableCylinders.measurableSet : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)}
  (ht : t ∈ MeasureTheory.measurableCylinders α), MeasurableSet (MeasureTheory.measurableCylinders.set ht)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi : ∀ {θ : Real.Angle} {ψ : ℝ}, θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑Real.pi
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.closure_le_centralizer_centralizer : ∀ {M : Type u_1} [inst : AddSemigroup M] (s : Set M),
  AddSubsemigroup.closure s ≤ AddSubsemigroup.centralizer ↑(AddSubsemigroup.centralizer s)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- `d[s] f x` (scoped to the `Manifold` namespace) elaborates to `mvfderivWithin I J f s x`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termD[_]__» : Lean.ParserDescr
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.addMonoidHom_ext_iff : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] {N : AddSubgroup G} [nN : N.Normal]
  {f g : G ⧸ N →+ M}, f = g ↔ f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)
-- Mathlib.Algebra.Homology.Homotopy
dNext_eq_dFrom_fromNext : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι),
  (dNext i) f = CategoryTheory.CategoryStruct.comp (C.dFrom i) ((fromNext i) f)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hasForgetToCommAlgCat : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (CommBialgCat R) (CommAlgCat R)
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_eq_true_iff_exists_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulHashable α] [EquivBEq α]
  {p : α → β → Bool}, m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) m[a] = true
-- Init.Control.Lawful.Instances
StateT.run_map : ∀ {m : Type u → Type u_1} {α β σ : Type u} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ),
  (f <$> x).run s = (fun p => (f p.1, p.2)) <$> x.run s
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The proposition that the function preserves multiplication  -/
MulRingSeminorm.map_mul' : ∀ {R : Type u_2} [inst : NonAssocRing R] (self : MulRingSeminorm R) (x y : R),
  self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.forget_obj_of : ∀ {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 : CategoryTheory.Limits.PreservesFiniteColimits F],
  (CategoryTheory.RightExactFunctor.forget C D).obj (CategoryTheory.RightExactFunctor.of F) = F
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.id_tensorHom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X₁ X₂ : CategoryTheory.Dial C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
      (CategoryTheory.CategoryStruct.id X₂) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_2 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) (startPos endPos : s.Pos)
  (hps :
    searcher.IsPlausibleStep (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos)))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
            ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
          ⟨Std.IterStep.done, property⟩ →
        motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ =>
      h_1 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ =>
      h_2 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_2 searcher' startPos endPos hps ⋯
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_injective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Surjective ⇑f → Function.Injective (Submonoid.comap f)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toGeneralLinearGroup.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  SpecialLinearGroup.toGeneralLinearGroup =
    (LinearMap.GeneralLinearGroup.generalLinearEquiv R V).symm.toMonoidHom.comp SpecialLinearGroup.toLinearEquiv
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.BackwardRule.mk : Lean.Expr → Lean.Meta.Sym.Pattern → List ℕ → Lean.Meta.Sym.BackwardRule
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.vecMul_permMatrix : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] {v : n → R}
  [inst_2 : CommRing R], Matrix.vecMul v (Equiv.Perm.permMatrix R σ) = v ∘ ⇑(Equiv.symm σ)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.nfp_lt_ord : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}} {c : Ordinal.{u_1}},
  Cardinal.aleph0 < c.cof → (∀ i < c, f i < c) → ∀ {a : Ordinal.{u_1}}, a < c → Ordinal.nfp f a < c
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_move : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (T : Turing.Tape Γ) (d : Turing.Dir),
  Turing.Tape.map f (Turing.Tape.move d T) = Turing.Tape.move d (Turing.Tape.map f T)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_C : ∀ {R : Type u} [inst : Semiring R] {a : R}, Polynomial.derivative (Polynomial.C a) = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.mk.sizeOf_spec : ∀ (newConsts : Lean.VisibilityMap✝ (List Lean.AsyncConst✝))
  (replayKernel : Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment))
  (dyn : Dynamic),
  sizeOf { newConsts := newConsts, replayKernel := replayKernel, dyn := dyn } = 1 + sizeOf newConsts + sizeOf dyn
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_le_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (compare (t.minKeyD fallback) k).isLE = true
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_ofNat : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], ‖OfNat.ofNat n‖ = OfNat.ofNat n
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  {F : TopCat.Presheaf C X} {ι : Type v'} {U : ι → TopologicalSpace.Opens ↑X} {X_1 : C}
  {f f' : X_1 ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U},
  f = f' ↔
    ∀ (j : CategoryTheory.Discrete ι),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j) =
        CategoryTheory.CategoryStruct.comp f'
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j)
-- Mathlib.Data.Set.Prod
Set.empty_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β}, ∅ ×ˢ t = ∅
-- Lean.Meta.Hint
/-- Converts an array of diff actions into a Unicode string that visually depicts the diff.

Note that this function does not return the string that results from applying the diff to some
input; rather, it returns a string representation of the actions that the diff itself comprises,
such as `b̵a̵c̲h̲e̲e̲rs̲`.
 -/
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.mkDiffString : Array (Lean.Diff.Action × String) → String
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodalWeight.congr_simp : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (s s_1 : Finset ι),
  s = s_1 →
    ∀ (v v_1 : ι → F), v = v_1 → ∀ (i i_1 : ι), i = i_1 → Lagrange.nodalWeight s v i = Lagrange.nodalWeight s_1 v_1 i_1
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.Colimit.ι_desc_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasColimit F] (s : CategoryTheory.Limits.Cocone F) (j : J) (x : F.obj j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.desc F s))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
-- Lean.Data.Lsp.Extra
/-- `$/lean/rpc/release` client->server notification.

A notification to release remote references. Should be sent by the client when it no longer needs
`RpcRef`s it has previously received from the server. Not doing so is safe but will leak memory.  -/
Lean.Lsp.RpcReleaseParams : Type
-- Init.Data.Vector.Find
Vector.findFinIdx?_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, Vector.findFinIdx? p xs = none ↔ ∀ x ∈ xs, ¬p x = true
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {I : Ideal R},
  I.IsMaximal → I = IsLocalRing.maximalIdeal R
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_normal : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (K : Subgroup N) [hH : H.Normal]
  [hK : K.Normal], (H.prod K).Normal
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.match_1.eq_1 : ∀ (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) (x : Substring.Raw) (p : String.Pos.Raw)
  (h_1 : (x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p)
  (h_2 : (ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p),
  (match x, 0, p with
    | x, 0, p => h_1 x p
    | ss, i.succ, p => h_2 ss i p) =
    h_1 x p
-- Mathlib.Algebra.Group.Pi.Units
IsUnit.val_inv_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {x : (i : ι) → M i} (hx : IsUnit x) (i : ι),
  ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.latticeClosure_subset_closure : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α}, latticeClosure s ⊆ ↑(BooleanSubalgebra.closure s)
-- Mathlib.Data.PFun
PFun.coe_preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), (↑f).preimage s = f ⁻¹' s
-- Mathlib.Order.Minimal
/-- **Alias** of `Set.minimal_iff_forall_sdiff_singleton`. -/
Set.minimal_iff_forall_diff_singleton : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) → (Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x}))
-- Mathlib.Data.List.Forall2
List.rel_append : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.LiftFun (List.Forall₂ R) (Relator.LiftFun (List.Forall₂ R) (List.Forall₂ R)) (fun x1 x2 => x1 ++ x2)
    fun x1 x2 => x1 ++ x2
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, (t.getKey? a).isSome = true ↔ a ∈ t
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_dvd_false : ∀ {a b a' b' : ℤ}, Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → (b'.emod a' != 0) = true → ¬a ∣ b
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_one_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (j : ℕ) (hj : j + 1 < n + 1 + 1),
  CategoryTheory.ComposableArrows.Precomp.map F f 1 ⟨j + 1, hj⟩ ⋯ = F.map' 0 j ⋯ ⋯
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ω.eq_1 : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base),
  RootPairing.GeckConstruction.ω b = Matrix.fromBlocks 1 0 0 (Matrix.of fun i j => if i = -j then 1 else 0)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_iInf : ∀ {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : ι → Subalgebra R A), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.instIsCentralVAdd : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α], IsCentralVAdd M αᵃᵒᵖ
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → s ∈ nhds x → ContinuousAt f x
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_array_forRevM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m PUnit.{u + 1}) (xs : Array α)
  (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.forRevM (f x) xs start stop
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.homotopyEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (P Q : CategoryTheory.ProjectiveResolution X),
  P.homotopyEquiv Q =
    { hom := CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id X) P Q,
      inv := CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id X) Q P,
      homotopyHomInvId :=
        (CategoryTheory.ProjectiveResolution.liftCompHomotopy (CategoryTheory.CategoryStruct.id X)
                (CategoryTheory.CategoryStruct.id X) P Q P).symm.trans
          (⋯.mpr (CategoryTheory.ProjectiveResolution.liftIdHomotopy X P)),
      homotopyInvHomId :=
        (CategoryTheory.ProjectiveResolution.liftCompHomotopy (CategoryTheory.CategoryStruct.id X)
                (CategoryTheory.CategoryStruct.id X) Q P Q).symm.trans
          (⋯.mpr (CategoryTheory.ProjectiveResolution.liftIdHomotopy X Q)) }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_succ_eq_map : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] [inst_8 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerableLeast? α] {hi : α},
  (*...Std.PRange.succ hi).toArray = #[Std.PRange.UpwardEnumerable.least] ++ Array.map Std.PRange.succ (*...hi).toArray
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vaddAssocClass : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [inst_4 : VAddAssocClass S R M] (p : SubAddAction R M), VAddAssocClass S R ↥p
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapId_hom_app : ∀ (I : Type w₀) (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I),
  (CategoryTheory.Pi.comapId I C).hom.app X i = CategoryTheory.CategoryStruct.id X i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `card_le_card_add_left` for a more convenient but less general version for types with a
left-cancellative addition.  -/
Finset.card_le_card_add_left_of_injective : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {a : α},
  a ∈ s → IsAddLeftRegular a → t.card ≤ (s + t).card
-- Mathlib.Combinatorics.SetFamily.Compression.UV
Set.Sized.uvCompression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {u v : Finset α} {r : ℕ},
  u.card = v.card → Set.Sized r ↑𝒜 → Set.Sized r ↑(UV.compression u v 𝒜)
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ (a : ℝ) (n : ℕ),
      μ {x | ‖x‖ ≤ a} * μ {x | ProbabilityTheory.Fernique.normThreshold a (n + 1) < ‖x‖} ≤
        μ {x | ProbabilityTheory.Fernique.normThreshold a n < ‖x‖} ^ 2
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_omega0 : ∀ {a : Ordinal.{u_4}}, a < Ordinal.omega0 → a + Ordinal.omega0 = Ordinal.omega0
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- Any linearly ordered abelian group with zero that is locally finite embeds into `ℤᵐ⁰`.  -/
LocallyFiniteOrder.orderMonoidWithZeroHom : (G : Type u_3) →
  [inst : LinearOrderedCommGroupWithZero G] → [LocallyFiniteOrder Gˣ] → G →*₀o WithZero (Multiplicative ℤ)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.norm_map_of_mem_unitary : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {u : H →L[𝕜] H}, u ∈ unitary (H →L[𝕜] H) → ∀ (x : H), ‖u x‖ = ‖x‖
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_eq_aeval : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  MvPolynomial.rename f = MvPolynomial.aeval (MvPolynomial.X ∘ f)
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.lt_iff_lt : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S}, v.IsEquiv w → ∀ {x y : R}, v x < v y ↔ w x < w y
-- Lean.Elab.Quotation
/-- `C[$(e)]` ~> `let a := e; C[$a]`. Used in the implementation of antiquot splices.  -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.floatOutAntiquotTerms : Lean.Syntax → StateT (Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax) Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Data.EReal.Basic
EReal.rec_top : ∀ {motive : EReal → Sort u_1} (bot : motive ⊥) (coe : (a : ℝ) → motive ↑a) (top : motive ⊤),
  EReal.rec bot coe top ⊤ = top
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A right homology data for a short complex `S` induces a left homology data for `S.op`.  -/
CategoryTheory.ShortComplex.RightHomologyData.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → S.RightHomologyData → S.op.LeftHomologyData
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, orderOf x ∣ Fintype.card G