mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality_faithful : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Faithful], (CategoryTheory.Limits.Cocone.functoriality F G).Faithful
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β),
  MeasureTheory.AEEqFun.comp g hg f = MeasureTheory.AEEqFun.mk (g ∘ ↑f) ⋯
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN : {α : Type u_1} → [Lean.Grind.NatModule α] → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Expr → α
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.ofIso_target : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ≅ Y), (AlgebraicGeometry.Scheme.PartialIso.ofIso f).target = ⊤
-- Mathlib.Algebra.Order.Group.Synonym
pow_ofDual : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : βᵒᵈ), a ^ OrderDual.ofDual b = a ^ b
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- `-1` is a square in `F` iff `#F` is not congruent to `3` mod `4`.  -/
FiniteField.isSquare_neg_one_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
-- Aesop.BaseM
Aesop.BaseM.instInhabitedState.default : Aesop.BaseM.State
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv =
    X.πE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.isScalarTower_mid : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {R : Type u_4} [inst_3 : Semiring R] [inst_4 : Algebra L R] [inst_5 : Algebra K R] [IsScalarTower K L R],
  IsScalarTower K (↥S) R
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] Set.univ → s ∪ t =ᵐ[μ] Set.univ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingHom.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S),
  MonoidAlgebra.mapRingHom M f =
    { toFun := MonoidAlgebra.map ↑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.exists_add_spanSingleton_mul_eq : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal (nonZeroDivisors R) K},
  a ≤ c → a ≠ 0 → b ≠ 0 → ∃ x, a + FractionalIdeal.spanSingleton (nonZeroDivisors R) x * b = c
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_of_analyticOn_iteratedFDerivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, (∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) → ContDiffOn 𝕜 n f s
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_principal_eq_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), (Filter.principal s).limsInf = sInf s
-- Std.Time.Format.DateFormat
/-- Short extended-day-period strings for the `B` pattern (CLDR flexible day periods).
Order: midnight, night, morning, noon, afternoon, evening.
 -/
Std.Time.DateFormatSymbols.extendedDayPeriodShort : Std.Time.DateFormatSymbols → Vector String 6
-- Mathlib.Algebra.Order.Field.Basic
div_mul_le_div_mul_of_div_le_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b c d e : α}
  [IsStrictOrderedRing α], a / b ≤ c / d → 0 ≤ e → a / (b * e) ≤ c / (d * e)
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_mapDomain : ∀ {σ : Type u_1} {M : Type u_2} {τ : Type u_5} (f : σ → τ) [inst : AddCommMonoid M] (x : σ →₀ M),
  Finsupp.degree (Finsupp.mapDomain f x) = Finsupp.degree x
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Relation between the fiber functors on presheaves for the points `Φ.map F K`
and `Φ` when `F : C ⥤ D` is a cocontinuous and continuous functor between
sites `(C, J)` and `(D, K)`.  -/
CategoryTheory.GrothendieckTopology.Point.sheafFiberMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [inst_2 : F.IsCocontinuous J K] →
                  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] →
                    (A : Type u'') →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          [inst_6 : F.IsContinuous J K] →
                            (Φ.map F K).sheafFiber ≅ (F.sheafPushforwardContinuous A J K).comp Φ.sheafFiber
-- Init.Data.Array.Basic
/-- Applies the monadic action `f` to each element of an array from right to left, in reverse order.

The optional parameters `start` and `stop` control the region of the array to which `f` should be
applied. Iteration proceeds from `start` (exclusive) to `stop` (inclusive), so no `f` is not invoked
unless `start > stop`. By default, the entire array is used.
 -/
Array.forRevM : {α : Type u} →
  {m : Type v → Type w} →
    [Monad m] → (α → m PUnit.{v + 1}) → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m PUnit.{v + 1}
-- Mathlib.Order.Interval.Multiset
Multiset.nodup_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, (Multiset.Ioo a b).Nodup
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.mkEMatchTheoremUsingSingletonPatterns.go : Array Lean.Expr → Lean.Expr → StateT (Array (Lean.Expr × List Lean.HeadIndex)) Lean.Meta.Grind.CollectorM✝ Unit
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_cast_neg : ∀ {n : ℕ} (x : ZMod n), (-x).cast = -x.cast % ↑n
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddCommMonCat.instIsLeftAdjointFree : AddCommMonCat.free.IsLeftAdjoint
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.mul_log_strictAntiOn : StrictAntiOn (fun x => x * Real.log x) (Set.Icc 0 (Real.exp (-1)))
-- Init.Try
/-- Helper internal tactic used to implement `evalSuggest` in `try?`  -/
Lean.Parser.Tactic.tryResult : Lean.ParserDescr
-- Mathlib.Data.Finsupp.Basic
Finsupp.uncurry.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α →₀ β →₀ M),
  f.uncurry =
    { support := f.support.disjiUnion (fun a => Finset.map (Function.Embedding.sectR a β) (f a).support) ⋯,
      toFun := fun x => (f x.1) x.2, mem_support_toFun := ⋯ }
