mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_of_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E}
  {s : Set E} [ContinuousAdd E], s ∈ nhds x → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.FieldTheory.Galois.Basic
Algebra.IsQuadraticExtension.congr_simp : ∀ (R : Type u_2) (S : Type u_3) [inst : CommSemiring R] [inst_1 : StrongRankCondition R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S], Algebra.IsQuadraticExtension R S = Algebra.IsQuadraticExtension R S
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse_eq_inverse' : ∀ {M : Type u_2} {X : Type u_5} [inst : SMul M X] {Y₁ : Type u_8} [inst_1 : SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- If every set `A` is open if for every compact `K` the intersection `K ∩ A` is open in `K`,
then the space is a compactly coherent space.  -/
CompactlyCoherentSpace.of_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (A : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' A)) → IsOpen A) → CompactlyCoherentSpace X
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_eq_bot_iff_center_eq_top : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = ⊥ ↔ AddSubgroup.center G = ⊤
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_iSup₂ : ∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Subgroup Mˣ),
  (⨆ i, ⨆ j, f i j).ofUnits = ⨆ i, ⨆ j, (f i j).ofUnits
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffOn_extend_symm : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M → ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑(e.extend I).symm) (↑I '' e.target)
-- Mathlib.RingTheory.Noetherian.Nilpotent
Ideal.FG.isNilpotent_iff_le_nilradical : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.FG → (IsNilpotent I ↔ I ≤ nilradical R)
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.of_comp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, (g.comp f).FormallyUnramified → g.FormallyUnramified
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.sum_support_decompose : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ]
  [inst_5 : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)] (r : M),
  ∑ i ∈ DFinsupp.support ((DirectSum.decompose ℳ) r), ↑(((DirectSum.decompose ℳ) r) i) = r
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.indepSets : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndepSets s κ μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.Kernel.IndepSets (s i) (s j) κ μ
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_mono : ∀ {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {g : β → α},
  m₁ ≤ m₂ → MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂
-- Qq.Macro
/-- `ql(u)` quotes the universe level `u`.  -/
Qq.«termQl(_)» : Lean.ParserDescr
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Unpacks the mantissa portion of the packed float. If this is a normal number, this
will be missing the implicit bit.
 -/
Float.Model.UnpackedFloat.unpackMantissa : {spec : Float.Model.Format} → BitVec spec.numBits → BitVec spec.mantissaBitsWithoutImplicit
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.add_left : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] {s t : Finset α},
  t.Nontrivial → s.Nonempty → (s + t).Nontrivial
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The natural multifork associated to `S : J.Cover X` for a presheaf `P`.
Saying that this multifork is a limit is essentially equivalent to the sheaf condition at the
given object for the given covering sieve. See `Sheaf.lean` for an equivalent sheaf condition
using this.
 -/
