mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.IsLimit.lift.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F}
  (hc hc_1 : CategoryTheory.Limits.IsLimit c),
  hc = hc_1 →
    ∀ {X : C} (f f_1 : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (e_f : f = f_1)
      (hf :
        ∀ ⦃i j : J⦄ (g : i ⟶ j),
          CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
            CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)),
      CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf = CategoryTheory.Limits.Wedge.IsLimit.lift hc_1 f_1 ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `x ⇨ y` is equal to `y ⊔ xᶜ`  -/
CompleteBooleanAlgebra.himp_eq : ∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (x y : α), x ⇨ y = y ⊔ xᶜ
-- Mathlib.Algebra.Category.Ring.Epi
RingHom.surjective_iff_epi_and_finite : ∀ {R S : CommRingCat} {f : R ⟶ S},
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) ↔ CategoryTheory.Epi f ∧ (CommRingCat.Hom.hom f).Finite
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.nat_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ), padicNorm p ↑m < 1 ↔ p ∣ m
-- Mathlib.Order.Filter.Pointwise
Filter.addCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddCommMonoid α],
  Filter.addCommMonoid =
    { toAdd := Filter.addZeroClass.toAdd, add_assoc := ⋯, toZero := Filter.addZeroClass.toZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := Filter.addMonoid.toNSMul, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.cosh : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.cosh (f x)) μ
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- The formal counterpart of `dslope`, corresponding to the expansion of `(f z - f 0) / z`. If `f`
has `p` as a power series, then `dslope f` has `fslope p` as a power series.  -/
FormalMultilinearSeries.fslope : {𝕜 : Type u} →
  {E : Type v} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → FormalMultilinearSeries 𝕜 𝕜 E → FormalMultilinearSeries 𝕜 𝕜 E
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_univ_iff : ∀ {X : Type u} [inst : TopologicalSpace X], IsLindelof Set.univ ↔ LindelofSpace X
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.equivalenceOfIsTerminal_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).functor = CategoryTheory.Over.forget X
-- Mathlib.Analysis.ODE.PicardLindelof
/-- `IsPicardLindelof` is preserved when shrinking the time interval.  -/
IsPicardLindelof.shrink_time : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax tmin' tmax' : ℝ} {t₀ : ↑(Set.Icc tmin tmax)}
  {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∀ (t₀' : ↑(Set.Icc tmin' tmax')), ↑t₀ = ↑t₀' → tmin ≤ tmin' → tmax' ≤ tmax → IsPicardLindelof f t₀' x₀ a r L K
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_attach : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (f : ι → M), ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x
-- Init.Data.BitVec.Lemmas
BitVec.not_eq_comm : ∀ {w : ℕ} {x y : BitVec w}, ~~~x = y ↔ x = ~~~y
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instIsScalarTowerSubtypePreLpMemAddSubgroup : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} {p : ENNReal}
  [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜']
  [inst_3 : (i : α) → Module 𝕜 (E i)] [inst_4 : (i : α) → Module 𝕜' (E i)] [inst_5 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_6 : ∀ (i : α), IsBoundedSMul 𝕜' (E i)] [inst_7 : SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)],
  IsScalarTower 𝕜' 𝕜 ↥(lp E p)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- This property `HasLeftKanExtension L F` holds when the functor `F` has a left
Kan extension along `L`.  -/
CategoryTheory.Functor.HasLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → Prop
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- The natural projection from `GL n R` to `PGL n R`.  -/
Matrix.ProjGenLinGroup.mk : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] → [inst_1 : DecidableEq n] → [inst_2 : CommRing R] → GL n R →* Matrix.ProjGenLinGroup n R
-- Init.Data.String.Lemmas.FindPos
String.Pos.toSlice_prev : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, (p.prev h).toSlice = p.toSlice.prev ⋯
-- Mathlib.Algebra.Group.Translate
translate_sum_right : ∀ {ι : Type u_1} {M : Type u_4} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommMonoid M] (a : G)
  (f : ι → G → M) (s : Finset ι), translate a (∑ i ∈ s, f i) = ∑ i ∈ s, translate a (f i)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_def : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [inst_3 : DecidablePred p] (f : Π₀ (i : ι), β i),
  DFinsupp.filter p f = DFinsupp.mk (Finset.filter p f.support) fun i => f ↑i
