mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Indicator
norm_indicator_le_of_subset : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {s t : Set α},
  s ⊆ t → ∀ (f : α → E) (a : α), ‖s.indicator f a‖ ≤ ‖t.indicator f a‖
-- Mathlib.MeasureTheory.Order.Lattice
/-- **Alias** of `Measurable.inf`. -/
Measurable.inf' : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Min M]
  [MeasurableInf₂ M], Measurable f → Measurable g → Measurable (f ⊓ g)
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Iic : ∀ {n : ℕ} (b : Fin n), (Finset.Iic b).card = ↑b + 1
-- Mathlib.Data.Num.Bitwise
SNum.nz.inj : ∀ {a a_1 : NzsNum}, SNum.nz a = SNum.nz a_1 → a = a_1
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The set of comparisons.  -/
Mathlib.Tactic.Linarith.LinarithData.comps : Mathlib.Tactic.Linarith.LinarithData → Mathlib.Tactic.Linarith.PCompSet
-- Lean.Data.Lsp.Extra
/-- Build dependencies once, but then do not build them again on import changes / crashes. Used for `didOpen` notifications that are explicitly intended for manually triggering the build.  -/
Lean.Lsp.DependencyBuildMode.once : Lean.Lsp.DependencyBuildMode
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.zero_inv : ∀ {k : Type u_2} [inst : Field k], 0⁻¹ = 0
-- Init.Data.List.Pairwise
List.Pairwise.tail : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l → List.Pairwise R l.tail
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_pow_right`. -/
Equiv.Perm.SameCycle.of_pow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x ((f ^ n) y) → f.SameCycle x y
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.fibration_iff : ∀ {X Y : SSet} (f : X ⟶ Y), HomotopicalAlgebra.Fibration f ↔ SSet.modelCategoryQuillen.J.rlp f
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_pair : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {x y : α}, {x, y}.infsep = dist x y
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_counitIso_hom_app_hom_toFun : ∀ (X : TwoP) (a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X),
  (TwoP.swapEquiv.counitIso.hom.app X).hom.toFun a = a
-- Mathlib.RingTheory.Localization.NormTrace
Algebra.map_leftMulMatrix_localization : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
  (M : Submonoid R) [inst_7 : IsLocalization M Rₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  [inst_9 : Algebra Rₘ Sₘ] [inst_10 : Algebra R Sₘ] [inst_11 : IsScalarTower R Rₘ Sₘ] [inst_12 : IsScalarTower R S Sₘ]
  {ι : Type u_5} [inst_13 : Fintype ι] [inst_14 : DecidableEq ι] (b : Module.Basis ι R S) (a : S),
  (algebraMap R Rₘ).mapMatrix ((Algebra.leftMulMatrix b) a) =
    (Algebra.leftMulMatrix (Module.Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete
CategoryTheory.Codiscrete.equivFun_symm_apply_obj_as : ∀ {X : Type u} {n : ℕ} (f : Fin (n + 1) → X) (k : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)),
  ((CategoryTheory.Codiscrete.equivFun.symm f).obj k).as = f k
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Number of steps performed so far.  -/
Lean.Meta.Sym.DSimp.State.numSteps : Lean.Meta.Sym.DSimp.State → ℕ
-- Mathlib.Probability.Kernel.Proper
/-- Auxiliary lemma for `IsProper.lintegral_mul` and
`IsProper.setLIntegral_eq_indicator_mul_lintegral`.  -/
_private.Mathlib.Probability.Kernel.Proper.0.ProbabilityTheory.Kernel.IsProper.lintegral_indicator_mul_indicator : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {A B : Set X} {x₀ : X},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      MeasurableSet A →
        MeasurableSet B →
          ∫⁻ (x : X), B.indicator 1 x * A.indicator 1 x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_sub : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : (Fin n → ℂ) → E}
  {c : Fin n → ℂ} {R : Fin n → ℝ},
  TorusIntegrable f c R →
    TorusIntegrable g c R →
      (∯ (x : Fin n → ℂ) in T(c, R), f x - g x) =
        (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_2 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w) (curr_2 : ℕ),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr_2.succ n d wn wr q r =
    {
      aig :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).aig,
      q :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).q,
      r :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).r,
      hle := ⋯ }
-- Mathlib.RingTheory.Ideal.Maps
Ideal.orderEmbeddingOfSurjective_apply : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (hf : Function.Surjective ⇑f) (I : Ideal S),
  (Ideal.orderEmbeddingOfSurjective f hf) I = Ideal.comap f I
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
_private.Mathlib.MeasureTheory.Function.ConvergenceInMeasure.0.MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_or_left_inj : ∀ {m x y : ℕ}, m &&& x = m &&& y ∧ m ||| x = m ||| y ↔ x = y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [Std.LawfulEqOrd α] [inst : Inhabited γ] {f : α → β → γ} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.map f t) k =
      (Option.map (f k) (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyoneda_obj_obj_coe : ∀ (M : CommMonCatᵒᵖ) (N : CommMonCat), ↑((CommMonCat.coyoneda.obj M).obj N) = (↑(Opposite.unop M) →* ↑N)
-- Mathlib.Topology.Order.Bornology
isOrderBornology_iff_eq_orderBornology : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Lattice α] [inst_2 : Nonempty α],
  IsOrderBornology α ↔ inst = orderBornology
-- Mathlib.Algebra.Algebra.Hom
/-- The algebra morphism underlying `algebraMap`.  -/
Algebra.algHom : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] → [inst_4 : Algebra S A] → [inst_5 : Algebra R A] → [IsScalarTower R S A] → S →ₐ[R] A
-- Lean.Parser.Extra
Lean.Parser.nodeWithAntiquot.parenthesizer : String → Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Term
/-- Helper parser for marking `match`-alternatives that should not trigger errors if unused.
We use them to implement `macro_rules` and `elab_rules`
 -/
Lean.Parser.Term.noErrorIfUnused : Lean.Parser.Parser
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ {i₂ i₂' : I₂},
      c₂.Rel i₂ i₂' →
        ∀ (j : J),
          c₁.π c₂ c (i₁', i₂) = j →
            c₁.ε₁ c₂ c (i₁, i₂) •
                CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
                  (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
                    ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) =
              -CategoryTheory.CategoryStruct.comp
                  ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j))
                  (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanGroup.is_nonarchimedean : ∀ {G : Type u_1} {inst : Group G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanGroup G],
  ∀ U ∈ nhds 1, ∃ V, ↑V ⊆ U
-- Mathlib.Algebra.Group.TransferInstance
Equiv.commMonoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : CommMonoid β],
  e.commMonoid = Function.Injective.commMonoid ⇑e ⋯ ⋯ ⋯ ⋯
-- Init.Data.Order.Ord
Std.LawfulEqOrd.eq_of_compare : ∀ {α : Type u} [inst : Ord α] [Std.LawfulEqOrd α] {a b : α}, compare a b = Ordering.eq → a = b
-- Mathlib.Algebra.Star.StarAlgHom
/-- The first projection of a product is a non-unital ⋆-algebra homomorphism.  -/
NonUnitalStarAlgHom.fst : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : Star B] → A × B →⋆ₙₐ[R] A
-- Mathlib.FieldTheory.LinearDisjoint
/-- Two intermediate fields are linearly disjoint if and only if
they are linearly disjoint as subalgebras.  -/
IntermediateField.linearDisjoint_iff' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B ↔ A.LinearDisjoint B.toSubalgebra
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- `Matrix.invertibleOfFromBlocks₂₂Invertible` and `Matrix.fromBlocks₂₂Invertible` as an
equivalence.  -/
Matrix.invertibleEquivFromBlocks₂₂Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible D] → Invertible (Matrix.fromBlocks A B C D) ≃ Invertible (A - B * ⅟D * C)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_inv : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.zpowers g⁻¹ = Subgroup.zpowers g
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_zero : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), f 0 = 0
-- Mathlib.AlgebraicGeometry.Group.Abelian
AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed : ∀ {K : Type u} [inst : Field K] [IsAlgClosed K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K)))
  [AlgebraicGeometry.IsProper G.hom]
  [AlgebraicGeometry.IsIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj G G).left]
  [inst_4 : CategoryTheory.GrpObj G], CategoryTheory.IsCommMonObj G
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.isCoprime_of_ne : ∀ {R : Type u_1} [inst : CommSemiring R] {I J : MaximalSpectrum R}, I ≠ J → IsCoprime I.asIdeal J.asIdeal
-- Mathlib.FieldTheory.Normal.Closure
/-- An extension `L/F` in which every minimal polynomial of `K/F` splits is maximal with respect
to `F`-embeddings of `K`, in the sense that `K →ₐ[F] L` achieves maximal cardinality.
We construct an explicit injective function from an arbitrary `K →ₐ[F] L'` into `K →ₐ[F] L`,
using an embedding of `normalClosure F K L'` into `L`.  -/
Algebra.IsAlgebraic.algHomEmbeddingOfSplits : {F : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F L] →
                [Algebra.IsAlgebraic F K] →
                  (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
                    (L' : Type u_4) → [inst_6 : Field L'] → [inst_7 : Algebra F L'] → (K →ₐ[F] L') ↪ K →ₐ[F] L
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.eq_1 : ∀ (n : ℕ) (R : Type u_1) [inst : CommSemiring R], Ring.KrullDimLE n R = Order.KrullDimLE n (PrimeSpectrum R)
-- Init.Data.Nat.Lemmas
Nat.pow_mul : ∀ (a m n : ℕ), a ^ (m * n) = (a ^ m) ^ n
-- Mathlib.Tactic.TFAE
/-- Attempt to prove `getLastD l P' → P` given an explicit list `l`.  -/
Mathlib.Tactic.TFAE.proveGetLastDImpl : Array (ℕ × ℕ × Lean.Expr) →
  Array Q(Prop) → ℕ → ℕ → List ℕ → (P P' : Q(Prop)) → (l : Q(List Prop)) → Lean.MetaM Q(«$l».getLastD «$P'» → «$P»)
-- Mathlib.Data.Fintype.EquivFin
Function.RightInverse.leftInverse_of_card_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {f : α → β} {g : β → α},
  Function.RightInverse f g → Fintype.card β ≤ Fintype.card α → Function.LeftInverse f g
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The identity modification.  -/
CategoryTheory.Lax.OplaxTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (η : F ⟶ G) → CategoryTheory.Lax.OplaxTrans.Modification η η
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- **Alias** of `Matroid.IsBasis'.cardinalMk_sdiff_comm`. -/
Matroid.IsBasis'.cardinalMk_diff_comm : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis' I X → M.IsBasis' J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Init.Data.Order.Lemmas
Std.LawfulOrderLeftLeaningMax.of_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [inst_2 : DecidableLE α],
  (∀ (a b : α), a ⊔ b = if b ≤ a then a else b) → Std.LawfulOrderLeftLeaningMax α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel morphism of a monomorphism is a zero morphism  -/
CategoryTheory.Limits.kernel.ι_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [CategoryTheory.Mono f], CategoryTheory.Limits.kernel.ι f = 0
-- Mathlib.Data.Int.Order.Units
Int.sq_eq_one_of_sq_lt_four : ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Right unitality of the enriched structure  -/
CategoryTheory.MonoidalClosed.comp_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y] {Z : C} (h : x ⟹ y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (x ⟹ y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (x ⟹ y) (CategoryTheory.MonoidalClosed.id y))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp x y y) h)) =
    h
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep_iff_IndepSets : ∀ {Ω : Type u_1} (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.Indep m₁ m₂ μ ↔ ProbabilityTheory.IndepSets {s | MeasurableSet s} {s | MeasurableSet s} μ
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- Relation between the resultant and the discriminant.

(Note this is actually false when `f` is a constant polynomial not equal to 1, so the assumption on
the degree is genuinely needed.)  -/
Polynomial.resultant_deriv : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  0 < f.degree →
    f.resultant (Polynomial.derivative f) f.natDegree (f.natDegree - 1) =
      (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_addUnits_iff_val_mem : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) (x : AddUnits G), x ∈ H.addUnits ↔ ↑x ∈ H
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂_mono : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ g₁ : α₁ → β₁ → Finset γ₁} {f₂ g₂ : α₂ → β₂ → Finset γ₂},
  (∀ (a : α₁) (b : β₁), f₁ a b ⊆ g₁ a b) →
    (∀ (a : α₂) (b : β₂), f₂ a b ⊆ g₂ a b) →
      ∀ (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂), Finset.sumLift₂ f₁ f₂ a b ⊆ Finset.sumLift₂ g₁ g₂ a b
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_ofNatMultiset : ∀ (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p), ↑(PrimeMultiset.ofNatMultiset v h).prod = v.prod
-- Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R},
  (∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) → Submodule.IsPrincipal J
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv_comp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃),
  (CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) f)
          ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) g))
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃))
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_induction : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  {p : α → Prop}, p ⊥ → (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) → (∀ b ∈ s, p (f b)) → p (s.sup f)
-- Mathlib.LinearAlgebra.DFinsupp
/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom` composed with `DFinsupp.filter_add_monoid_hom`; that is, every element in the
bounded `iSup` can be produced from taking a finite number of non-zero elements from the `S i` that
satisfy `p i`, coercing them to `γ`, and summing them.  -/
Submodule.biSup_eq_range_dfinsupp_lsum : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Prop) [inst_4 : DecidablePred p] (S : ι → Submodule R N),
  ⨆ i, ⨆ (_ : p i), S i =
    (((DFinsupp.lsum ℕ) fun i => (S i).subtype) ∘ₗ DFinsupp.filterLinearMap R (fun i => ↥(S i)) p).range
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The image of a measurable set under an antitone map is measurable.  -/
MeasurableSet.image_of_antitoneOn : ∀ {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
  [BorelSpace α] [inst_3 : LinearOrder α] [OrderTopology α] [PolishSpace α] [inst : TopologicalSpace β]
  [inst_5 : MeasurableSpace β] [BorelSpace β] [inst_7 : LinearOrder β] [OrderTopology β] [SecondCountableTopology β],
  MeasurableSet t → AntitoneOn g t → MeasurableSet (g '' t)
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.mk : Lean.Name → ℕ → ℕ → ℕ → ℕ → Lean.IR.CtorInfo
-- Mathlib.Analysis.Complex.CoveringMap
Complex.isCoveringMapOn_exp : IsCoveringMapOn Complex.exp {0}ᶜ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.isReduced_iff_not_step : ∀ {α : Type u} {L₁ : List (α × Bool)},
  FreeAddGroup.IsReduced L₁ ↔ ∀ (L₂ : List (α × Bool)), ¬FreeAddGroup.Red.Step L₁ L₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_mem_cycles₂_iff_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G × G) (a : ↑A),
  (fun₀ | g => a) ∈ groupHomology.cycles₂ A ↔ ((fun₀ | g.2 => (A.ρ g.1⁻¹) a) + fun₀ | g.1 => a) = fun₀ | g.1 * g.2 => a
-- Init.Grind.ToInt
/-- The embedding is strictly monotone with respect to `<`.  -/
Lean.Grind.ToInt.LT.lt_iff : ∀ {α : Type u} {inst : LT α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.LT α I] (x y : α), x < y ↔ ↑x < ↑y
-- Init.Data.UInt.Lemmas
UInt64.toUSize_mod_of_dvd : ∀ (a b : UInt64), b.toNat ∣ 4294967296 → (a % b).toUSize = a.toUSize % b.toUSize
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Day.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subDays : Std.Time.WallTime → Std.Time.Day.Offset → Std.Time.WallTime
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_conjTranspose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R},
  Summable f L → Summable (fun x => (f x).conjTranspose) L
-- Lean.Level
Lean.Level.mvar.sizeOf_spec : ∀ (a : Lean.LMVarId), sizeOf (Lean.Level.mvar a) = 1 + sizeOf a
-- Init.Omega.Int
Lean.Omega.Fin.ofNat_val_mul : ∀ {n : ℕ} {x y : Fin n}, ↑↑(x * y) = ↑↑x * ↑↑y % ↑n