-- Mathlib.Order.Basic
Prod.mk_le_mk_iff_left : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b : β},
  (a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
le_add_iff_lt_right_or_exists_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α]
  [IsLeftCancelAdd α], a ≤ b + c ↔ a < c ∨ ∃ d ≤ b, a = d + c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) h)
-- Mathlib.RingTheory.Fintype
Finset.univ_of_card_le_two : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Fintype R] [inst_2 : DecidableEq R],
  Fintype.card R ≤ 2 → Finset.univ = {0, 1}
-- Mathlib.Probability.Kernel.Disintegration.Density
/-- Density of the kernel `κ` with respect to `ν`. This is a function `α → γ → Set β → ℝ` which
is measurable on `α × γ` for all measurable sets `s : Set β` and satisfies that
`∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s)` for all measurable `A : Set γ`.  -/
ProbabilityTheory.Kernel.density : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            [MeasurableSpace.CountablyGenerated γ] →
              ProbabilityTheory.Kernel α (γ × β) → ProbabilityTheory.Kernel α γ → α → γ → Set β → ℝ
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.inductive_claim_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {k : ℝ} {m : ℕ},
  3 ≤ m →
    (∀ (ε : Fin 3 → ℤ),
        (∀ (i : Fin 3), |ε i| = 1) → ↑(List.map (fun i => A ^ ε i) (List.finRange 3)).prod.card ≤ k * ↑A.card) →
      ∀ (ε : Fin m → ℤ),
        (∀ (i : Fin m), |ε i| = 1) → ↑(List.map (fun i => A ^ ε i) (List.finRange m)).prod.card ≤ k ^ (m - 2) * ↑A.card
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.of_precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι' : Type u_6} {g : ι' → ι}
  {β : ι → Type u_7} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  Function.Surjective g → ProbabilityTheory.iIndepFun (fun i => f (g i)) μ → ProbabilityTheory.iIndepFun f μ
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMulOneClass.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitMulOneClass F = { one := One.one, mul := Mul.mul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.neighborSet_map : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (f : V ↪ W) (v : V),
  (SimpleGraph.map (⇑f) G).neighborSet (f v) = ⇑f '' G.neighborSet v
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.linearMap_comp_rid : ∀ (R : Type uR) (S : Type uS) {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  ↑R (Algebra.linearMap S (TensorProduct R S B)) ∘ₗ (Algebra.TensorProduct.rid R R S).toLinearMap =
    LinearMap.lTensor S (Algebra.linearMap R B)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listL.eq_3 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (parent : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right c l v parent).listL = parent.listL ++ (l.toList ++ [v])
-- Mathlib.Data.Set.Finite.Lattice
Set.Infinite.sUnion : ∀ {α : Type u} {s : Set (Set α)}, s.Infinite → (⋃₀ s).Infinite
-- Mathlib.Data.Set.Finite.Basic
Set.finite_preimage_inl_and_inr : ∀ {α : Type u} {β : Type v} {s : Set (α ⊕ β)}, (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite
-- Mathlib.Algebra.Ring.Parity
Nat.succ_mod_two_add_mod_two : ∀ (m : ℕ), (m + 1) % 2 + m % 2 = 1
-- Lean.Elab.Tactic.Omega.Core
/-- Prepare the Fourier-Motzkin elimination data for each variable.  -/
Lean.Elab.Tactic.Omega.Problem.fourierMotzkinData : Lean.Elab.Tactic.Omega.Problem → Array Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.strongAnodyneExtensions_ι_iff : ∀ {X : SSet} (A : X.Subcomplex), SSet.strongAnodyneExtensions A.ι ↔ ∃ P, P.IsRegular
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_abs : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {β : Type u_5} [inst_1 : TopologicalSpace β]
  [inst_2 : Lattice β] [inst_3 : TopologicalLattice β] [inst_4 : AddGroup β] [inst_5 : IsTopologicalAddGroup β]
  (f : α →ₘ[μ] β), ↑|f| =ᵐ[μ] fun x => |↑f x|
-- Mathlib.Algebra.Algebra.Basic
/-- If `R →+* S` is surjective, then `S`-linear maps between modules are exactly `R`-linear maps.  -/
LinearMap.extendScalarsOfSurjectiveEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            {N : Type u_4} →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module S M] →
                      [IsScalarTower R S M] →
                        [inst_8 : Module R N] →
                          [inst_9 : Module S N] →
                            [inst_10 : IsScalarTower R S N] →
                              Function.Surjective ⇑(algebraMap R S) → (M →ₗ[R] N) ≃ₗ[R] M →ₗ[S] N
-- Mathlib.Data.Set.Card
Set.Infinite.encard_eq : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.encard = ⊤
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d').hom
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_neg_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y : M),
  QuadraticMap.polar (⇑Q) x (-y) = -QuadraticMap.polar (⇑Q) x y
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.equalCommonLMVars? : Lean.LMVarId → Lean.LMVarId → Aesop.EqualUpToIdsM (Option Bool)
-- Mathlib.LinearAlgebra.Prod
Submodule.map_inl : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M), Submodule.map (LinearMap.inl R M M₂) p = p.prod ⊥
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.exists_enc_dec : ∀ {Γ : Type u_1} [inst : Inhabited Γ] [Finite Γ],
  ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.stalkIso_inv : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥U),
  (U.stalkIso x).inv = AlgebraicGeometry.Scheme.Hom.stalkMap U.ι x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial]
  (x : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cocycles₁IsoOfIsTrivial A).hom) x
