mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.splitter : (motive : Option Bool → Option Bool → Sort u_1) →
  (lhsVal rhsVal : Option Bool) →
    ((x : Option Bool) → motive (some false) x) →
      ((x : Option Bool) → (x = some false → False) → motive x (some false)) →
        ((x : Option Bool) → (x = some false → False) → motive (some true) x) →
          ((x : Option Bool) → (x = some false → False) → (x = some true → False) → motive x (some true)) →
            ((x x_1 : Option Bool) →
                (x = some false → False) →
                  (x_1 = some false → False) → (x = some true → False) → (x_1 = some true → False) → motive x x_1) →
              motive lhsVal rhsVal
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.factorThruImage_eq : ∀ {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e]
  {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = φ → CategoryTheory.Limits.factorThruImage φ = e
-- Mathlib.Data.Set.Card
Set.exists_mem_notMem_of_ncard_lt_ncard : ∀ {α : Type u_1} {s t : Set α},
  s.ncard < t.ncard → autoParam s.Finite Set.exists_mem_notMem_of_ncard_lt_ncard._auto_1 → ∃ e ∈ t, e ∉ s
-- Mathlib.Data.Rat.Defs
Rat.intCast_div_eq_divInt : ∀ (n d : ℤ), ↑n / ↑d = Rat.divInt n d
-- Mathlib.LinearAlgebra.Semisimple
/-- A linear endomorphism is semisimple if every invariant submodule has in invariant complement.

See also `Module.End.isSemisimple_iff`.  -/
Module.End.isSemisimple_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.MonoidalOpposite.mopMopEquivalence C =
    (CategoryTheory.MonoidalOpposite.unmopEquiv Cᴹᵒᵖ).trans (CategoryTheory.MonoidalOpposite.unmopEquiv C)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.forget_δ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y : Action V G),
  CategoryTheory.Functor.OplaxMonoidal.δ (Action.forget V G) X Y =
    CategoryTheory.CategoryStruct.id ((Action.forget V G).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Any type satisfying `MonoidHomClass` and `ContinuousMapClass` can be cast into
`ContinuousMonoidHom` via `ContinuousMonoidHom.toContinuousMonoidHom`.  -/
ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            {F : Type u_7} →
              [inst_4 : FunLike F A B] → [MonoidHomClass F A B] → [ContinuousMapClass F A B] → CoeOut F (A →ₜ* B)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km fallback : α},
  t.minKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Algebra.BigOperators.Finprod
/-- For functions with finite support, multiplication commutes with finsums. See `mul_finsum` for a
statement assuming that `R` has no zero divisors.
 -/
mul_finsum' : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] (f : α → R) (r : R),
  Function.HasFiniteSupport f → r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_natAbs_eq_min : ∀ {n : ℕ} [hpos : NeZero n] (a : ZMod n), a.valMinAbs.natAbs = min a.val (n - a.val)
-- Std.Internal.UV.TCP
/-- Gets the local address of a bound TCP socket.
 -/
Std.Internal.UV.TCP.Socket.getSockName : Std.Internal.UV.TCP.Socket → IO Std.Net.SocketAddress
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.inv_hom_apply : ∀ {X Y : FinBddDistLat} (e : X ≅ Y) (x : ↑X.toDistLat),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M],
  (TrivSqZeroExt.inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range TrivSqZeroExt.inr) = ⊤
-- Init.Core
/-- Existential quantification. If `p : α → Prop` is a predicate, then `∃ x : α, p x`
asserts that there is some `x` of type `α` such that `p x` holds.
To create an existential proof, use the `exists` tactic,
or the anonymous constructor notation `⟨x, h⟩`.
To unpack an existential, use `cases h` where `h` is a proof of `∃ x : α, p x`,
or `let ⟨x, hx⟩ := h` where `.

Because Lean has proof irrelevance, any two proofs of an existential are
definitionally equal. One consequence of this is that it is impossible to recover the
witness of an existential from the mere fact of its existence.
For example, the following does not compile:
```
example (h : ∃ x : Nat, x = x) : Nat :=
  let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
  x
```
The error message `recursor 'Exists.casesOn' can only eliminate into Prop` means
that this only works when the current goal is another proposition:
```
example (h : ∃ x : Nat, x = x) : True :=
  let ⟨x, _⟩ := h  -- ok, because the goal is `True : Prop`
  trivial
