mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.TestFunction
/-- A test function on `Ω` is `μ`-integrable for any measure `μ` on `E` satisfying
`LocallyIntegrableOn 1 Ω μ`. Note that this is a weaker assumption than both
- `IsLocallyFiniteMeasure (μ.restrict Ω)` (because we say nothing about points outside of `Ω`)
- `IsFiniteMeasureOnCompacts (μ.restrict Ω)` (because we say nothing about compacts not
  contained in `Ω`)

For example, if `μ` is the measure with density `fun (x : ℝ) ↦ x⁻¹` with respect to the Lebesgue
measure and `Ω` is the open set `Ioo 0 1`, we have `LocallyIntegrableOn 1 Ω μ` (hence `μ` defines
a distribution on `Ω`) but the other two conditions are not satisfied.
 -/
TestFunction.integrable : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E},
  MeasureTheory.LocallyIntegrableOn (fun x => 1) (↑Ω) μ → ∀ (f : TestFunction Ω F n), MeasureTheory.Integrable (⇑f) μ
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
_private.Lean.Meta.Tactic.Grind.EMatchTheoremPtr.0.Lean.Meta.Grind.isSameEMatchTheoremPtr.unsafe_impl_2 : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatchTheorem → Bool
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.of_subsingleton : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Subsingleton R], LinearIndepOn R v s
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaForget_inv_app_app_hom_apply : ∀ (X : AddCommGrpCatᵒᵖ) (X_1 : AddCommGrpCat) (f : Opposite.unop X ⟶ X_1),
  (CategoryTheory.ConcreteCategory.hom ((AddCommGrpCat.coyonedaForget.inv.app X).app X_1)) f = AddCommGrpCat.Hom.hom f
-- Mathlib.Data.Set.Insert
/-- **Alias** of the reverse direction of `Set.inter_singleton_eq_empty`. -/
Set.inter_singleton_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s ∩ {a} = ∅
-- Mathlib.Data.Set.SMulAntidiagonal
Set.mem_smulAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t : Set P} {a : P} {x : G × P},
  x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
-- Mathlib.Tactic.Attr.Register
/-- Simp attribute for lemmas about `Even`  -/
Parser.Attr.parity_simps : Lean.ParserDescr
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.cokernel.π_desc_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = 0) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.desc f k h))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x) =
    (CategoryTheory.ConcreteCategory.hom k) x
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.toCommMonoidWithZero : {M₀ : Type u_2} → CancelCommMonoidWithZero M₀ → CommMonoidWithZero M₀
-- Mathlib.Data.Set.Finite.Lattice
/-- A finite set is bounded below.  -/
Set.Finite.bddBelow : ∀ {α : Type u} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {s : Set α}, s.Finite → BddBelow s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.categoryStruct_id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = (CategoryTheory.Oplax.OplaxTrans.id F).app a
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.hom_ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {X : C}
  {f f' : X ⟶ CategoryTheory.Limits.limit F},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π F j) =
        CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π F j)) →
    f = f'
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] (s : Finset β), s -ᵥ ∅ = ∅
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → g x ≠ 0 → ContDiffWithinAt 𝕜 n (f / g) s x
-- Mathlib.Logic.Relation
Relation.reflGen_minimal : ∀ {α : Type u_1} {r r' : α → α → Prop} [Std.Refl r'], r ≤ r' → Relation.ReflGen r ≤ r'
-- Lean.Environment
Lean.ImportState : Type
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.eq_2 : ∀ (acc : String) (s : String.Slice), String.Slice.intercalate.go✝ acc s [] = acc
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted_monomial : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) (n : σ →₀ ℕ) (a : R),
  MvPowerSeries.IsRestricted c ((MvPowerSeries.monomial n) a)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.exists_ae_eq_range_subset : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α},
  AEMeasurable f μ →
    ∀ {t : Set β}, (∀ᵐ (x : α) ∂μ, f x ∈ t) → t.Nonempty → ∃ g, Measurable g ∧ Set.range g ⊆ t ∧ f =ᵐ[μ] g
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (B : LinearMap.BilinForm K V) (W : Subspace K V),
  B.IsRefl → Submodule.map (Submodule.subtype W) (LinearMap.domRestrict B W).ker = W ⊓ B.orthogonal ⊤
