mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The complex hyperbolic sine function is everywhere differentiable, with the derivative
`cosh x`.  -/
Complex.hasDerivAt_sinh : ∀ (x : ℂ), HasDerivAt Complex.sinh (Complex.cosh x) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k fallback =
      fallback
-- Mathlib.Order.Directed
/-- **Alias** of the forward direction of `directedOn_iff_directed`. -/
DirectedOn.directed_val : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, DirectedOn r s → Directed r Subtype.val
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α),
  σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) σ.cycleFactorsFinset.val
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero_isoAdd'_ : ∀ {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} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)),
  CategoryTheory.Functor.CommShift.isoAdd' ⋯ (CategoryTheory.Functor.CommShift.isoZero F A) e = e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.Normal.mono : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {G H : C} {inst_2 : CategoryTheory.AddGrpObj G} {inst_3 : CategoryTheory.AddGrpObj H} {φ : H ⟶ G}
  [self : CategoryTheory.IsAddMonHom.Normal φ], CategoryTheory.Mono φ
-- Mathlib.Order.Interval.Set.Infinite
Set.Ici_infinite : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a : α), (Set.Ici a).Infinite
-- Mathlib.Algebra.Polynomial.OfFn
/-- If `n ≤ i` the `i`-th coefficient of `ofFn n v` is `0`.  -/
Polynomial.ofFn_coeff_eq_zero_of_ge : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n i : ℕ} (v : Fin n → R),
  n ≤ i → ((Polynomial.ofFn n) v).coeff i = 0
-- Mathlib.RingTheory.Polynomial.ContentIdeal
/-- If the coefficients of `p` generate the whole ring, then `p` is primitive.  -/
Polynomial.isPrimitive_of_contentIdeal_eq_top : ∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R}, p.contentIdeal = ⊤ → p.IsPrimitive
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.isOpenMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), IsOpenMap ⇑e
-- Mathlib.Data.Finset.NAry
Finset.inf'_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeInf δ] (g : γ → δ) (h : (Finset.image₂ f s t).Nonempty),
  (Finset.image₂ f s t).inf' h g = t.inf' ⋯ fun y => s.inf' ⋯ fun x => g (f x y)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.comp_of_injective : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {β : Type u_3} {f : β → M} {g : α → β},
  Function.Injective g → Function.HasFiniteSupport f → Function.HasFiniteSupport (f ∘ g)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_toAddSubgroup : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M),
  (Submodule.map f p).toAddSubgroup = AddSubgroup.map (↑f) p.toAddSubgroup
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.eq_2 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R 1 = Polynomial.X
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.cofanMapObj.eq_1 : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] (j : J),
  X.cofanMapObj p j = CategoryTheory.GradedObject.CofanMapObjFun.mk X p j (X.mapObj p j) fun i hi => X.ιMapObj p i j hi
-- Mathlib.Combinatorics.Graph.Basic
/-- `edgeSet` can be determined using `IsLink`, so the graph constructed from `G.vertexSet` and
`G.IsLink` using any value for `edgeSet` is equal to `G` itself.  -/
Graph.mk_eq_self : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {E : Set β} (hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y),
  { vertexSet := G.vertexSet, IsLink := G.IsLink, edgeSet := E, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ } =
    G
-- Mathlib.Data.Finsupp.Basic
/-- Given `f : α → β` and `v : α →₀ M`, `mapDomain f v : β →₀ M`
is the finitely supported function whose value at `a : β` is the sum
of `v x` over all `x` such that `f x = a`.  -/
Finsupp.mapDomain : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : AddCommMonoid M] → (α → β) → (α →₀ M) → β →₀ M
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The opposite of a pre-path object is a precylinder object.  -/
HomotopicalAlgebra.PrepathObject.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} → HomotopicalAlgebra.PrepathObject A → HomotopicalAlgebra.Precylinder (Opposite.op A)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddMonCat fun x1 x2 => ↑x1 →+ ↑x2
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.step.inj : ∀ {cls : Lean.Name} {decls : Array Lean.IR.Decl} {cls_1 : Lean.Name} {decls_1 : Array Lean.IR.Decl},
  Lean.IR.LogEntry.step cls decls = Lean.IR.LogEntry.step cls_1 decls_1 → cls = cls_1 ∧ decls = decls_1
