mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Nat.Pairwise
/-- The list `List.finRange n` is increasing.  -/
List.pairwise_le_finRange : ∀ (n : ℕ), List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.finRange n)
-- Mathlib.RingTheory.HahnSeries.Cardinal
/-- The `κ`-bounded subgroup of Hahn series with less than `κ` terms.  -/
HahnSeries.cardSuppLTAddSubgroup : (Γ : Type u_1) →
  (R : Type u_2) →
    (κ : Cardinal.{u_1}) →
      [inst : PartialOrder Γ] → [inst_1 : AddGroup R] → [hκ : Fact (Cardinal.aleph0 ≤ κ)] → AddSubgroup (HahnSeries Γ R)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_congr_identDistrib : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ},
  ProbabilityTheory.IdentDistrib X Y μ μ' → ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ'
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.length.eq_1 : ∀ {n : ℕ} (c : CompositionAsSet n), c.length = c.boundaries.card - 1
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_symm_apply_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Iic x)), (OrderIso.sumLexIicIoi x).symm ↑a = Sum.inl a
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ext_iff : ∀ {X Y : GrpCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.natCard_eq : ∀ (G : Type u_1) [inst : AddCommGroup G] (n : ℕ) [NeZero n] [Module.Free ℤ G] [Module.Finite ℤ G],
  Nat.card (ModN G n) = n ^ Module.finrank ℤ G
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_reindex : ∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  {κ' : Type u_7} (b : Module.Basis κ A B) (f : κ ≃ κ'),
  Algebra.traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (Algebra.traceMatrix A ⇑b)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instCompleteLatticeSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → CompleteLattice (Subalgebra R A)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendHom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt), (s.extendHom f).hom = f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} [inst_2 : SizeOf C] (hom : M.X ⟶ N.X) [isMonHom_hom : CategoryTheory.IsMonHom hom],
  sizeOf { hom := hom, isMonHom_hom := isMonHom_hom } = 1 + sizeOf hom + sizeOf isMonHom_hom
-- Init.Data.Int.Order
Int.add_neg : ∀ {a b : ℤ}, a < 0 → b < 0 → a + b < 0
-- Mathlib.Tactic.Inhabit
/-- Derives `Inhabited α` from `Nonempty α` with `Classical.choice`.  -/
Lean.Elab.Tactic.nonempty_to_inhabited : (α : Sort u_1) → Nonempty α → Inhabited α
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsLocalIso
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.polyCharpoly_coeff_rank_ne_zero : ∀ (R : Type u_1) (L : Type u_3) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R]
  [inst_7 : DecidableEq ι], ((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L) ≠ 0
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.whiskerLeft_toNatTrans : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴)
  {G H : CategoryTheory.BasedFunctor 𝒴 𝒵} (α : G ⟶ H),
  (CategoryTheory.BasedCategory.whiskerLeft F α).toNatTrans = F.whiskerLeft α.toNatTrans
-- Init.Data.Int.Order
Int.instTransLe : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Std.Internal.Do.Order.Basic
/-- Indexed supremum  -/
Lean.Order.iSup : {α : Type u} → [Lean.Order.CompleteLattice α] → {ι : Type v} → (ι → α) → α
-- Init.Data.List.Monadic
List.forIn_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)},
  forIn (List.map g l) init f = forIn l init fun a y => f (g a) y
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_of_pow_le_pow_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ}
  [MulPosMono M₀], n ≠ 0 → 0 ≤ b → a ^ n ≤ b ^ n → a ≤ b
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation of `p : PadicAlgCl p` is `1/p`.  -/
PadicAlgCl.valuation_p : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Valued.v ↑p = 1 / ↑p
-- Mathlib.Order.Filter.AtTopBot.Basic
Nat.map_cast_int_atTop : Filter.map Nat.cast Filter.atTop = Filter.atTop
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_mul : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a b : G), ↑(a * b) = ↑a * ↑b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.neg_lt_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a : α}, 0 < a → -a < a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of the results of subtracting a default base point
from the given points, as a linear map on the weights.  This is
intended to be used when the sum of the weights is 0; that condition
is specified as a hypothesis on those lemmas that require it.  -/
Finset.weightedVSub : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [S : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → (ι → k) →ₗ[k] V
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.unop_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.LeftFraction X Y), φ.unop.f = φ.f.unop
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Get proofs of `-x^2 ≤ 0` and `-(x*x) ≤ 0`, when those terms appear in `ls`  -/
_private.Mathlib.Tactic.Linarith.Preprocessing.0.Mathlib.Tactic.Linarith.nlinarithGetSquareProofs : List Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Init.Data.Int.LemmasAux
Int.natCast_toNat_eq_self : ∀ {a : ℤ}, ↑a.toNat = a ↔ 0 ≤ a
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_4 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_4 id c pivot rupHints ratHints
-- Mathlib.Data.EReal.Operations
EReal.neg_mul : ∀ (x y : EReal), -x * y = -(x * y)
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  V₁ =ᶠ[nhdsWithin x (insert x s)] V →
    W₁ =ᶠ[nhdsWithin x (insert x s)] W →
      VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Lean.Declaration