-- Mathlib.Algebra.Group.ULift
ULift.neg.eq_1 : ∀ {α : Type u} [inst : Neg α], ULift.neg = { neg := fun f => { down := -f.down } }
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.match_1.eq_2 : ∀ {α : Type} (motive : List α → Sort u_1) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.FieldTheory.Finite.Basic
/-- A variation on Fermat's little theorem. See `ZMod.pow_card_sub_one_eq_one`  -/
ZMod.pow_card : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (x : ZMod p), x ^ p = x
-- Mathlib.Algebra.Group.Basic
inv_mul_eq_of_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b = a * c → a⁻¹ * b = c
-- Mathlib.Order.Interval.Set.Image
StrictAnti.image_Iio_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictAnti f → f '' Set.Iio b ⊆ Set.Ioi (f b)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabNumLit : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan), CategoryTheory.Bicategory.HasLeftKanExtension f g
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_sub_cosh : ∀ (x : ℂ), Complex.sinh x - Complex.cosh x = -Complex.exp (-x)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerMVarErrorCustomInfo : Lean.MVarId → Lean.Syntax → Lean.MessageData → Lean.Elab.TermElabM Unit
-- Init.BinderPredicates
Lean.binderPred.quot : Lean.ParserDescr
-- Mathlib.Topology.Order.Compact
/-- A complete linear order is a compact space.

We do not register an instance for a `[CompactIccSpace α]` because this would only add instances
for products (indexed or not) of complete linear orders, and we have instances with higher priority
that cover these cases.  -/
compactSpace_of_completeLinearOrder : ∀ {α : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α], CompactSpace α
-- Mathlib.Algebra.Order.Floor.Ring
/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is.  -/
Mathlib.Meta.Positivity.evalIntFloor : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N),
  AddMonoidHom.mker (f.domRestrict S) = AddSubmonoid.comap S.subtype (AddMonoidHom.mker f)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instPartialOrder : {M : Type u_1} → [inst : MulOneClass M] → PartialOrder (Submonoid M)
-- Mathlib.RepresentationTheory.Basic
Representation.apply_bijective : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G), Function.Bijective ⇑(ρ g)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.X_eq_normalizeX : ∀ {k : Type u_2} [inst : Field k], PowerSeries.X = normalize PowerSeries.X
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.coconePointwiseProduct_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  {F : (i : α) → CategoryTheory.Functor (I i) C} (c : (i : α) → CategoryTheory.Limits.Cocone (F i)),
  (CategoryTheory.Limits.coconePointwiseProduct c).ι =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.pi fun i => (c i).ι)
        (CategoryTheory.Limits.Pi.functor α))
      (CategoryTheory.Limits.Pi.constCompPiIsoConst fun i => (c i).pt).hom
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.foldr.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Ordnode α → β → Sort u_2) (z : β) (h_1 : (z : β) → motive Ordnode.nil z)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → (z : β) → motive (Ordnode.node size l x r) z),
  (match Ordnode.nil, z with
    | Ordnode.nil, z => h_1 z
    | Ordnode.node size l x r, z => h_2 size l x r z) =
    h_1 z
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring `R` has finite quotients if the quotient `R ⧸ I` is finite for all nonzero ideals of `R`.
 -/
