mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The ring isomorphism between multivariable polynomials in a sum of two types,
and multivariable polynomials in one of the types,
with coefficients in multivariable polynomials in the other type.
 -/
MvPolynomial.sumRingEquiv : (R : Type u) →
  (S₁ : Type v) →
    (S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
-- Init.Data.Float.Float32
/-- Computes the hyperbolic cosine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`coshf`.
 -/
Float32.cosh : Float32 → Float32
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Formally adjoin an initial object to a category.  -/
CategoryTheory.WithInitial : Type u → Type u
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyInvHomId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂), e.symm.homotopyInvHomId = e.homotopyHomInvId
-- Lean.Meta.Sym.Arith.Types
/-- Commutative rings.  -/
Lean.Meta.Sym.Arith.State.rings : Lean.Meta.Sym.Arith.State → Array Lean.Meta.Sym.Arith.CommRing
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instFunLike : {M : Type u_4} → {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZero N] → FunLike (M →+ N) M N
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.insert : ∀ {𝕜 : 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} {s : Set M},
  MDiffAt[s] f x → MDiffAt[insert x s] f x
-- Mathlib.Order.Booleanisation
Booleanisation.comp_le_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Booleanisation.comp a ≤ Booleanisation.comp b ↔ b ≤ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minEntryD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {fallback : (a : α) × β a}, t₁.minEntryD fallback = t₂.minEntryD fallback
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo : Type
-- Mathlib.Data.Int.CardIntervalMod
Int.Ioc_filter_modEq_eq : ∀ (a b : ℤ) {r : ℤ} (v : ℤ),
  {x ∈ Finset.Ioc a b | x ≡ v [ZMOD r]} =
    Finset.map { toFun := fun x => x + v, inj' := ⋯ } ({x ∈ Finset.Ioc (a - v) (b - v) | r ∣ x})
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalCommSemiring : {R : Type u_1} →
  {M : Type u_4} → [inst : CommSemiring R] → [CommSemigroup M] → NonUnitalCommSemiring (MonoidAlgebra R M)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w'))
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F]
  [inst_2 : CategoryTheory.FunctorToTypes.Small.{max w w'', w', v, u} F] (X : C),
  (CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso F).inv.app X =
    ((Equiv.ulift.trans (equivShrink (F.obj X)).symm).trans (equivShrink (F.obj X))).toIso.inv
-- Std.Sat.AIG.LawfulOperator
_private.Std.Sat.AIG.LawfulOperator.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1)
  (h_1 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_1 ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.closedBall_zero_eq : ∀ {n : Type u_7} [inst : Fintype n] (r : ℝ), 0 ≤ r → Metric.closedBall 0 r = {x | ∑ i, x.ofLp i ^ 2 ≤ r ^ 2}
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.comp_left_injective : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (e : M ≃* N), Function.Injective fun f => f.comp ↑e
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instUnionOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Union (Std.ExtTreeMap α β cmp)
-- Mathlib.Order.Filter.Partial
Filter.pmap_res : ∀ {α : Type u} {β : Type v} (l : Filter α) (s : Set α) (f : α → β),
  Filter.pmap (PFun.res f s) l = Filter.map f (l ⊓ Filter.principal s)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift.unique' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ : MultilinearMap R s E} {φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E},
  φ'.compMultilinearMap (PiTensorProduct.tprod R) = φ → φ' = PiTensorProduct.lift φ
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.mk.injEq : ∀ (lctx : Lean.LocalContext) (expr : Lean.Expr) (ref : Lean.Syntax) (msgData? : Option Lean.MessageData)
  (lctx_1 : Lean.LocalContext) (expr_1 : Lean.Expr) (ref_1 : Lean.Syntax) (msgData?_1 : Option Lean.MessageData),
  ({ lctx := lctx, expr := expr, ref := ref, msgData? := msgData? } =
      { lctx := lctx_1, expr := expr_1, ref := ref_1, msgData? := msgData?_1 }) =
    (lctx = lctx_1 ∧ expr = expr_1 ∧ ref = ref_1 ∧ msgData? = msgData?_1)
-- Mathlib.Data.Finset.Density
Finset.nnratCast_dens : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : Semifield 𝕜] [CharZero 𝕜] (s : Finset α),
  ↑s.dens = ↑s.card / ↑(Fintype.card α)
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Uniqueness part of **Sylvester's law of inertia** (negative part):
for any weighted sum of squares equivalent to `Q`,
the number of strictly negative weights is equal to `sigNeg Q`.  -/
QuadraticForm.sigNeg_of_equiv_weightedSumSquares : ∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_4} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : Module 𝕜 M] {Q : QuadraticForm 𝕜 M} {ι : Type u_5} [inst_4 : Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜],
  QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w) → sigNeg Q = {i | w i < 0}.ncard
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mk_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.MonoOver.mk f).obj.left = A
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRightHom.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4),
  TensorProduct.piScalarRightHom R S N ι =
    TensorProduct.AlgebraTensorModule.lift (TensorProduct.piScalarRightHomBil R S N ι)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.contains (t.minKey he) = true
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n), Module.End.HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the counit is an isomorphism, then the right adjoint is fully faithful.  -/
CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → [CategoryTheory.IsIso h.counit] → R.FullyFaithful
-- Mathlib.Algebra.Ring.Int.Defs
Int.instRing : Ring ℤ
-- Mathlib.Analysis.CStarAlgebra.Classes
instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal : {A : Type u_1} → [inst : CStarAlgebra A] → (x : A) → [IsStarNormal x] → CommCStarAlgebra ↥(StarAlgebra.elemental ℂ x)
-- Mathlib.NumberTheory.Height.Basic
/-- The `totalWeight` of a field with `AdmissibleAbsValues` is the sum of the multiplicities of
the archimedean places.  -/
Height.totalWeight : (K : Type u_1) → [inst : Field K] → [Height.AdmissibleAbsValues K] → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_nat_mul_two_pi : ∀ (x : ℝ) (n : ℕ), Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  StrictConcaveOn 𝕜 s f → StrictConcaveOn 𝕜 s g → StrictConcaveOn 𝕜 s (f + g)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.natZExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.Algebra.Group.Even
isSquare_op_iff : ∀ {α : Type u_2} [inst : Mul α] {a : α}, IsSquare (MulOpposite.op a) ↔ IsSquare a
-- Aesop.Tree.Data
Aesop.GoalUnsafe : Type
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- Pick a presentation of an ind-object `X` using choice.  -/
CategoryTheory.Ind.presentation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.Ind C) → CategoryTheory.Limits.IndObjectPresentation ((CategoryTheory.Ind.inclusion C).obj X)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.eq_comp_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (f : β → α) (g : α → α), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roc_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toList[i]? = none ↔ (n - m).toNat ≤ i
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.list_prod_singleton : ∀ {M : Type u_5} [inst : Monoid M] (s : List M), (List.map (fun i => {i}) s).prod = {s.prod}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G),
  CategoryTheory.CategoryStruct.comp f g⁻¹ = (CategoryTheory.CategoryStruct.comp f g)⁻¹