-- Mathlib.MeasureTheory.VectorMeasure.Prod
/-- The product of two vector measures `μ` and `ν` with respect to a continuous bilinear map `B`,
giving mass `B (μ s) (ν t)` to any measurable product set `s × t`.
If such a measure does not exist, we use the junk value `0`.  -/
MeasureTheory.VectorMeasure.prod : {X : Type u_2} →
  {Y : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          {mX : MeasurableSpace X} →
            {mY : MeasurableSpace Y} →
              [inst : NormedAddCommGroup E] →
                [inst_1 : NormedSpace ℝ E] →
                  [inst_2 : NormedAddCommGroup F] →
                    [inst_3 : NormedSpace ℝ F] →
                      [inst_4 : NormedAddCommGroup G] →
                        [inst_5 : NormedSpace ℝ G] →
                          MeasureTheory.VectorMeasure X E →
                            MeasureTheory.VectorMeasure Y F →
                              (E →L[ℝ] F →L[ℝ] G) → MeasureTheory.VectorMeasure (X × Y) G
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.MakeEditLinkProps.mk.injEq : ∀ (edit : Lean.Lsp.TextDocumentEdit) (newSelection? : Option Lean.Lsp.Range) (title? : Option String)
  (edit_1 : Lean.Lsp.TextDocumentEdit) (newSelection?_1 : Option Lean.Lsp.Range) (title?_1 : Option String),
  ({ edit := edit, newSelection? := newSelection?, title? := title? } =
      { edit := edit_1, newSelection? := newSelection?_1, title? := title?_1 }) =
    (edit = edit_1 ∧ newSelection? = newSelection?_1 ∧ title? = title?_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesKernel.iso_inv_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.ι f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (G.map f)) h
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/mBzV1Rx.png) commute.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U)
      ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
              (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app
        (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k))
          (Opposite.unop
            (Opposite.op
              ((TopologicalSpace.Opens.map
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
                        (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1
                (Opposite.unop (Opposite.op U))))))
        ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))
-- Mathlib.RingTheory.WittVector.InitTail
/-- `WittVector.select P x`, for a predicate `P : ℕ → Prop` is the Witt vector
whose `n`-th coefficient is `x.coeff n` if `P n` is true, and `0` otherwise.
 -/
WittVector.select : {p : ℕ} → {R : Type u_1} → [CommRing R] → (ℕ → Prop) → WittVector p R → WittVector p R
-- Mathlib.Algebra.CharP.Invertible
/-- In a ring of characteristic `p`, `(n : R)` is invertible when `n` is coprime with `p`, with
inverse `n.gcdA p`.  -/
invertibleOfCoprime : {R : Type u_1} → [inst : Ring R] → {p : ℕ} → [CharP R p] → {n : ℕ} → n.Coprime p → Invertible ↑n
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.pullback_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint],
  SheafOfModules.pullbackComp (CategoryTheory.CategoryStruct.id S) φ =
    CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pullbackId S) (SheafOfModules.pullback φ) ≪≫
      (SheafOfModules.pullback φ).leftUnitor
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D'),
  (CategoryTheory.StructuredArrow.prodEquivalence S S' T T').counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.StructuredArrow.prodInverse S S' T T').comp
                (CategoryTheory.StructuredArrow.prodFunctor S S' T T')).obj
            f))
      ⋯
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.left : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Ordered → l.Ordered
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.GrothendieckTopology.close_eq_self_of_isClosed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  {S : CategoryTheory.Sieve X}, J₁.IsClosed S → J₁.close S = S
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.cospanUnop_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanUnop f g).hom.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.unop X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.unop Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.unop Z)).hom
-- Mathlib.Algebra.GroupWithZero.Defs
CommMonoidWithZero.mk : {M₀ : Type u_2} →
  [toCommMonoid : CommMonoid M₀] →
    [toZero : Zero M₀] → (∀ (a : M₀), 0 * a = 0) → (∀ (a : M₀), a * 0 = 0) → CommMonoidWithZero M₀
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.all_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {p : (a : α) → β a → Bool},
  ((↑m).toList.all fun x => p x.fst x.snd) = (↑m).all p
-- Mathlib.Algebra.Lie.Basic
LieAlgebra.ext_iff : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} {x y : LieAlgebra R L},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.Algebra.Ring.Units
Units.divp_add : ∀ {α : Type u} [inst : Semiring α] (a b : α) (u : αˣ), a /ₚ u + b = (a + b * ↑u) /ₚ u
-- Mathlib.Data.List.Sym
List.setOfPred_mem_sym2 : ∀ {α : Type u_1} {xs : List α}, {z | z ∈ xs.sym2} = {x | x ∈ xs}.sym2
-- Mathlib.Control.Bifunctor
/-- Left map of a bifunctor.  -/
Bifunctor.fst : {F : Type u₀ → Type u₁ → Type u₂} → [Bifunctor F] → {α α' : Type u₀} → {β : Type u₁} → (α → α') → F α β → F α' β
-- Batteries.Data.Nat.Lemmas
Nat.casesAuxOn_succ : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive (n + 1)) (n : ℕ),
  Nat.casesAuxOn (n + 1) zero succ = succ n
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_inr : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid N),
  Submonoid.map (MonoidHom.inr M N) s = ⊥.prod s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (Std.ExtDHashMap.Const.insertMany m l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNegZeroClass.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : NegZeroClass G],
  Filter.Germ.instNegZeroClass = { toZero := Filter.Germ.instZero, toNeg := Filter.Germ.instNeg, neg_zero := ⋯ }
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.fromSum_map_inl : ∀ {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] {c c' : C} (f : c ⟶ c'),
  (CategoryTheory.Join.fromSum C D).map ((CategoryTheory.Sum.inl_ C D).map f) = (CategoryTheory.Join.inclLeft C D).map f
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The weighted degree of a nonzero weighted homogeneous polynomial is well-defined.  -/
MvPolynomial.IsWeightedHomogeneous.inj_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {m n : M} {w : σ → M},
  φ ≠ 0 → MvPolynomial.IsWeightedHomogeneous w φ m → MvPolynomial.IsWeightedHomogeneous w φ n → m = n
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.LFunction.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (Φ Φ_1 : ZMod N → ℂ),
  Φ = Φ_1 → ∀ (s s_1 : ℂ), s = s_1 → ZMod.LFunction Φ s = ZMod.LFunction Φ_1 s_1
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.le_comap_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), p ≤ Submodule.comap f (Submodule.map f p)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyRingEquiv_eq_coeff_zero : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : IsEmpty σ] {x : MvPolynomial σ R},
  (MvPolynomial.isEmptyRingEquiv R σ) x = MvPolynomial.coeff 0 x