Ring.HasFiniteQuotients : (R : Type u_1) → [CommRing R] → Prop
-- Batteries.Recycling.MonadSatisfying.Basic
/-- The `SatisfiesM p x` predicate is monotonic in `p`.  -/
SatisfiesM.imp : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p q : α → Prop} [inst : Functor m] [LawfulFunctor m] {x : m α},
  SatisfiesM p x → (∀ {a : α}, p a → q a) → SatisfiesM q x
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.K')
  (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.push k s q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_2 k s q
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1}
  {Y : I → C} (x x_1 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y),
  x = x_1 →
    ∀ (X : C) ⦃Y_1 : C⦄ (f f_1 : Y_1 ⟶ X) (e_f : f = f_1) (a : (CategoryTheory.Sieve.ofObjects Y X).arrows f),
      x.familyOfElements X f a = x_1.familyOfElements X f_1 ⋯
-- Mathlib.Order.Ideal
/-- **Alias** of the reverse direction of `Order.Ideal.biSup_finset_mem_iff`. -/
Order.Ideal.biSup_finset_mem : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Type u_2} {f : α → P} {s : Finset α},
  (∀ i ∈ s, f i ∈ I) → ⨆ i ∈ s, f i ∈ I
-- Mathlib.Data.DFinsupp.Interval
/-- Given a finitely supported function `f : Π₀ i, Finset (α i)`, one can define the finset
`f.pi` of all finitely supported functions whose value at `i` is in `f i` for all `i`.  -/
DFinsupp.pi : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (α i)] → (Π₀ (i : ι), Finset (α i)) → Finset (Π₀ (i : ι), α i)
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.l_top : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] (gi : GaloisInsertion l u), l ⊤ = ⊤
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_emod : ∀ (a b : ℤ), a % b % b = a % b
-- Mathlib.Data.Finset.Image
Finset.mem_range_iff_mem_finset_range_of_mod_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ},
  0 < n → (∀ (i : ℤ), f (i % ↑n) = f i) → (a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f ↑i) (Finset.range n))
-- Init.Meta.Defs
Lean.Syntax.instRepr : Repr Lean.Syntax
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The induced map on the first homology of the (naive) cotangent complex.
 -/
Algebra.Extension.H1Cotangent.map : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u'} →
              {S' : Type v'} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [IsScalarTower R R' S'] → P.Hom P' → P.H1Cotangent →ₗ[S] P'.H1Cotangent
-- Mathlib.Data.PNat.Xgcd
/-- We can now define the full reduction function, which applies
step as long as possible, and then applies finish. Note that the
"have" statement puts a fact in the local context, and the
equation compiler uses this fact to help construct the full
definition in terms of well-founded recursion.  The same fact
needs to be introduced in all the inductive proofs of properties
given below.  -/
PNat.XgcdType.reduce : PNat.XgcdType → PNat.XgcdType
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.over_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Over X),
  U.right = { as := PUnit.unit }