-- Mathlib.RingTheory.Ideal.NatInt
Nat.one_mem_closure_iff : ∀ {s : Set ℕ}, 1 ∈ AddSubmonoid.closure s ↔ 1 ∈ s
-- Mathlib.Algebra.Ring.Semireal.Defs
/-- In a semireal ring, `-1` is not a sum of squares.  -/
IsSemireal.not_isSumSq_neg_one : ∀ (R : Type u_1) [inst : AddGroup R] [inst_1 : One R] [inst_2 : Mul R] [IsSemireal R], ¬IsSumSq (-1)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.comp_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (Q : QuadraticMap R N P) (f : M →ₗ[R] N) (x : M), (Q.comp f) x = Q (f x)
-- Mathlib.Order.Circular
CircularPreorder.toBtw : {α : Type u_1} → [self : CircularPreorder α] → Btw α
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {X_1 Y : CategoryTheory.ComposableArrows ι 2} (φ : X_1 ⟶ Y),
  (X.ω₂.map φ).hom₂ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app ⟨2, ⋯⟩) ⋯)
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State : Type
-- Lean.HeadIndex
Lean.HeadIndex.lit : Lean.Literal → Lean.HeadIndex
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isSkewAdjoint_iff_neg_self_adjoint : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : M → M),
  B.IsSkewAdjoint f ↔ (-B).IsAdjointPair B f f
-- Init.Data.List.Lemmas
List.isEmpty_iff_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.isEmpty = true ↔ l.length = 0
-- Init.Sym.Lemmas
Lean.Sym.Rat.le_eq_true : ∀ (a b : ℚ), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
selfAdjoint.norm_sq_expUnitary_sub_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] {x : ↥(selfAdjoint A)},
  ‖x‖ ≤ Real.pi → ‖↑(selfAdjoint.expUnitary x) - 1‖ ^ 2 = 2 * (1 - Real.cos ‖x‖)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.comp_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y Z : C}
  (f : X ⟶ Y) (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (g - h) =
    CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f h
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
CliffordAlgebra.isUnit_ι_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) [Invertible 2] {m : M}, IsUnit ((CliffordAlgebra.ι Q) m) ↔ IsUnit (Q m)
-- Mathlib.Order.Closure
ClosureOperator.ext_iff : ∀ {α : Type u_1} [inst : Preorder α] {c₁ c₂ : ClosureOperator α}, c₁ = c₂ ↔ ∀ (x : α), c₁ x = c₂ x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β k},
  (t.insert k v).toList.Perm (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) t.toList)
-- Mathlib.Order.BooleanAlgebra.Basic
codisjoint_himp_self_right : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Codisjoint x (x ⇨ y)
-- Mathlib.CategoryTheory.Category.Basic
/-- The typeclass `Category C` describes morphisms associated to objects of type `C`.
The universe levels of the objects and morphisms are unconstrained, and will often need to be
specified explicitly, as `Category.{v} C`. (See also `LargeCategory` and `SmallCategory`.)  -/
CategoryTheory.Category : Type u → Type (max u (v + 1))
-- Mathlib.Analysis.Complex.SqrtDeriv
/-- `Complex.sqrt` is continuous at `z` provided `0 ≤ z.re` or `z.im ≠ 0`. This is weaker than
requiring `z ∈ slitPlane`, as it additionally includes the imaginary axis and `0`.  -/
Complex.continuousAt_sqrt : ∀ {z : ℂ}, 0 ≤ z.re ∨ z.im ≠ 0 → ContinuousAt Complex.sqrt z
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n]
  [inst_6 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterMapWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let __x ← (f b).run
        match __x with
          | some c => pure (g d c)
          | x => pure d)
      init it
-- Batteries.Data.List.Lemmas
List.findIdxNth_countPBefore_of_lt_length_of_pos : ∀ {α : Type u_1} {i : ℕ} {p : α → Bool} {xs : List α} {h : i < xs.length},
  p xs[i] = true → List.findIdxNth p xs (List.countPBefore p xs i) = i
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.bound' : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} (self : f.NonlinearRightInverse) (y : F),
  ‖self.toFun y‖ ≤ ↑self.nnnorm * ‖y‖
-- Init.Data.UInt.Bitwise
UInt32.and_assoc : ∀ (a b c : UInt32), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_one : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → One (γ a b)],
  Sigma.uncurry 1 = 1
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
/-- A stepping stone to `CStarAlgebra.exists_sum_four_unitary` that specifies the unitary
elements precisely. The `let`s in the statement are intentional.  -/
CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (x : A) (hx : x ≠ 0),
  have u₁ := selfAdjoint.unitarySelfAddISMul (realPart (‖x‖⁻¹ • x)) ⋯;
  have u₂ := selfAdjoint.unitarySelfAddISMul (imaginaryPart (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + Complex.I • (↑u₂ + ↑(star u₂)))