CategoryTheory.GrothendieckTopology.Cover.multifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {D : Type u₁} →
          [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
            (S : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.Multifork (S.index P)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Isomorphic monoids have isomorphic monoid algebras.  -/
MonoidAlgebra.mapDomainRingEquiv : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → [inst_1 : Monoid M] → [inst_2 : Monoid N] → M ≃* N → MonoidAlgebra R M ≃+* MonoidAlgebra R N
-- Init.Data.Nat.Lemmas
Nat.mul_mul_mul_comm : ∀ (a b c d : ℕ), a * b * (c * d) = a * c * (b * d)
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Returns `true` if, at the current depth, we should omit the term and use `⋯` rather than
delaborating it. This function can only return `true` if `pp.deepTerms` is set to `false`.
It also contains a heuristic to allow "shallow terms" to be delaborated, even if they appear deep in
an expression, which prevents terms such as atomic expressions or `OfNat.ofNat` literals from being
delaborated as `⋯`.
 -/
Lean.PrettyPrinter.Delaborator.shouldOmitExpr : Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Bool
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- When `C` is braided, there is an isomorphism `Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`, natural
in both `F₁` and `F₂`.
Note that `(externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁`
type checks.  -/
CategoryTheory.MonoidalCategory.externalProductSwap : (J₁ : Type u₁) →
  (J₂ : Type u₂) →
    (C : Type u₃) →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [CategoryTheory.BraidedCategory C] →
                (CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₂ C).comp
                    ((CategoryTheory.Functor.whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj
                      (CategoryTheory.Prod.swap J₂ J₁)) ≅
                  (CategoryTheory.Prod.swap (CategoryTheory.Functor J₁ C) (CategoryTheory.Functor J₂ C)).comp
                    (CategoryTheory.MonoidalCategory.externalProductBifunctor J₂ J₁ C)
-- Init.Data.UInt.Lemmas
UInt16.ofNat_toNat : ∀ {x : UInt16}, UInt16.ofNat x.toNat = x
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.sqrt`.  -/
Mathlib.Meta.Positivity.evalNatSqrt : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Expr
_private.Lean.Expr.0.Lean.natLEPred : Lean.Expr
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  0 ∈ s → ∀ (r : R), (MvPowerSeries.truncFinset R s) (MvPowerSeries.C r) = MvPolynomial.C r
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasureTheory.AnalyticSet_def : ∀ {α : Type u_3} [inst : TopologicalSpace α] (s : Set α),
  MeasureTheory.AnalyticSet s = (s = ∅ ∨ ∃ f, Continuous f ∧ Set.range f = s)
-- Lean.Language.Basic
/-- Waits on and returns all snapshots in the tree.  -/
Lean.Language.SnapshotTree.getAll : Lean.Language.SnapshotTree → Array Lean.Language.Snapshot
-- Init.Data.SInt.Lemmas
Int32.neg_neg : ∀ {a : Int32}, - -a = a
-- Init.Control.Lawful.Basic
/-- The `mapConst` implementation is equivalent to the default implementation.
 -/
LawfulFunctor.map_const : ∀ {f : Type u → Type v} {inst : Functor f} [self : LawfulFunctor f] {α β : Type u},
  Functor.mapConst = Functor.map ∘ Function.const β
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.foundBVar : ℕ → Lean.Meta.Grind.NormalizePattern.M✝ Bool
-- Mathlib.SetTheory.ZFC.Basic
/-- All functions are classically definable.  -/
Classical.allZFSetDefinable : {n : ℕ} → (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) → ZFSet.Definable n F
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_7 : {α : Type u} → Std.Rio.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mclosure_preimage_le : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (s : Set N),
  AddSubmonoid.closure (⇑f ⁻¹' s) ≤ AddSubmonoid.comap f (AddSubmonoid.closure s)
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofIntLE : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt),
  (Int64.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM'.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : (x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys))
  (h_2 : (x : List α) → (x_2 : List β) → motive x x_2),
  (∀ (x_2 : α) (xs : List α) (y : β) (ys : List β), x = x_2 :: xs → x_1 = y :: ys → False) →
    (match x, x_1 with
      | x :: xs, y :: ys => h_1 x xs y ys
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.outCLM_isUniformInducing : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : UniformSpace E] [inst_4 : IsUniformAddGroup E] [inst_5 : ContinuousConstSMul K E],
  IsUniformInducing ⇑(SeparationQuotient.outCLM K E)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_setOfPred_mem_eq_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R {x | ↑x ∈ s} = ⊤
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_left' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp (p + a) b = p + toIcoMod hp a b
-- Init.Data.Int.Order
Int.natAbs_negSucc : ∀ (n : ℕ), (Int.negSucc n).natAbs = n.succ
-- Mathlib.Algebra.Group.Prod
AddHom.prod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N)
  (g : M →ₙ+ P) (x : M), (f.prod g) x = (f x, g x)
-- Mathlib.Data.PFun
/-- Composition of partial functions as a partial function.  -/
PFun.comp : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (β →. γ) → (α →. β) → α →. γ
-- Mathlib.Combinatorics.HalesJewett
/-- A function `f : α → α'` determines a function `line α ι → line α' ι`. For a coordinate `i`
`l.map f` is the identity at `i` if `l` is, and constantly `f y` if `l` is constantly `y` at `i`.  -/
Combinatorics.Line.map : {α : Type u_5} → {α' : Type u_6} → {ι : Type u_7} → (α → α') → Combinatorics.Line α ι → Combinatorics.Line α' ι
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.eval_pappAck : ∀ (m n : ℕ), (Nat.Partrec.Code.pappAck m).eval n = Part.some (ack m n)
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] {s : Set G},
  IsClosed s → IsClosed (-s)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂_apply : ∀ {A : Type u_1} {R : Type u_2} [inst : Semiring A] [inst_1 : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8}
  {Pₗ : Type u_9} {Qₗ : Type u_10} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid Nₗ] [inst_4 : AddCommMonoid Pₗ]
  [inst_5 : AddCommMonoid Qₗ] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ]
  [inst_9 : Module A Pₗ] [inst_10 : SMulCommClass R A Pₗ] [inst_11 : Module R A] [inst_12 : Module A M]
  [inst_13 : Module A Qₗ] [inst_14 : SMulCommClass R A Qₗ] [inst_15 : IsScalarTower R A Qₗ]
  [inst_16 : IsScalarTower R A Pₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ) (m : M) (n : Nₗ),
  ((f.compr₂ g) m) n = g ((f m) n)
-- Mathlib.Order.LiminfLimsup
Filter.sdiff_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α),
  a \ Filter.liminf u f = Filter.limsup (fun b => a \ u b) f
-- Init.Data.UInt.Lemmas
UInt8.le_iff_toFin_le : ∀ {a b : UInt8}, a ≤ b ↔ a.toFin ≤ b.toFin
-- Init.Data.Int.Lemmas
Int.zero_add : ∀ (a : ℤ), 0 + a = a
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.coe_edgeFinset : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype ↑G.edgeSet], ↑G.edgeFinset = G.edgeSet
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp_symm : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M}
  (H : AddSubmonoid.map k.toAddMonoidHom T = S) (x : M), (f.ofAddEquivOfDom H) (k.symm x) = f x
-- Lean.Parser.Types
Lean.Parser.ParserState.restore : Lean.Parser.ParserState → ℕ → String.Pos.Raw → Lean.Parser.ParserState
-- Mathlib.MeasureTheory.Measure.MutuallySingular
/-- Two measures `μ`, `ν` are said to be mutually singular if there exists a measurable set `s`
such that `μ s = 0` and `ν sᶜ = 0`.  -/
MeasureTheory.Measure.MutuallySingular : {α : Type u_1} → {x : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Prop
-- Lean.Meta.CoeAttr
Lean.Meta.instInhabitedCoeFnInfo : Inhabited Lean.Meta.CoeFnInfo
-- Batteries.Recycling.RBTree.WF
/-- The `balance1` function does nothing if the first argument is already balanced.  -/
RBTree.RBNode.balance1_eq : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  l.Balanced c n → l.balance1 v r = RBTree.RBNode.node RBTree.RBColor.black l v r
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2-coboundaries `B²(G, A)` of `A : Rep k G`, defined as the image of the map
`Fun(G, A) → Fun(G × G, A)` sending `(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).`  -/
groupCohomology.coboundaries₂ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u_1, u, u} k G) → Submodule k (G × G → ↑A)
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map₂_map_left_comm`.  -/
Filter.map_map₂_distrib_left : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : Filter α}
  {g : Filter β} {n : γ → δ} {m' : α' → β → δ} {n' : α → α'},
  (∀ (a : α) (b : β), n (m a b) = m' (n' a) b) → Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n' f) g
-- Mathlib.Topology.LocallyConstant.Basic
TopologicalSpace.Clopens.mk.congr_simp : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (isClopen' : IsClopen carrier),
  { carrier := carrier, isClopen' := isClopen' } = { carrier := carrier_1, isClopen' := ⋯ }
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is left distributive over addition  -/
NonUnitalNonAssocRing.left_distrib : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a b c : α), a * (b + c) = a * b + a * c
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.pairwise_toList_le : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [LT α] [inst_3 : Std.PRange.Least? α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_8 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inr_coprodIsoPushout_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodIsoPushout X Y).hom =
    CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ColorFocused.mk.inj : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ}
  {lines : Multiset (Combinatorics.Line.AlmostMono C)} {focus : ι → Option α}
  {is_focused : ∀ p ∈ lines, ↑p.line none = focus}
  {distinct_colors : (Multiset.map Combinatorics.Line.AlmostMono.color lines).Nodup}
  {lines_1 : Multiset (Combinatorics.Line.AlmostMono C)} {focus_1 : ι → Option α}
  {is_focused_1 : ∀ p ∈ lines_1, ↑p.line none = focus_1}
  {distinct_colors_1 : (Multiset.map Combinatorics.Line.AlmostMono.color lines_1).Nodup},
  { lines := lines, focus := focus, is_focused := is_focused, distinct_colors := distinct_colors } =
      { lines := lines_1, focus := focus_1, is_focused := is_focused_1, distinct_colors := distinct_colors_1 } →
    lines = lines_1 ∧ focus = focus_1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_iff_lt_or_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE a b ↔ Std.PRange.UpwardEnumerable.LT a b ∨ a = b
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.Indep.sdiff`. -/
Matroid.Indep.diff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∀ (X : Set α), M.Indep (I \ X)
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj X ≅ 𝟭 D` and `X : GradedObject J D`,
this is the isomorphism `((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a ≅ Y a.2`
when `a : J × I` is such that `a.2 = 0`.  -/
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) →
                    (Y : C) →
                      (F.flip.obj Y ≅ CategoryTheory.Functor.id D) →
                        (X : CategoryTheory.GradedObject J D) →
                          (a : J × I) →
                            a.2 = 0 →
                              (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
                                  ((CategoryTheory.GradedObject.single₀ I).obj Y) a ≅
                                X a.1)
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.right : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop}, Nat.RecursiveIn.below ⋯
-- Mathlib.Algebra.Group.Commute.Units
IsUnit.of_pow_eq_one : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {a : M}, a ^ n = 1 → n ≠ 0 → IsUnit a
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A fiber in a bundle satisfying the `[RiemannianBundle E]` typeclass inherits
an `InnerProductSpace ℝ` structure.