```
 -/
Exists : {α : Sort u} → (α → Prop) → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.mkOfOrthogonalEqBot.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {v v_1 : ι → E} (e_v : v = v_1) (hon : Orthonormal 𝕜 v)
  (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥),
  OrthonormalBasis.mkOfOrthogonalEqBot hon hsp = OrthonormalBasis.mkOfOrthogonalEqBot ⋯ ⋯
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.TreeMap.maxKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α
-- Lean.Attributes
Lean.getAttrParamOptPrio : Lean.Syntax → Lean.AttrM ℕ
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Iic : ∀ {n : ℕ} (a : Fin n), Finset.image Fin.val (Finset.Iic a) = Finset.Iic ↑a
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.Preadditive.mono_iff_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map f))
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.fixedReduce_mkQ : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (e : V ≃ₗ[R] V) (x : V),
  e.fixedReduce ((↑e).fixedSubmodule.mkQ x) = (↑e).fixedSubmodule.mkQ (e x)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.toSubmonoid : {M : Type u_1} → [inst : MulOneClass M] → SaturatedSubmonoid M → Submonoid M
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorIdSearchStepOfBackwardPattern.match_3.eq_1 : ∀ {ρ : Type} (pat : ρ) (s : String.Slice) (it : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (motive : Option (s.sliceTo it.internalState.currPos).Pos → Sort u_1) (pos : (s.sliceTo it.internalState.currPos).Pos)
  (h_1 : (pos_1 : (s.sliceTo it.internalState.currPos).Pos) → some pos = some pos_1 → motive (some pos_1))
  (h_2 : some pos = none → motive none),
  (match h' : some pos with
    | some pos_1 => h_1 pos_1 h'
    | none => h_2 h') =
    h_1 pos ⋯
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Given a power series `P = u • X + O(X²)` with `u` is an unit in ring `R`,
this is the power series `Q` such that `P(Q(X)) = X`.
See `PowerSeries.subst_substInvOfIsUnit_right`.

See also `PowerSeries.substInv` for a variant using `Invertible`.  -/
PowerSeries.substInvOfIsUnit : {R : Type u_2} → [inst : CommRing R] → (P : PowerSeries R) → IsUnit ((PowerSeries.coeff 1) P) → PowerSeries R
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.isPrenex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsPrenex
-- Mathlib.Topology.Irreducible
/-- A set `s` is irreducible if and only if
for every finite collection of open sets all of whose members intersect `s`,
`s` also intersects the intersection of the entire collection
(i.e., there is an element of `s` contained in every member of the collection).  -/
isIrreducible_iff_sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsIrreducible s ↔ ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_add_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), deriv (fun x => c + x) x = 1
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- If `q` is a prime ideal of `p.Fiber S`,  then the localization `(p.Fiber S)_q` is an algebra
over the localization `R_p` since `p.Fiber S` is already an `R_p`-algebra. This `R_p`-algebra
structure on `(p.Fiber S)_q` agrees with the one coming from the fact that `q` lies over `p`.  -/
Ideal.instIsLiesOverAlgebraFiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (q : Ideal (p.Fiber S)) [inst_4 : q.IsPrime], Localization.AtPrime.IsLiesOverAlgebra p q
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
UniformContinuous.dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : UniformSpace β] {f g : β → α},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun b => dist (f b) (g b)
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.RequestM.findCmdParsedSnap.containsHoverPos : Lean.Server.FileWorker.EditableDocument → String.Pos.Raw → Lean.Language.Lean.CommandParsedSnapshot → Bool
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  DifferentiableWithinAt 𝕜 f s x → derivWithin (c • f) s x = c • derivWithin f s x
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [inst_2 : TopologicalSpace γ] {t : Set γ},
  TendstoLocallyUniformlyOn F f p s →
    ∀ (g : γ → α), Set.MapsTo g t s → ContinuousOn g t → TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t
-- Mathlib.Algebra.Module.TransferInstance
/-- When `α` is equipped with the `A`-module structure transferred via `e : α ≃+ β`,
this isomorphism is `A`-linear.  -/
AddEquiv.linearEquiv : {α : Type u_2} →
  {β : Type u_3} →
    (A : Type u_4) →
      [inst : Semiring A] →
        [inst_1 : AddCommMonoid α] → [inst_2 : AddCommMonoid β] → [inst_3 : Module A β] → (e : α ≃+ β) → α ≃ₗ[A] β
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_ne_last_apply : ∀ {n : ℕ} {i j : Fin (n + 1)} (hi : i ≠ Fin.last n), j ≠ i → (finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instT2Space : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X] [T2Space X],
  T2Space (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The tensor product of two bilinear forms, a shorthand for dot notation.  -/
LinearMap.BilinMap.tmul : {R : Type uR} →
  {A : Type uA} →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        {N₁ : Type uN₁} →
          {N₂ : Type uN₂} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring A] →
                [inst_2 : AddCommMonoid M₁] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : AddCommMonoid N₁] →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Algebra R A] →
                          [inst_7 : Module R M₁] →
                            [inst_8 : Module A M₁] →
                              [inst_9 : Module R N₁] →
                                [inst_10 : Module A N₁] →
                                  [inst_11 : SMulCommClass R A M₁] →
                                    [IsScalarTower R A M₁] →
                                      [inst_13 : SMulCommClass R A N₁] →
                                        [IsScalarTower R A N₁] →
                                          [inst_15 : Module R M₂] →
                                            [inst_16 : Module R N₂] →
                                              LinearMap.BilinMap A M₁ N₁ →
                                                LinearMap.BilinMap R M₂ N₂ →
                                                  LinearMap.BilinMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_natCast_eq_toNNReal : ∀ (n : ℕ), (↑n).toNNReal = (↑n).toNNReal
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_eq_zero : ∀ {a : Cardinal.{v}}, Cardinal.lift.{u, v} a = 0 ↔ a = 0
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.mk.inj : ∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {f₀ f₁ : C(X, Y)}
  {toContinuousMap : C(↑unitInterval × X, Y)} {map_zero_left : ∀ (x : X), toContinuousMap.toFun (0, x) = f₀ x}
  {map_one_left : ∀ (x : X), toContinuousMap.toFun (1, x) = f₁ x} {toContinuousMap_1 : C(↑unitInterval × X, Y)}
  {map_zero_left_1 : ∀ (x : X), toContinuousMap_1.toFun (0, x) = f₀ x}
  {map_one_left_1 : ∀ (x : X), toContinuousMap_1.toFun (1, x) = f₁ x},
  { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left } =
      { toContinuousMap := toContinuousMap_1, map_zero_left := map_zero_left_1, map_one_left := map_one_left_1 } →
    toContinuousMap = toContinuousMap_1
-- Init.Omega.Coeffs
/-- Are the coefficients all zero?  -/
Lean.Omega.Coeffs.isZero : Lean.Omega.Coeffs → Prop
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆.eq_1 : CartanMatrix.E₆ =
  !![2, 0, -1, 0, 0, 0;
    0, 2, 0, -1, 0, 0;
    -1, 0, 2, -1, 0, 0;
    0, -1, -1, 2, -1, 0;
    0, 0, 0, -1, 2, -1;
    0, 0, 0, 0, -1, 2]
-- Init.Data.BitVec.Lemmas
BitVec.twoPow_mul_eq_shiftLeft : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), BitVec.twoPow w i * x = x <<< i
-- Mathlib.CategoryTheory.Yoneda
/-- If `coyoneda.map f` is an isomorphism, so was `f`.
 -/
CategoryTheory.Coyoneda.isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  [CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)], CategoryTheory.IsIso f
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toNatLinearEquiv_trans : ∀ {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃),
  (e.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.ComposableArrows.threeδ₃Toδ₂.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ f₃_1 : k ⟶ l)
  (e_f₃ : f₃ = f₃_1) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃ =
    CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃_1 f₂₃ ⋯
-- Mathlib.Tactic.Tauto
/-- Simulates the `<;>` tactic combinator.
First runs `tac1` and then runs `tac2` on all newly-generated subgoals.
 -/
_private.Mathlib.Tactic.Tauto.0.Mathlib.Tactic.Tauto.«term_<;>_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsRightCancelAdd α], IsRightCancelAdd (Colex α)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.inv_le_self : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulRightMono α] {a : α}, 1 ≤ a → a⁻¹ ≤ a
-- Mathlib.CategoryTheory.Elements
CategoryTheory.NatTrans.mapElements_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (φ : F ⟶ G)
  (x : F.Elements),
  (CategoryTheory.NatTrans.mapElements φ).obj x =
    match x with
    | ⟨X, x⟩ => ⟨X, (CategoryTheory.ConcreteCategory.hom (φ.app X)) x⟩
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.smulZeroClass : {R : Type u_5} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Zero M] → [inst_1 : Zero N] → [SMulZeroClass R M] → [SMulZeroClass R N] → SMulZeroClass R (M × N)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `K / E / F` is a field extension tower such that `K / F` is purely inseparable,
then `E / F` is also purely inseparable.  -/
IsPurelyInseparable.tower_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K], IsPurelyInseparable F E
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_ofSupport : ∀ {V : Type u} {G : SimpleGraph V} {l : List V} (hne : l ≠ []) (hchain : List.IsChain G.Adj l),
  (SimpleGraph.Walk.ofSupport l hne hchain).length = l.length - 1
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.wellFoundedRelation : {R : Type u} → [EuclideanDomain R] → WellFoundedRelation R
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_mk_factorThruImage_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.image.lift
        { I := CategoryTheory.Limits.image f, m := CategoryTheory.Limits.image.ι f, m_mono := ⋯,
          e := CategoryTheory.Limits.factorThruImage f, fac := ⋯ })
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
-- Std.Http.Data.Status
Std.Http.Status.notFound.sizeOf_spec : sizeOf Std.Http.Status.notFound = 1
-- Init.Data.UInt.Lemmas
UInt64.toUSize_mod_of_dvd_usizeSize : ∀ (a b : UInt64), b.toNat ∣ USize.size → (a % b).toUSize = a.toUSize % b.toUSize
-- Mathlib.Analysis.Complex.Norm
Complex.dist_of_im_eq : ∀ {z w : ℂ}, z.im = w.im → dist z w = dist z.re w.re
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.tendsto_eulerMascheroniSeq' : Filter.Tendsto Real.eulerMascheroniSeq' Filter.atTop (nhds Real.eulerMascheroniConstant)
-- Mathlib.RingTheory.Perfection
/-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,
any homomorphism `R →+* S` can be lifted to a homomorphism `R →+* Perfection S p`.  -/
Perfection.lift : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    (R : Type u₁) →
      [inst : CommSemiring R] →
        [CharP R p] →
          [PerfectRing R p] →
            (S : Type u₂) → [inst_3 : CommSemiring S] → [inst_4 : CharP S p] → (R →+* S) ≃ (R →+* Perfection S p)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.mem_saturation_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {s : Submonoid M} {x : M}, x ∈ s.saturation ↔ ∃ y, x * y ∈ s
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Polynomial.instFree : ∀ {R : Type u_1} [inst : Semiring R], Module.Free R (Polynomial R)
-- Mathlib.FieldTheory.Separable
/-- If `n = 0` in `R` and `b` is a unit, then `a * X ^ n + b * X + c` is separable.  -/
Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} (a b c : R),
  ↑n = 0 → IsUnit b → (Polynomial.C a * Polynomial.X ^ n + Polynomial.C b * Polynomial.X + Polynomial.C c).Separable
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₂_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₂.map f = f.τ₂
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `C` and `g` tends to `atBot` then `f + g` tends to `atBot`.  -/
Filter.Tendsto.add_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_lt_ceil_of_lt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a b : R},
  a < b → ⌊a⌋ < ⌈b⌉
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.lt_of_lt_of_ne_top : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : LinearOrder n] [inst_2 : LT m] {i₁ i₂ : m}, A.IsPivotedBy l → i₁ < i₂ → l i₁ ≠ ⊤ → l i₁ < l i₂
-- Mathlib.GroupTheory.OrderOfElement
zpow_mod_orderOf : ∀ {G : Type u_1} [inst : Group G] (x : G) (z : ℤ), x ^ (z % ↑(orderOf x)) = x ^ z
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_pi_ball : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [inst_3 : (i : ι) → MetricSpace (α i)] (x : (i : ι) → α i)
  {r : ℝ}, 0 < r → MeasureTheory.volume (Metric.ball x r) = ∏ i, MeasureTheory.volume (Metric.ball (x i) r)
-- Std.Net.Addr
/-- This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
 -/
Std.Net.IPv4Addr.octets : Std.Net.IPv4Addr → Vector UInt8 4
-- Mathlib.NumberTheory.SmoothNumbers
/-- The product of the prime factors of `n` that are less than `N` is an `N`-smooth number.  -/
Nat.prod_mem_smoothNumbers : ∀ (n N : ℕ), (List.filter (fun x => decide (x < N)) n.primeFactorsList).prod ∈ N.smoothNumbers
-- Mathlib.CategoryTheory.IsoCat
/-- A functor `F : C ⥤ D` is an isomorphism of categories if it is full, faithful and
bijective on objects. Such a functor has a strict inverse `Functor.strictInv` and assembles
into an `IsoCat` via `Functor.asIsomorphism`.  -/
CategoryTheory.Functor.IsIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.String.Lemmas.Order
String.Pos.isUTF8FirstByte_getUTF8Byte_offset : ∀ {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos}, (s.getUTF8Byte p.offset h).IsUTF8FirstByte
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFiniteAut : ∀ (X : FintypeCat), Finite (CategoryTheory.Aut X)