mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_6 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w l r : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr l)
  (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r)
  (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.append rhs h with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_6 w l r lhs rhs h
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instCanLift : ∀ {α : Type u}, CanLift (WithOne α) α WithOne.coe fun a => a ≠ 1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_subset_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.finite_setOfPred_matroid`.

---

For finite `E`, finitely many matroids have ground set contained in `E`.  -/
Matroid.finite_setOf_matroid : ∀ {α : Type u_1} {E : Set α}, E.Finite → {M | M.E ⊆ E}.Finite
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} {l : List α} {k : α},
  Std.DTreeMap.Const.insertManyIfNewUnit t (k :: l) = Std.DTreeMap.Const.insertManyIfNewUnit (t.insertIfNew k ()) l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.map_fst_toList_eq_keys : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  List.map Prod.fst (Std.DTreeMap.Raw.Const.toList t) = t.keys
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  (hf : AlgebraicGeometry.sourceLocalClosure W P f) (i : hf.cover.I₀),
  P (CategoryTheory.CategoryStruct.comp (hf.cover.f i) f)
-- Mathlib.FieldTheory.KummerExtension
autEquivZmod.eq_1 : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1)
  [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n] {ζ : K}
  (hζ : IsPrimitiveRoot ζ n),
  autEquivZmod H L hζ =
    (autEquivRootsOfUnity ⋯ H L).trans
      ((MulEquiv.subgroupCongr ⋯).trans (AddEquiv.toMultiplicativeRight ⋯.zmodEquivZPowers.symm))
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.ker_toQuotient : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  relations.toQuotient.ker = Submodule.span A (Set.range relations.relation)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateAnchors.mk.sizeOf_spec : ∀ (candidates : Array Lean.Meta.Grind.SplitCandidateWithAnchor) (numDigits : ℕ),
  sizeOf { candidates := candidates, numDigits := numDigits } = 1 + sizeOf candidates + sizeOf numDigits
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- `f.next i` is `f.f j` if there is some `r i j`, and `f.f j` otherwise.  -/
HomologicalComplex.Hom.next : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → {C₁ C₂ : HomologicalComplex V c} → C₁.Hom C₂ → (i : ι) → C₁.xNext i ⟶ C₂.xNext i
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (x : ↥X) (y : ↑(X.presheaf.stalk (e.inv (e.hom x)))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom x))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv (e.hom x))) y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkCongr ⋯).hom) y
-- Mathlib.NumberTheory.LSeries.PrimesInAP
Nat.infinite_setOfPred_prime_and_modEq : ∀ {q a : ℕ}, q ≠ 0 → a.Coprime q → {p | Nat.Prime p ∧ p ≡ a [MOD q]}.Infinite
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.supDegree_esymmAlgHomMonomial : ∀ {R : Type u_3} {n m : ℕ} [inst : CommSemiring R] {r : R},
  r ≠ 0 →
    ∀ (t : Fin n →₀ ℕ),
      n ≤ m →
        ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.esymmAlgHomMonomial (Fin m) t r))) =
          (Fin.accumulate n m) ⇑t
-- Init.Data.String.Decode
ByteArray.validateUTF8At : ByteArray → ℕ → Bool
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_ref__1 : Lean.ParserDescr
-- Mathlib.Data.Analysis.Topology
/-- A `Ctop` realizes the topological space it generates.  -/
Ctop.toRealizer : {α : Type u_1} → {σ : Type u_3} → (F : Ctop α σ) → Ctop.Realizer α
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_v : ∀ (u : PNat.XgcdType), u.flip.v = u.v.swap
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_one : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)], (PiTensorProduct.mapL fun i => 1) = 1
-- Mathlib.Topology.Inseparable
IsClosed.continuous_piecewise_of_specializes : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f g : X → Y}
  [inst_2 : DecidablePred fun x => x ∈ s],
  IsClosed s → Continuous f → Continuous g → (∀ (x : X), g x ⤳ f x) → Continuous (s.piecewise f g)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_top : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq V] [inst_1 : Ring α],
  SimpleGraph.adjMatrix α ⊤ = Matrix.of fun i j => if i = j then 0 else 1
-- Init.Data.Nat.Lemmas
Nat.right_eq_add : ∀ {a b : ℕ}, b = a + b ↔ a = 0
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField : ∀ {𝕜 : 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),
  ¬IsRCLikeNormedField 𝕜 → Set.range ↑I = Set.univ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonRenameParams.fromJson : Lean.Json → Except String Lean.Lsp.RenameParams
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_intCast : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (z : ℤ), (↑z).toEnd = ↑z
-- Batteries.Control.Nondet.Basic
/-- Filter a nondeterministic value.  -/
Nondet.filter : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → (α → Bool) → Nondet m α → Nondet m α
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is additive in the first coordinate.  -/
PreInnerProductSpace.Core.add_left : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : PreInnerProductSpace.Core 𝕜 F) (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z
-- Mathlib.Order.BooleanAlgebra.Basic
_private.Mathlib.Order.BooleanAlgebra.Basic.0.sdiff_le' : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y ≤ x
-- Mathlib.Algebra.Ring.IsFormallyReal
AddSubsemigroup.coe_sumNonzeroSq : ∀ (R : Type u_1) [inst : AddMonoid R] [inst_1 : Mul R], ↑(AddSubsemigroup.sumNonzeroSq R) = {s | IsSumNonzeroSq s}
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.codeBlock : Lean.Elab.Term.Do.ToCodeBlock.Catch → Lean.Elab.Term.Do.CodeBlock
-- Mathlib.RingTheory.Idempotents
Subsemigroup.mem_corner_iff_mem_range_mul_right : ∀ {R : Type u_1} {e : R} [inst : Semigroup R],
  IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ r ∈ Set.range fun x => x * e
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.reindex_toColimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J'] {X : C}
  (h : P.ColimitOfShape J X) (G : CategoryTheory.Functor J' J) [inst_3 : G.Final],
  (h.reindex G).toColimitPresentation = h.reindex G
-- Init.Data.Array.Zip
Array.zip_map_right : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {as : Array α} {bs : Array β},
  as.zip (Array.map f bs) = Array.map (Prod.map id f) (as.zip bs)
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- If `N` is a submodule with finite rank, do induction on adjoining a linear independent
element to a submodule.  -/
Submodule.inductionOnRankAux : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_5} →
      [inst : Ring R] →
        [IsDomain R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              Module.Basis ι R M →
                (P : Submodule R M → Sort u_7) →
                  ((N : Submodule R M) →
                      ((N' : Submodule R M) →
                          N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') →
                        P N) →
                    (n : ℕ) →
                      (N : Submodule R M) →
                        (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
-- Mathlib.Topology.EMetricSpace.Weak
/-- If `some : α → Option α` is an open embedding and `α` is has a weak pseudo extended metric
structure, the structure extends naturally to `Option α`.  -/
Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : TopologicalSpace (Option α)] →
      [m : WeakPseudoEMetricSpace α] →
        [inst_1 : EDist (Option α)] →
          inst_1 = Option.toEDist → Topology.IsOpenEmbedding some → WeakPseudoEMetricSpace (Option α)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.le_lift_iff : ∀ {a : Cardinal.{u}} {b : Cardinal.{max u v}}, b ≤ Cardinal.lift.{v, u} a ↔ ∃ a' ≤ a, Cardinal.lift.{v, u} a' = b
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.K'.elim.match_1.splitter : (motive : Turing.PartrecToTM2.K' → Sort u_1) →
  (x : Turing.PartrecToTM2.K') →
    (Unit → motive Turing.PartrecToTM2.K'.main) →
      (Unit → motive Turing.PartrecToTM2.K'.rev) →
        (Unit → motive Turing.PartrecToTM2.K'.aux) → (Unit → motive Turing.PartrecToTM2.K'.stack) → motive x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.Const.get! : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → [Inhabited β] → Std.DTreeMap.Raw α (fun x => β) cmp → α → β
-- Mathlib.Order.Hom.Basic
OrderEmbedding.gtEmbedding_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) (x : α), f.gtEmbedding x = f x
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_smul_of_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {r : ℝ},
  0 < r → ∀ (x : V), NormedSpace.normalize (r • x) = NormedSpace.normalize x
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.smul_le_self_of_tower : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_4}
  [inst_3 : Monoid α] [inst_4 : SMul α R] [inst_5 : DistribMulAction α M] [inst_6 : SMulCommClass α R M]
  [IsScalarTower α R M] (a : α) (S : Submodule R M), a • S ≤ S
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_symm_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (a : CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂).symm a =
    adj₂.homEquiv₂.symm
      (CategoryTheory.CategoryStruct.comp (adj₁.homEquiv₁.symm a) (CategoryTheory.Bicategory.associator l₁ h r₂).inv)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.mk : {H : Type u_5} →
  [inst : TopologicalSpace H] →
    {M : Type u_6} →
      (atlas : Set (PartialEquiv M H)) →
        (chartAt : M → PartialEquiv M H) →
          (∀ (x : M), x ∈ (chartAt x).source) →
            (∀ (x : M), chartAt x ∈ atlas) →
              (∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source) →
                (∀ (e e' : PartialEquiv M H),
                    e ∈ atlas → e' ∈ atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source) →
                  ChartedSpaceCore H M
-- Mathlib.Algebra.Order.Kleene
Prod.instIdemSemiring : {α : Type u_1} → {β : Type u_2} → [IdemSemiring α] → [IdemSemiring β] → IdemSemiring (α × β)
-- Mathlib.Analysis.Convex.Between
sbtw_lineMap_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y : P}
  {r : R}, Sbtw R x ((AffineMap.lineMap x y) r) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_nonneg : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V), 0 ≤ f.normDet
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
Set.Subsingleton.threeAPFree : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α}, s.Subsingleton → ThreeAPFree s
-- Lean.Meta.Sym.AlphaShareBuilder
/-- Same as `mkAppS f args` but reversing `args`, with max sharing.  -/
Lean.Meta.Sym.Internal.mkAppRevS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Array Lean.Expr → m Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDerivWithin_sin_Ioo : ∀ (n : ℕ) {a b x : ℝ}, x ∈ Set.Ioo a b → iteratedDerivWithin n Real.sin (Set.Ioo a b) x = iteratedDeriv n Real.sin x
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabNameMkStr : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Set.Order
/-- Quantifying over a set is antitone in the set  -/
Set.antitone_bforall : ∀ {α : Type u_1} {P : α → Prop}, Antitone fun s => ∀ x ∈ s, P x
-- Mathlib.FieldTheory.Separable
Polynomial.not_separable_zero : ∀ {R : Type u} [inst : CommSemiring R] [Nontrivial R], ¬Polynomial.Separable 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves finite limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_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) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteColimits F.op
-- Mathlib.Util.Notation3
Mathlib.Notation3.MatchState.mk.injEq : ∀ (vars : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances))
  (scopeState : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)))
  (foldState : Std.HashMap Lean.Name (Array Lean.Term))
  (vars_1 : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances))
  (scopeState_1 : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)))
  (foldState_1 : Std.HashMap Lean.Name (Array Lean.Term)),
  ({ vars := vars, scopeState := scopeState, foldState := foldState } =
      { vars := vars_1, scopeState := scopeState_1, foldState := foldState_1 }) =
    (vars = vars_1 ∧ scopeState = scopeState_1 ∧ foldState = foldState_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The isomorphism `S.leftHomology ≅ h.H` induced by a left homology data `h` for a
short complex `S`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → [inst_2 : S.HasLeftHomology] → S.leftHomology ≅ h.H
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.quasiIso_eq_quasiIso_map_quotient : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C],
  HomotopyCategory.quasiIso C c = (HomologicalComplex.quasiIso C c).map (HomotopyCategory.quotient C c)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.copy_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α → β)
  (g : α →𝒄 β) (h : f = ⇑g) (a : α), (OmegaCompletePartialOrder.ContinuousHom.copy f g h) a = f a
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (c : Cᵒᵖ) (d : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj (Opposite.unop c) (Opposite.unop d) =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.MvPolynomialC.numBound.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A composition of natural transformations gives the composition of corresponding functors.  -/
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₀ F₁ F₂ : CategoryTheory.Functor C C} →
      (α : F₀ ⟶ F₁) →
        (β : F₁ ⟶ F₂) →
          CategoryTheory.Endofunctor.Algebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Endofunctor.Algebra.functorOfNatTrans β).comp
              (CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_eq_top : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M}, c.toSetoid = ⊤ ↔ c = ⊤
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.continuous_rpow_const : ∀ {y : ℝ}, 0 ≤ y → Continuous fun x => x ^ y
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.mk.sizeOf_spec : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (declNames : Array Lean.Name)
  (declNameNonRec : Lean.Name) (argsPacker : Lean.Meta.ArgsPacker) (fixedParamPerms : Lean.Elab.FixedParamPerms),
  sizeOf
      { declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, argsPacker := argsPacker, fixedParamPerms := fixedParamPerms } =
    1 + sizeOf declName + sizeOf levelParams + sizeOf type + sizeOf value + sizeOf declNames + sizeOf declNameNonRec +
        sizeOf argsPacker +
      sizeOf fixedParamPerms
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).isEmpty =
      ((m.isEmpty || m.size == 1 && m.contains k) && (f (Std.DHashMap.Raw.Const.get? m k)).isNone)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal_one : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R],
  n ≠ 0 → (MvPowerSeries.truncTotal n) 1 = 1
-- Mathlib.RingTheory.DedekindDomain.Different
not_dvd_differentIdeal_of_isCoprime : ∀ (A : Type u_1) {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal]
  [Finite (A ⧸ p)] (P Q : Ideal B) [P.IsMaximal],
  IsCoprime P Q → P * Q = Ideal.map (algebraMap A B) p → ¬P ∣ differentIdeal A B
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.map.eq_1 : ∀ {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(Set.powersetCard α n)),
  Set.powersetCard.map n f s = ⟨Finset.map f ↑s, ⋯⟩
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.ofNat : ℕ → Lean.Meta.NormCast.Label
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.tensor_map_id_left_eq_map : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) [inst_1 : IsNoetherianRing R] {M : Type u} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module R N] (f : M →ₗ[R] N)
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R N],
  TensorProduct.AlgebraTensorModule.map LinearMap.id f =
    ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ
      AdicCompletion.map I f ∘ₗ ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M)
-- Lean.Meta.AppBuilder
/-- Returns `a < b`. This method assumes `a` and `b` have the same type.  -/
Lean.Meta.mkLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- **Alias** of `CategoryTheory.NatTrans.Coequifibered`. -/
AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization : {J : Type u_1} →
  {C : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_3} C] → CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)
-- Mathlib.Data.SetLike.Basic
SetLike.coe_strictMono : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B],
  StrictMono SetLike.coe