-- Mathlib.Data.Finset.Sups
Finset.diffs_union_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s₁ s₂ t : Finset α},
  (s₁ ∪ s₂).diffs t = s₁.diffs t ∪ s₂.diffs t
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β), (WithZero.map' f) 0 = 0
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.infty_mem_opensOfCompl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} (h₁ : IsClosed s) (h₂ : IsCompact s),
  OnePoint.infty ∈ OnePoint.opensOfCompl s h₁ h₂
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.conjugator.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (l : List (α × Bool)),
  FreeGroup.reduceCyclically.conjugator l =
    List.bidirectionalRec [] (fun x => []) (fun a x b rCC => if b.1 = a.1 ∧ (!b.2) = a.2 then a :: rCC else []) l
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_nil : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.wordProd [] = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.erase_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- like `coe_le_one`, but with the inequality in `Ioc (0:R) 1`.  -/
Set.Ioc.le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {t : ↑(Set.Ioc 0 1)},
  t ≤ 1
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.instStrongNormalizationMonoid : {R : Type u} →
  [inst : CommRing R] → [NoZeroDivisors R] → [StrongNormalizationMonoid R] → StrongNormalizationMonoid (Polynomial R)
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context : Type
-- Mathlib.Data.Finset.Erase
Finset.erase_subset_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s t : Finset α}, s ⊆ t → s.erase a ⊆ t.erase a
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.intro : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} (x : F.B a → PFunctor.Approx.CofixA F n)
  (x' : F.B a → PFunctor.Approx.CofixA F (n + 1)),
  (∀ (i : F.B a), PFunctor.Approx.Agree (x i) (x' i)) →
    PFunctor.Approx.Agree (PFunctor.Approx.CofixA.intro a x) (PFunctor.Approx.CofixA.intro a x')
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.elimType : Lean.Meta.ElimInfo → Lean.Expr
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ico_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c < a → c ∉ Set.Ico a b
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_congr_ae : ∀ {α : 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 : α), f a =ᵐ[κ a] g a) → κ.withDensity f = κ.withDensity g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) ↔ k ∈ t ∨ l.contains k = true
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_eq_cancelAux : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) →
    Nat.Internal.Linear.Poly.denote_eq ctx (Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)
-- Mathlib.Data.Semiquot
/-- A member of `Semiquot α` is classically a nonempty `Set α`,
and in the VM is represented by an element of `α`; the relation
between these is that the VM element is required to be a member
of the set `s`. The specific element of `s` that the VM computes
is hidden by a quotient construction, allowing for the representation
of nondeterministic functions.  -/
Semiquot : Type u_1 → Type u_1
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Array α → Sort u_2) (x x_1 : ℕ) (x_2 : Array α)
  (h_1 : (x x_3 : ℕ) → (x_4 : Array α) → motive [] x x_3 x_4)
  (h_2 : (head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc),
  (match [], x, x_1, x_2 with
    | [], x, x_3, x_4 => h_1 x x_3 x_4
    | head :: tail, 0, 0, x => h_2 head tail x
    | a :: xs, 0, i.succ, acc => h_3 a xs i acc
    | a :: xs, i.succ, 0, acc => h_4 a xs i acc
    | a :: xs, i.succ, j.succ, acc => h_5 a xs i j acc) =
    h_1 x x_1 x_2
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.originalTop_le : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞},
  TestFunction.originalTop Ω F n ≤ TestFunction.topologicalSpace Ω F n
-- Mathlib.CategoryTheory.Subobject.Basic
/-- The morphism in `C` from the arbitrarily chosen underlying object to the ambient object.
 -/