-- Mathlib.Combinatorics.Additive.Dissociation
not_mulDissociated : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α},
  ¬MulDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.isLocallyNoetherian_Spec : ∀ {R : CommRingCat}, AlgebraicGeometry.IsLocallyNoetherian (AlgebraicGeometry.Spec R) ↔ IsNoetherianRing ↑R
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Given a set `S`, `S.matrix` is the set of matrices `M`
all of whose entries `M i j` belong to `S`.  -/
Set.matrix : {m : Type u_2} → {n : Type u_3} → {α : Type v} → Set α → Set (Matrix m n α)
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence preserves non-negative distance. Forward direction of `congruent_iff_nndist_eq`.  -/
Congruent.nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- In a symmetric monoidal category, the left distributivity is equal to
the right distributivity up to braiding isomorphisms.  -/
CategoryTheory.coprodComparison_tensorLeft_braiding_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.BraidedCategory C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z) (β_ X (Y ⨿ Z)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ X Y).hom (β_ X Z).hom)
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z)
-- Lean.Meta.Tactic.SplitIf
/-- Simplify the `if-then-else` targeted by the `split` tactic. If `useNewSemantics` is `true`, the flag
`backward.split` is ignored.
 -/
Lean.Meta.simpIfTarget : Lean.MVarId → optParam Bool false → optParam Bool false → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_uIcc : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
  x ∈ Finset.uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderivWithin_neg` -/
mvfderivWithin_fun_neg : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g : M → F} {x : M}, UniqueMDiffAt[s] x → (d[s] fun i => -g i) x = -d[s] g x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → Option γ},
  t.WF →
    (Std.TreeMap.Raw.filterMap f t).toList =
      List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) t.toList
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The `aleph` function gives the infinite cardinals listed by their ordinal index. `aleph 0 = ℵ₀`,
`aleph 1 = succ ℵ₀` is the first uncountable cardinal, and so on.

For a version including finite cardinals, see `Cardinal.preAleph`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℵ_` in identifiers is `aleph`. -/
Cardinal.termℵ_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Groupoid
/-- A `LargeGroupoid` is a groupoid
where the objects live in `Type (u+1)` while the morphisms live in `Type u`.
 -/
CategoryTheory.LargeGroupoid : Type (u + 1) → Type (u + 1)
-- Mathlib.Tactic.Linarith.Parsing
/-- `SumOfMonom m` lifts `m` to a sum with coefficient `1`.  -/
Mathlib.Tactic.Linarith.SumOfMonom : Mathlib.Tactic.Linarith.Monom → Mathlib.Tactic.Linarith.Sum
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A wide pullback shape for any type `J` can be written simply as `Option J`.  -/
CategoryTheory.Limits.WidePullbackShape : Type w → Type w
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetCreatesPullbackOfLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] →
            CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g)
              AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget SemiRingCat)
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotKerEquivRange_symm_apply_image : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x ∈ f.range),
  f.quotKerEquivRange.symm ⟨f x, h⟩ = f.ker.mkQ x
-- Init.Control.Lawful.Instances
StateT.run_bind_lift : ∀ {m : Type u → Type u_1} {β α σ : Type u} [inst : Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ),
  (StateT.lift x >>= f).run s = do
    let a ← x
    (f a).run s
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.norm_tsumCLM_le : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E], ‖lp.tsumCLM 𝕜 α E‖ ≤ 1
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C),
  ((CategoryTheory.flippingIso.hom.toFunctor.obj F).obj k).obj j = (F.obj j).obj k
-- Mathlib.Tactic.Choose
/-- The syntax reference for the identifier (for hover info)  -/
Mathlib.Tactic.Choose.ChooseArg.ref : Mathlib.Tactic.Choose.ChooseArg → Lean.Syntax
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.iInf_pow_smul : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff I M → ⨅ n, I ^ n • ⊤ = ⊥
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.sigma : {I : Type w₁} →
  {C : I → Type u₁} →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      CategoryTheory.Category.{max (max u₁ v₁) w₁, max u₁ w₁} ((i : I) × C i)