-- Init.Data.List.Basic
List.instDecidableMemOfLawfulBEq : {α : Type u} → [inst : BEq α] → [LawfulBEq α] → (a : α) → (as : List α) → Decidable (a ∈ as)
-- Mathlib.Algebra.Notation.Prod
Prod.fst_inv : ∀ {G : Type u_8} {H : Type u_9} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.1 = p.1⁻¹
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryFin0_symm_apply_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (x : G') (v : Fin 0 → G),
  ((continuousMultilinearCurryFin0 𝕜 G G').symm x) v = x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_union : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  Disjoint s₁ s₂ → ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_and_prime_pow_iff_prime : ∀ {n : ℕ}, Squarefree n ∧ IsPrimePow n ↔ Nat.Prime n
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.eq' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S},
  f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (AddLocalization.r S) (a₁, a₂) (b₁, b₂)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Number of non-star matches so far  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.score : Lean.Meta.RefinedDiscrTree.PartialMatch✝ → ℕ
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mk.injEq : ∀ {α : Type u} [inst : AddMonoid α] (val neg : α) (val_neg : val + neg = 0) (neg_val : neg + val = 0) (val_1 neg_1 : α)
  (val_neg_1 : val_1 + neg_1 = 0) (neg_val_1 : neg_1 + val_1 = 0),
  ({ val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
      { val := val_1, neg := neg_1, val_neg := val_neg_1, neg_val := neg_val_1 }) =
    (val = val_1 ∧ neg = neg_1)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.mk.injEq : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (I : Set J)
  (left : autoParam (i ∈ I) CategoryTheory.SimplicialThickening.Path.left._autoParam)
  (right : autoParam (j ∈ I) CategoryTheory.SimplicialThickening.Path.right._autoParam)
  (left_le : autoParam (∀ k ∈ I, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam)
  (le_right : autoParam (∀ k ∈ I, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam) (I_1 : Set J)
  (left_1 : autoParam (i ∈ I_1) CategoryTheory.SimplicialThickening.Path.left._autoParam)
  (right_1 : autoParam (j ∈ I_1) CategoryTheory.SimplicialThickening.Path.right._autoParam)
  (left_le_1 : autoParam (∀ k ∈ I_1, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam)
  (le_right_1 : autoParam (∀ k ∈ I_1, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam),
  ({ I := I, left := left, right := right, left_le := left_le, le_right := le_right } =
      { I := I_1, left := left_1, right := right_1, left_le := left_le_1, le_right := le_right_1 }) =
    (I = I_1)
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.subsetSum_erase_zero : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M}, (A.erase 0).subsetSum = A.subsetSum
-- Init.Data.Int.DivMod.Lemmas
Int.fmod.eq_2 : ∀ (m n : ℕ), (m = 0 → False) → (Int.ofNat m).fmod (Int.ofNat n) = Int.ofNat (m % n)
-- Mathlib.Order.Fin.Finset
/-- This is the order isomorphism from `Fin 1` to a finset `{a}`.  -/
Fin.orderIsoSingleton : {α : Type u_1} → [inst : Preorder α] → (a : α) → Fin 1 ≃o ↥{a}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.instCategory : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                CategoryTheory.Category.{max v₃ v₁, max (max u₃ u₁) v₂} (CategoryTheory.Limits.CategoricalPullback F G)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_eq_toNat_relrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  A.relfinrank B = Cardinal.toNat (A.relrank B)
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.addCommute_iff_add_neg_cancel : ∀ {M : Type u_1} [inst : AddMonoid M] {u : AddUnits M} {a : M}, AddCommute (↑u) a ↔ ↑u + a + ↑(-u) = a
-- Init.Data.List.Basic
List.zip_cons_cons : ∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1},
  (a :: as).zip (b :: bs) = (a, b) :: as.zip bs
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey.mk.sizeOf_spec : ∀ (expr : Lean.Expr), sizeOf { expr := expr } = 1 + sizeOf expr
-- Mathlib.Order.BooleanAlgebra.Basic
compl_lt_compl_iff_lt : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], yᶜ < xᶜ ↔ x < y
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_sub : ∀ {K : Type u} [inst : CommRing K] (p q : FractionRing (Polynomial K)),
  { toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }
-- Mathlib.Algebra.Group.Basic
right_eq_add : ∀ {M : Type u_4} [inst : AddMonoid M] [IsRightCancelAdd M] {a b : M}, b = a + b ↔ a = 0
-- Mathlib.Order.Sublattice
Sublattice.comap_id : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), Sublattice.comap (LatticeHom.id α) L = L
-- Mathlib.Topology.Connected.Basic
isPreconnected_empty : ∀ {α : Type u} [inst : TopologicalSpace α], IsPreconnected ∅
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ClearInsertInductionMotive.congr_simp : ∀ {n : ℕ} (f f_1 : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (e_f : f = f_1)
  (assignments_size : f.assignments.size = n)
  (units units_1 : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
  units = units_1 →
    ∀ (a a_1 : ℕ),
      a = a_1 →
        ∀ (a_2 a_3 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
          a_2 = a_3 →
            f.ClearInsertInductionMotive assignments_size units a a_2 = f_1.ClearInsertInductionMotive ⋯ units_1 a_1 a_3
-- Mathlib.Algebra.Notation.Prod
Prod.swap_neg : ∀ {G : Type u_8} {H : Type u_9} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).swap = -p.swap
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
factors in `S` as `∏ i, P i ^ e i`, then `S ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`.  -/
Ideal.Factors.piQuotientEquiv : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : IsDedekindDomain S] →
            (p : Ideal R) →
              Ideal.map (algebraMap R S) p ≠ ⊥ →
                S ⧸ Ideal.map (algebraMap R S) p ≃+*
                  ((P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset) →
                    S ⧸ ↑P ^ p.ramificationIdx' ↑P)
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn.go : {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u} →
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
    {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
      {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} →
        (t : Mathlib.Tactic.Translate.ArgReorder) →
          ((t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t) →
            ((t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t) →
              ((t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                  Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t) →
                ((t : ℕ × Mathlib.Tactic.Translate.ArgReorder) →
                    Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t) →
                  motive_1 t ×' t.below
-- LeanSearchClient.Syntax
LeanSearchClient.queryStateSearch : String → ℕ → String → Lean.MetaM (Array LeanSearchClient.SearchResult)
-- Mathlib.Algebra.Algebra.Operations
/-- A dependent version of `mul_induction_on`.  -/
Submodule.mul_induction_on' : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {M N : Submodule R A} {C : (r : A) → r ∈ M * N → Prop},
  (∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯) →
    (∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯) →
      ∀ {r : A} (hr : r ∈ M * N), C r hr
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {P Q : TopCat.Presheaf C X} {f g : P ⟶ Q},
  f = g ↔ ∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.mk_singleton_self : ∀ {R : Type u_3} [inst : Ring R] (x : R) [inst_1 : (Ideal.span {x}).IsTwoSided],
  (Ideal.Quotient.mk (Ideal.span {x})) x = 0
-- Mathlib.Order.Interval.Set.Infinite
Set.instInfiniteElemIioOfNoMinOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] {a : α}, Infinite ↑(Set.Iio a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.range_cos_infinite : (Set.range Real.cos).Infinite
-- Mathlib.Topology.Algebra.Star.LinearMap
/-- The involutive intrinsic star structure on continuous linear maps.  -/
ContinuousLinearMap.intrinsicInvolutiveStar : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] →
                      [inst_8 : StarAddMonoid F] →
                        [StarModule R F] →
                          [inst_10 : TopologicalSpace E] →
                            [inst_11 : TopologicalSpace F] →
                              [ContinuousStar E] → [ContinuousStar F] → InvolutiveStar (WithConv (E →L[R] F))
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset β} {a : α},
  a +ᵥ s₁ ∩ s₂ ⊆ (a +ᵥ s₁) ∩ (a +ᵥ s₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.RepresentationTheory.Maschke
MonoidAlgebra.Submodule.instIsSemisimpleRepresentation : ∀ {G : Type u_5} {k : Type u_6} {V : Type u_7} [inst : Group G] [inst_1 : Field k] [Finite G] [NeZero ↑(Nat.card G)]
  [inst_4 : AddCommGroup V] [inst_5 : Module k V] (ρ : Representation k G V), ρ.IsSemisimpleRepresentation
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.dual_isLoop_iff_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M✶.IsLoop e ↔ M.IsColoop e
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `f : X ⟶ Y` is an open immersion, then `X` is isomorphic to its image in `Y`.  -/
AlgebraicGeometry.Scheme.Hom.isoOpensRange : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [inst : AlgebraicGeometry.IsOpenImmersion f] → X ≅ ↑(AlgebraicGeometry.Scheme.Hom.opensRange f)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.instIsContinuousOfPreservesOneHypercovers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.PreservesOneHypercovers J K], F.IsContinuous J K
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator : (α : Type) →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) →
        [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] → Prop
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Variables that come from a lambda or forall binder.
The list index gives the De Bruijn index.  -/
Lean.Meta.RefinedDiscrTree.ExprInfo.bvars : Lean.Meta.RefinedDiscrTree.ExprInfo → List Lean.FVarId