Lean.AxiomVal.isUnsafeEx : Lean.AxiomVal → Bool
-- Init.Data.BitVec.Lemmas
BitVec.not_or_self : ∀ {w : ℕ} (x : BitVec w), ~~~x ||| x = BitVec.allOnes w
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Data.Int.Cast.Pi
Pi.intCast_def : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → IntCast (π i)] (n : ℤ), ↑n = fun x => ↑n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R),
  0 ≤ a * a
-- Init.Core
/-- An idempotent operation satisfies `a ∘ a = a`.  -/
Std.IdempotentOp.idempotent : ∀ {α : Sort u} {op : α → α → α} [self : Std.IdempotentOp op] (x : α), op x x = x
-- Mathlib.Algebra.Algebra.Equiv
/-- A linear equivalence of two modules induces an equivalence of algebras of their
endomorphisms.  -/
LinearEquiv.conjAlgEquiv : (R : Type u_1) →
  {S : Type u_2} →
    {M₁ : Type u_3} →
      {M₂ : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : Module R M₁] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M₂] →
                  [inst_5 : Semiring S] →
                    [inst_6 : Module S M₁] →
                      [inst_7 : Module S M₂] →
                        [inst_8 : SMulCommClass S R M₁] →
                          [inst_9 : SMulCommClass S R M₂] →
                            [inst_10 : SMul R S] →
                              [inst_11 : IsScalarTower R S M₁] →
                                [inst_12 : IsScalarTower R S M₂] → (M₁ ≃ₗ[S] M₂) → Module.End S M₁ ≃ₐ[R] Module.End S M₂
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_zero_left : ∀ (a : Ordinal.{u_1}), Ordinal.deriv 0 a = a
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instSMulZeroClass : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_5} →
        [inst : PartialOrder Γ] →
          [inst_1 : PartialOrder Γ'] →
            [inst_2 : VAdd Γ Γ'] →
              [IsOrderedCancelVAdd Γ Γ'] →
                [inst_4 : AddCommMonoid V] →
                  [inst_5 : Zero R] → [inst_6 : SMulZeroClass R V] → SMulZeroClass (HahnSeries Γ R) (HahnModule Γ' R V)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.mdifferentiableAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → MDiffAt f x
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The embedding of an additive magma into its additive magma algebra.  -/
AddMonoidAlgebra.ofMagma : (R : Type u_8) → (M : Type u_9) → [inst : Semiring R] → [inst_1 : Add M] → Multiplicative M →ₙ* AddMonoidAlgebra R M
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    Lean.Grind.Linarith.Expr.denote ctx lhs < Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p < 0
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.one : {α : Type u_1} → [inst : Zero α] → [inst_1 : One α] → [inst_2 : LE α] → [ZeroLEOneClass α] → One { x // 0 ≤ x }
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCancelCommMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CancelCommMonoid Mᵐᵒᵖ], DomMulAct.instCancelCommMonoidOfMulOpposite = inst
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.degree : Lean.Grind.CommRing.Poly → ℕ
-- Std.Http.Data.URI.Basic
/-- Gets the first value of a query parameter by key name, decoded as a string.
Returns `none` if the key is not found or if the value cannot be decoded as UTF-8.
 -/
Std.Http.URI.Query.get : Std.Http.URI.Query → String → Option String
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Slow.instDecidableMemP : {α : Type u_1} → {cut : α → Ordering} → {t : RBTree.RBNode α} → Decidable (RBTree.RBNode.MemP cut t)
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Convergence in Lp implies uniform tightness.  -/
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.unifTight_of_tendsto_Lp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : ℕ → α → β} {g : α → β},
  p ≠ ⊤ →
    (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
      MeasureTheory.MemLp g p μ →
        Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0) →
          MeasureTheory.UnifTight f p μ
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.registerBuiltinSimproc : Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.Simproc → IO Unit
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.addHom.eq_1 : @Pi.addHom = @AddHom.pi
-- Qq.Macro
Qq.Impl.unquoteExpr : Lean.Expr → Qq.Impl.UnquoteM Lean.Expr
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instStarModule : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {𝕜 : Type u_2} [inst_1 : Zero 𝕜] [inst_2 : Star 𝕜]
  [inst_3 : AddMonoid β] [inst_4 : StarAddMonoid β] [inst_5 : TopologicalSpace β] [inst_6 : ContinuousStar β]
  [inst_7 : SMulWithZero 𝕜 β] [inst_8 : ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β],
  StarModule 𝕜 (ZeroAtInftyContinuousMap α β)
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) (a : α), (g.comp f) a = g (f a)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤)) (X.Γevaluation x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp S.toCycles S.leftHomologyπ = 0
-- Mathlib.Algebra.GroupWithZero.Divisibility
ne_zero_of_dvd_ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] {p q : α}, q ≠ 0 → p ∣ q → p ≠ 0
-- Lean.Meta.Canonicalizer
/-- The definitionally equality tests are performed using the given transparency mode.
We claim `TransparencyMode.instances` is a good setting for most applications.
 -/