CategoryTheory.Subobject.arrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (Y : CategoryTheory.Subobject X) → CategoryTheory.Subobject.underlying.obj Y ⟶ X
-- Mathlib.Topology.Order
/-- The ordering on topologies on the type `α`. `t ≤ s` if every set open in `s` is also open in `t`
(`t` is finer than `s`).  -/
TopologicalSpace.instPartialOrder : {α : Type u} → PartialOrder (TopologicalSpace α)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_map : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {y : B},
  y ∈ Subalgebra.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.toIso_inv_ι_assoc : ∀ (X : AlgebraicGeometry.Scheme) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.topIso.inv (CategoryTheory.CategoryStruct.comp ⊤.ι h) = h
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The map sending the wreath product `D ≀ᵣ Q` to its representation as a permutation of `Λ × Q`
given `D`-set `Λ`.  -/
RegularWreathProduct.toPerm : (D : Type u_1) →
  (Q : Type u_2) →
    [inst : Group D] → [inst_1 : Group Q] → (Λ : Type u_3) → [MulAction D Λ] → D ≀ᵣ Q →* Equiv.Perm (Λ × Q)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (base : 𝒮) → ↑(F.obj { as := Opposite.op base }) → F.CoGrothendieck
-- Aesop.BuiltinRules.Assumption
_private.Aesop.BuiltinRules.Assumption.0.Aesop.BuiltinRules.assumption.tryHyp : Lean.MVarId → Lean.FVarId → Lean.Meta.TransparencyMode → Aesop.BaseM (Option (Aesop.RuleApplication × Bool))
-- Mathlib.LinearAlgebra.Dimension.Free
LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one : ∀ {R : Type u_2} [inst : CommSemiring R] [StrongRankCondition R] {M : Type u_3} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Module.Free R M], Module.finrank R M = 1 → ∀ (u : M →ₗ[R] M), ∃! c, u = c • LinearMap.id
-- Mathlib.RepresentationTheory.Basic
/-- **Alias** of `Representation.coeff_ofMulAction`. -/
Representation.ofMulAction_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] {H : Type u_4} [inst_2 : MulAction G H] (g : G)
  (f : MonoidAlgebra k H) (h : H), (((Representation.ofMulAction k G H) g) f).coeff h = f.coeff (g⁻¹ • h)
-- Lean.ToExpr
Lean.instToExprOptionOfToLevel : {α : Type u} → [Lean.ToLevel] → [Lean.ToExpr α] → Lean.ToExpr (Option α)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_4 : ∀ (coeff : ℤ) (a b : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff (a.sub b) =
    Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) b
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Set.Finite.multipliable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {s : Set β}, s.Finite → (Multipliable (f ∘ Subtype.val) ↔ Multipliable f)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrict_eq_zero_iff`. -/
AddMonoidHom.restrict_eq_zero_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] {f : M →+ N}
  [inst_2 : SetLike S M] [inst_3 : AddSubmonoidClass S M] {s : S}, f.domRestrict s = 0 ↔ ∀ x ∈ s, f x = 0
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.upsert.insertEmpty : {α : Type} → String → (Option α → α) → ℕ → Lean.Data.Trie α
-- Mathlib.Algebra.Exact.Sequence
/-- The Euler characteristic of a finite exact sequence is zero.  -/
Module.sum_neg_one_pow_finrank_eq_zero_of_exact : ∀ {k : Type u_1} [inst : DivisionRing k] {n : ℕ} (V : Fin (n + 2) → Type u_2)
  [inst_1 : (i : Fin (n + 2)) → AddCommGroup (V i)] [inst_2 : (i : Fin (n + 2)) → Module k (V i)]
  [∀ (i : Fin (n + 2)), FiniteDimensional k (V i)] (f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ),
  Function.Injective ⇑(f 0) →
    (∀ (i : Fin n), Function.Exact ⇑(f i.castSucc) ⇑(f i.succ)) →
      Function.Surjective ⇑(f (Fin.last n)) → ∑ i, (-1) ^ ↑i * ↑(Module.finrank k (V i)) = 0
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {J : Type u_1} (F : J → C)
  [inst_3 : CategoryTheory.Limits.HasBiproduct F], P (⨁ F) → ∀ (j : J), P (F j)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.proj` as an isometry, when all but one quadratic form is zero.  -/