The normal priority for an instance which always applies like this one should be 100.
We use 80 as this is rather specialized, so we want other paths to be tried first typically.
As this instance is quite specific and very costly because of higher-order unification, we
also scope it to the `Bundle` namespace.  -/
Bundle.instInnerProductSpaceReal : {B : Type u_7} →
  {E : B → Type u_8} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] →
          [h : Bundle.RiemannianBundle E] →
            [inst_3 : ∀ (b : B), IsTopologicalAddGroup (E b)] →
              [inst_4 : ∀ (b : B), ContinuousConstSMul ℝ (E b)] → (b : B) → InnerProductSpace ℝ (E b)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.ext : ∀ {α : Type u} {a b : Additive α}, Additive.toMul a = Additive.toMul b → a = b
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.mk.injEq : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_10}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_11} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] (toMulActionHom : A →ₑ[⇑φ] B) (map_zero' : toMulActionHom.toFun 0 = 0)
  (map_add' : ∀ (x y : A), toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y)
  (toMulActionHom_1 : A →ₑ[⇑φ] B) (map_zero'_1 : toMulActionHom_1.toFun 0 = 0)
  (map_add'_1 : ∀ (x y : A), toMulActionHom_1.toFun (x + y) = toMulActionHom_1.toFun x + toMulActionHom_1.toFun y),
  ({ toMulActionHom := toMulActionHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMulActionHom := toMulActionHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }) =
    (toMulActionHom = toMulActionHom_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getValueCast? a l = none
-- Mathlib.CategoryTheory.Sites.Canonical
/-- A variant of `yonedaFullyFaithful` with a raise in the universe level.  -/
CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] → (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).FullyFaithful
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
          (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.AddMonObj.zero
-- Std.Sync.Notify
Std.Notify.Consumer.normal.inj : ∀ {α : Type} {promise promise_1 : IO.Promise α},
  Std.Notify.Consumer.normal promise = Std.Notify.Consumer.normal promise_1 → promise = promise_1
-- Mathlib.Geometry.Diffeology.Basic
/-- A map `p : EuclideanSpace ℝ (Fin n) → X` is called a plot iff it is part of the diffeology on
`X`. This is equivalent to `p` being smooth with respect to the standard diffeology on
`EuclideanSpace ℝ (Fin n)`.  -/
Diffeology.IsPlot : {X : Type u_1} → [DiffeologicalSpace X] → {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1)
  (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨i.succ, hi⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_2 i hi
-- Init.Control.Lawful.Instances
EStateM.run_modify : ∀ {σ ε : Type u_1} (f : σ → σ) (s : σ), (modify f).run s = EStateM.Result.ok PUnit.unit (f s)