Lean.Meta.Canonicalizer.CanonM.run' : {α : Type} →
  Lean.Meta.CanonM α →
    optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances →
      optParam Lean.Meta.Canonicalizer.State { } → Lean.MetaM α
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.mk : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} →
                  {B₂ : LinearMap.BilinForm R M₂} →
                    (toLinearMap : M₁ →ₗ[R] M₂) →
                      (∀ (m m' : M₁), (B₂ (toLinearMap.toFun m)) (toLinearMap.toFun m') = (B₁ m) m') → B₁ →bᵢ B₂
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under addition.  -/
IntermediateField.add_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x y : L}, x ∈ S → y ∈ S → x + y ∈ S
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.subtypeVal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  IsUpperSet s → ∀ {a : ↑s}, Order.IsPredPrelimit a → Order.IsPredPrelimit ↑a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [QuasiSeparatedSpace ↥X],
  AlgebraicGeometry.QuasiCompact
    (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanShapeEnd_fst : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (f : CategoryTheory.Arrow J),
  (CategoryTheory.Limits.multicospanShapeEnd J).fst f = f.left
-- Mathlib.GroupTheory.Congruence.Hom
/-- Homomorphisms on the quotient of a monoid by a congruence relation are equal if they
are equal on elements that are coercions from the monoid.  -/
Con.lift_funext : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} (f g : c.Quotient →* P),
  (∀ (a : M), f ↑a = g ↑a) → f = g
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subtractionMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → SubtractionMonoid (f i)],
  Pi.subtractionMonoid = { toSubNegMonoid := Pi.subNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- In a category in which every epimorphism is regular, we can express every epimorphism as
a coequalizer. This is not an instance because it would create an instance loop.  -/
CategoryTheory.regularEpiOfEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.IsRegularEpiCategory C] → (f : X ⟶ Y) → [CategoryTheory.Epi f] → CategoryTheory.RegularEpi f
-- Mathlib.Algebra.Group.Action.Defs
AddAction.toAddSemigroupAction : {G : Type u_9} → {P : Type u_10} → {inst : AddMonoid G} → [self : AddAction G P] → AddSemigroupAction G P
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A simple continued fraction is a *(regular) continued fraction* ((r)cf) if all partial denominators
`bᵢ` are positive, i.e. `0 < bᵢ`.
 -/
SimpContFract.IsContFract : {α : Type u_1} → [inst : One α] → [Zero α] → [LT α] → SimpContFract α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_iInf : ∀ {V : Type u} (G : SimpleGraph V), G.chromaticNumber = ⨅ n, ↑↑n
-- Mathlib.Analysis.Convex.Strict
StrictConvex.is_linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] {s : Set F},
  StrictConvex 𝕜 s → ∀ {f : E → F}, IsLinearMap 𝕜 f → Continuous f → Function.Injective f → StrictConvex 𝕜 (f ⁻¹' s)
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivOpCLM_eq_lineDerivCLM : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F] {v : E}, LineDeriv.lineDerivOpCLM ℝ (Distribution Ω F ⊤) v = Distribution.lineDerivCLM v
-- Mathlib.Tactic.FunProp.Theorems
/-- Return proof of lambda theorem  -/
Mathlib.Meta.FunProp.LambdaTheorem.getProof : Mathlib.Meta.FunProp.LambdaTheorem → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow_mono : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)}, 𝒜 ⊆ ℬ → 𝒜.shadow ⊆ ℬ.shadow
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- Constructor for isomorphisms between lax monoidal functors.  -/
CategoryTheory.LaxMonoidalFunctor.isoOfComponents : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F G : CategoryTheory.LaxMonoidalFunctor C D} →
              (e : (X : C) → F.obj X ≅ G.obj X) →
                autoParam
                    (∀ {X Y : C} (f : X ⟶ Y),
                      CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom =
                        CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
                    CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_1 →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
                          (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
                        CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
                      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_3 →
                    autoParam
                        (∀ (X Y : C),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
                              (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
                              (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
                        CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_5 →
                      (F ≅ G)
-- Init.Data.UInt.Basic
/-- Converts a `Fin UInt8.size` into the corresponding `UInt8`.  -/
UInt8.ofFin : Fin UInt8.size → UInt8
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.points_mem_affineSpan_faceOpposite : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Nontrivial k] {n : ℕ} [inst_5 : NeZero n] (s : Affine.Simplex k P n) {i j : Fin (n + 1)},
  s.points j ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ j ≠ i
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.canonicallyOverPullback : {M S T : AlgebraicGeometry.Scheme} →
  [inst : M.Over S] → {f : T ⟶ S} → (CategoryTheory.Limits.pullback (M ↘ S) f).CanonicallyOver T