QuadraticMap.Isometry.proj : {ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : (i : ι) → Module R (Mᵢ i)] →
                [inst_4 : Module R P] →
                  [inst_5 : Fintype ι] →
                    [inst_6 : DecidableEq ι] →
                      (i : ι) → (Q : QuadraticMap R (Mᵢ i) P) → QuadraticMap.pi (Pi.single i Q) →qᵢ Q
-- Mathlib.Data.ENat.Basic
ENat.top_ne_one : ⊤ ≠ 1
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ioc_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → Nonempty ↑(Set.Ioc a b)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc).aig.decls.size
-- Mathlib.Data.Setoid.Partition
/-- All elements of a partition of α are the equivalence class of some y ∈ α.  -/
Setoid.exists_of_mem_partition : ∀ {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α},
  s ∈ c → ∃ y, s = {x | (Setoid.mkClasses c ⋯) x y}
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftId_inv_app_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 : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapLeftId L R).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Order.AddTorsor
instCovariantClassHVAddLeOfIsOrderedVAdd : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : LE P] [inst_2 : VAdd G P] [IsOrderedVAdd G P],
  CovariantClass G P (fun x1 x2 => x1 +ᵥ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.cancel_factors_ne : ∀ {α : Type u_1} [inst : Field α] {a b ad bd a' b' gcd : α},
  ad * a = a' → bd * b = b' → ad ≠ 0 → bd ≠ 0 → gcd ≠ 0 → (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.joinPoint.sizeOf_spec : ∀ (a : Array Lean.IR.Param) (a_1 : Lean.IR.FnBody),
  sizeOf (Lean.IR.LocalContextEntry.joinPoint a a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bytes : {β : Type} → Option ByteArray → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.evaluation_preservesColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesColimitsOfShape J (PresheafOfModules.evaluation R X)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_swap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (x : AddMonoid.Coprod N M),
  (AddMonoid.Coprod.lift f g) ((AddMonoid.Coprod.swap N M) x) = (AddMonoid.Coprod.lift g f) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Inhabited β] {a : α},
  t.get! a = t[a]!
-- Mathlib.Algebra.Group.Defs
LeftCancelMonoid.mk : {M : Type u} → [toMonoid : Monoid M] → [toIsLeftCancelMul : IsLeftCancelMul M] → LeftCancelMonoid M
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.IsHomological.mk' : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [inst_8 : F.PreservesZeroMorphisms],
  (∀ (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
      ∃ T' e, ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T' ⋯).map F).Exact) →
    F.IsHomological
-- Init.Data.UInt.Bitwise
USize.toBitVec_shiftLeft : ∀ (a b : USize), (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % ↑System.Platform.numBits)
-- Qq.Match
Qq.Impl.getPatVars : Lean.Term → StateT (Array Qq.Impl.PatternVar) Lean.Elab.TermElabM Lean.Term
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c')
  [inst_3 : e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i') {Z : C} (h : L.X i' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.stupidTruncMap φ e).f i')
      (CategoryTheory.CategoryStruct.comp (L.stupidTruncXIso e hi).hom h) =
    CategoryTheory.CategoryStruct.comp (K.stupidTruncXIso e hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') h)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F],
  G.pointwiseLeftKanExtensionCompIsoOfPreserves F L =
    ((L.pointwiseLeftKanExtension F).comp G).leftKanExtensionUnique
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseLeftKanExtensionUnit F) G)
        (L.associator (L.pointwiseLeftKanExtension F) G).hom)
      (L.pointwiseLeftKanExtension (F.comp G)) (L.pointwiseLeftKanExtensionUnit (F.comp G))
-- Init.Data.Nat.Basic
Nat.pred_le_iff : ∀ {n : ℕ} {m : ℕ}, n.pred ≤ m ↔ n ≤ m.succ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'Aux_single : ∀ {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : Semiring R₁] [inst_1 : Semiring S₁] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₂ S₁ N₂] [inst_8 : Fintype n]
  [inst_9 : Fintype m] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [inst_10 : DecidableEq n] [inst_11 : DecidableEq m]
  (f : Matrix n m N₂) (i : n) (j : m), ((Matrix.toLinearMap₂'Aux σ₁ σ₂ f) (Pi.single i 1)) (Pi.single j 1) = f i j