-- Init.Data.Fin.Lemmas
Fin.reverseInduction.go.congr_simp : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast cast_1 : (i : Fin n) → motive i.succ → motive i.castSucc),
  cast = cast_1 →
    ∀ (i : Fin (n + 1)) (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x x_1 : motive ⟨j, h⟩),
      x = x_1 → Fin.reverseInduction.go cast i j h h2 x = Fin.reverseInduction.go cast_1 i j h h2 x_1
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.comp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [inst_9 : CommSemiring T]
  [inst_10 : Algebra R T] [inst_11 : Algebra S T] [IsScalarTower R S T] [inst_13 : AddCommMonoid O]
  [inst_14 : Module R O] [inst_15 : Module S O] [inst_16 : Module T O] [inst_17 : IsScalarTower S T O]
  [inst_18 : IsScalarTower R S O] [inst_19 : IsScalarTower R T O] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ {g : N →ₗ[S] O}, IsBaseChange T g → IsBaseChange T (↑R g ∘ₗ f)
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.inf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S T : Submodule R M},
  S.IsPrimary → T.IsPrimary → (S.colon Set.univ).radical = (T.colon Set.univ).radical → (S ⊓ T).IsPrimary
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h_mem_cartanSubalgebra : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Fintype ι] [inst_7 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.h i ∈ RootPairing.GeckConstruction.cartanSubalgebra b
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.subset_smul : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {a : 𝕜}, Balanced 𝕜 s → 1 ≤ ‖a‖ → s ⊆ a • s
-- Init.Data.UInt.Lemmas
UInt64.ofFin_uint8ToFin : ∀ (n : UInt8), UInt64.ofFin (Fin.castLE UInt8.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64
-- Mathlib.Algebra.Order.Field.Canonical
tsub_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [IsStrictOrderedRing α]
  [inst_4 : Sub α] [OrderedSub α] (a b c : α), (a - b) / c = a / c - b / c
-- Std.Data.HashMap.Basic
Std.HashMap.instDecidableMem : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.HashMap α β} → {a : α} → Decidable (a ∈ m)
-- Init.SimpLemmas
Lean.false_arrow_congr : ∀ (p q : Prop), p = False → Lean.Arrow p q = True
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.find_mem : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)} (i : ι) (ne : c.Nonempty),
  ShrinkingLemma.PartialRefinement.find c ne i ∈ c
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.IsPrefix_zip : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (input : aig.BinaryRefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func],
  Std.Sat.AIG.IsPrefix aig.decls (Std.Sat.AIG.RefVec.zip aig input func).aig.decls
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c))
  (s : CategoryTheory.Limits.Cocone F.leftOp),
  (CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
-- Init.WFComputable
/-- A computable version of `Acc.ndrecOn`.  -/
Acc.ndrecOnC : {α : Sort u_1} →
  {r : α → α → Prop} →
    {C : α → Sort v} →
      {a : α} → Acc r a → ((x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) → C a
-- Mathlib.Order.RelIso.Basic
acc_liftOn₂'_iff : ∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂}
  {a : α}, Acc (fun x y => x.liftOn₂' y r H) (Quotient.mk'' a) ↔ Acc r a
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgEquiv_coe_ringHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B), ↑(Polynomial.mapAlgEquiv f) = Polynomial.mapRingHom ↑f
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutex.ref : {α : Type} → Std.SharedMutex α → IO.Ref α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.mk : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → PNat.XgcdType
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h' : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.DistinctKeys l →
    ∀ (h : l.Perm l'), Std.Internal.List.getValueCast a l h' = Std.Internal.List.getValueCast a l' ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.hom_comp_ι_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (f_1 : s ⟶ t) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp f_1.hom (CategoryTheory.CategoryStruct.comp t.ι h) =
    CategoryTheory.CategoryStruct.comp s.ι h
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_sub_self_of_tmod_eq : ∀ {a b c : ℤ}, a.tmod b = c → b ∣ c - a
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.curryAlgEquiv_symm_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (m : M) (n : N) (a : A),
  (MonoidAlgebra.curryAlgEquiv R).symm (MonoidAlgebra.single m (MonoidAlgebra.single n a)) =
    MonoidAlgebra.single (m, n) a
-- Init.Data.Option.Monadic
Option.idRun_forIn'_yield_eq_pelim : ∀ {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β),
  (forIn' o b fun a m b => ForInStep.yield <$> f a m b).run = o.pelim b fun a h => (f a h b).run
-- Mathlib.Order.Minimal
image_monotone_setOfPred_minimal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) →
    f '' {x | Minimal P x} = {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Mathlib.Topology.Separation.Regular
/-- Two disjoint sets in a normal space admit disjoint neighbourhoods.  -/
NormalSpace.normal : ∀ {X : Type u} {inst : TopologicalSpace X} [self : NormalSpace X] (s t : Set X),
  IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaFunctor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] (X : C)
  {X_1 Y : Type w} (f : X_1 ⟶ Y),
  (CategoryTheory.Limits.sigmaFunctor.obj X).map f =
    CategoryTheory.Limits.Sigma.map' ⇑(CategoryTheory.ConcreteCategory.hom f) fun x =>
      CategoryTheory.CategoryStruct.id X