mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_subset_skeletonLT`. -/
Topology.CWComplex.openCell_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Batteries.Data.List.Perm
List.Perm.idxBij_injective : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys), Function.Injective h.idxBij
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.instPartialOrder : {V : Type u_2} → PartialOrder (Digraph V)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_inf_eq : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  (W W' : Subspace K V₁),
  Submodule.dualAnnihilator (W ⊓ W') = Submodule.dualAnnihilator W ⊔ Submodule.dualAnnihilator W'
-- Lean.ReducibilityAttrs
Lean.getReducibilityStatusCore : Lean.Environment → Lean.Name → Lean.ReducibilityStatus
-- Mathlib.RingTheory.Ideal.Cotangent
/-- Lift a linear map `f : I →ₗ[R] M` that vanishes on products to a linear map on the
cotangent space `I ⧸ I ^ 2`.  -/
Ideal.Cotangent.lift : {R : Type u} →
  [inst : CommRing R] →
    {S : Type u_3} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {I : Ideal S} →
            {M : Type u_4} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] → (f : ↥I →ₗ[R] M) → (∀ (x y : ↥I), f (x * y) = 0) → I.Cotangent →ₗ[R] M
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
/-- The maximal spectrum of a commutative (semi)ring `R` is the type of all
maximal ideals of `R`.  -/
MaximalSpectrum : (R : Type u_1) → [CommSemiring R] → Type u_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The canonical map `X ⨿ₛ Y ⟶ X ⨿ₜ Y` given `S ⟶ T`.  -/
CategoryTheory.Limits.pushout.mapLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y S T : C} →
      (f : T ⟶ X) →
        (g : T ⟶ Y) →
          (i : S ⟶ T) →
            [inst_1 : CategoryTheory.Limits.HasPushout f g] →
              [inst_2 :
                  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f)
                    (CategoryTheory.CategoryStruct.comp i g)] →
                CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp i f)
                    (CategoryTheory.CategoryStruct.comp i g) ⟶
                  CategoryTheory.Limits.pushout f g
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_add_right_neg_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.Measure.map (fun t => -(g + t)) μ = μ
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.edist_continuousMapMk : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α] [inst_2 : CompactSpace α]
  {f g : UniformFun α β} (hf : Continuous (UniformFun.toFun f)) (hg : Continuous (UniformFun.toFun g)),
  edist { toFun := UniformFun.toFun f, continuous_toFun := hf }
      { toFun := UniformFun.toFun g, continuous_toFun := hg } =
    edist f g
-- Mathlib.Data.Matrix.Basic
RingEquiv.mopMatrix_symm_apply : ∀ {m : Type u_2} [inst : Fintype m] {α : Type u_14} [inst_1 : Mul α] [inst_2 : AddCommMonoid α] (M : (Matrix m m α)ᵐᵒᵖ),
  RingEquiv.mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op
-- Mathlib.Data.Nat.Count
Nat.count_succ_eq_succ_count_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p (n + 1) = Nat.count p n + 1 ↔ p n
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.one : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MCasesPat
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraints : Array String → Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact → String
-- Init.Omega.Constraint
/-- A lower bound.  -/
Lean.Omega.Constraint.lowerBound : Lean.Omega.Constraint → Lean.Omega.LowerBound
-- Mathlib.Computability.NFA
NFA.acceptsFrom_iUnion : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} (s : ι → Set σ),
  M.acceptsFrom (⋃ i, s i) = ⋃ i, M.acceptsFrom (s i)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X}
  (hf : CategoryTheory.CategoryStruct.comp f f = f)
  {c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i).section_ =
    i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Lean.Meta.Basic
Lean.Meta.InferTypeCache : Type
-- Lean.DocString.Types
/-- Inline literal code, typically rendered in a monospace font.
 -/
Lean.Doc.Inline.code : {i : Type u} → String → Lean.Doc.Inline i
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData.default : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Mathlib.NumberTheory.Padics.WithVal
Padic.withValUniformEquiv_norm_le_one_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (x : (Rat.padicValuation p).Completion),
  ‖Padic.withValUniformEquiv x‖ ≤ 1 ↔ Valued.v x ≤ 1
-- Mathlib.AlgebraicGeometry.Limits
/-- A scheme is initial if its underlying space is empty .  -/
AlgebraicGeometry.isInitialOfIsEmpty : {X : AlgebraicGeometry.Scheme} → [IsEmpty ↥X] → CategoryTheory.Limits.IsInitial X
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forgetCone_pt : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T), (CategoryTheory.Under.forgetCone X).pt = X
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- **Alias** of `Norm.norm`. -/
PiTensorProduct.projectiveSeminormFun : {E : Type u_8} → [self : Norm E] → E → ℝ
-- Mathlib.Data.Finmap
Finmap.keysLookupEquiv_apply_coe_snd : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s : Finmap β) (i : α),
  (↑(Finmap.keysLookupEquiv s)).2 i = Finmap.lookup i s
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_1.eq : ∀ {ε : Type u} {α : Type v} {motive_1 : Lean.AsyncList ε α → Sort u_1}
  {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1}
  {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1}
  (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) (F_1 : (t : Lean.AsyncList ε α) → t.below → motive_1 t)
  (F_2 : (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t)
  (F_3 : (t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t)
  (F_4 : (t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t),
  Lean.AsyncList.brecOn_1 t F_1 F_2 F_3 F_4 = F_2 t (Lean.AsyncList.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearIsometryEquiv.toMatrix_mem_unitaryGroup : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {G : Type u_7}
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] G) (b : OrthonormalBasis ι 𝕜 E)
  (b' : OrthonormalBasis ι 𝕜 G), (LinearMap.toMatrix b.toBasis b'.toBasis) ↑f.toLinearEquiv ∈ Matrix.unitaryGroup ι 𝕜
-- Lean.Expr
Lean.Int.mkInstHMod : Lean.Expr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.HashMap.filter f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]).get!
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.subset_adjoin : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A}, s ⊆ ↑(NonUnitalAlgebra.adjoin R s)
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_infty_iff : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f ⊤ ↔ BddAbove (Set.range fun i => ‖f i‖)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.norm_le_norm_mul_of_mem : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {k : 𝕜}, k ∈ spectrum 𝕜 a → ‖k‖ ≤ ‖a‖ * ‖1‖
-- Mathlib.CategoryTheory.Skeletal
/-- A natural isomorphism between `X ↦ ⟦X⟧ ↦ ⟦FX⟧` and `X ↦ FX ↦ ⟦FX⟧`. On the level of
categories, these are `C ⥤ Skeleton C ⥤ Skeleton D` and `C ⥤ D ⥤ Skeleton D`. So this says that
the square formed by these 4 objects and 4 functors commutes.  -/
CategoryTheory.Functor.toSkeletonFunctorCompMapSkeletonIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (CategoryTheory.toSkeletonFunctor C).comp F.mapSkeleton ≅ F.comp (CategoryTheory.toSkeletonFunctor D)
-- Mathlib.Order.Filter.Pointwise
Filter.instZPow.eq_1 : ∀ {α : Type u_2} [inst : One α] [inst_1 : Mul α] [inst_2 : Inv α],
  Filter.instZPow = { pow := fun s n => zpowRec npowRec n s }
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_self_iff_empty : ∀ {α : Type u_2} (s : Finset α), Disjoint s s ↔ s = ∅
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
HomotopyCategory.composableArrowsFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (f : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1),
  (HomotopyCategory.composableArrowsFunctor C).obj f =
    CochainComplex.mappingCone
      (f.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1 HomotopyCategory.composableArrowsFunctor._proof_2)
-- Lean.Data.PersistentArray
Lean.PersistentArray.toArray : {α : Type u} → Lean.PersistentArray α → Array α
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_ceil_mul_div_atTop : ∀ {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Field R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  [OrderTopology R] [inst_5 : FloorRing R] {a : R},
  0 ≤ a → Filter.Tendsto (fun x => ↑⌈a * x⌉₊ / x) Filter.atTop (nhds a)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Promote the morphism `F.mapId x : 𝟙 (F.obj x) ⟶ F.map (𝟙 x)`
to an isomorphism when `F` is strictly unitary.  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C) →
          (x : B) → CategoryTheory.CategoryStruct.id (F.obj x) ≅ F.map (CategoryTheory.CategoryStruct.id x)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_himp_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α),
  (s.inf fun b => f b ⇨ a) = s.sup f ⇨ a
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Modifications between strong transformations of oplax functors are equivalent to modifications
between the underlying oplax transformations.  -/
CategoryTheory.Oplax.StrongTrans.Modification.equivOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ) ≃
              CategoryTheory.Oplax.StrongTrans.Modification η θ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {fallback : α}, cmp ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.RingTheory.Derivation.DifferentialRing
mem_range_of_deriv_eq_zero : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Differential B] [Differential.ContainConstants A B] {x : B}, x′ = 0 → x ∈ (algebraMap A B).range
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ h.leftHomologyIso.hom =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.π
-- Mathlib.Analysis.Calculus.FDeriv.Pow
DifferentiableWithinAt.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ∀ (n : ℕ), DifferentiableWithinAt 𝕜 (fun x => f x ^ n) s x
-- Init.PropLemmas
exists_prop_eq' : ∀ {α : Sort u_1} {a' : α} {p : (a : α) → a' = a → Prop}, (∃ a, ∃ (h : a' = a), p a h) ↔ p a' ⋯
-- Init.Data.BitVec.Lemmas
BitVec.ule_eq_decide_le : ∀ {w : ℕ} {x y : BitVec w}, x.ule y = decide (x ≤ y)
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for `initialize_simps_projections`.  -/
Lean.Parser.Command.simpsProj : Lean.ParserDescr
-- Mathlib.Data.Nat.GCD.Basic
/-- **Alias** of `Nat.dvd_lcm_of_dvd_left`. -/
Nat.Dvd.dvd.nat_lcm_right : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ b.lcm c
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Finset.stronglyMeasurable_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (∑ i ∈ s, f i)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instOne : One Cardinal.{u}
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse =
    CategoryTheory.CategoryOfElements.fromStructuredArrow F
-- Mathlib.Computability.NFA
NFA.toDFA_correct : ∀ {α : Type u} {σ : Type v} {M : NFA α σ}, M.toDFA.accepts = M.accepts
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- the index type of the covering  -/
SheafOfModules.LocalGeneratorsData.I : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {M : SheafOfModules R} →
          [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → M.LocalGeneratorsData → Type w
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.below : {α : Type u_2} →
  {g : Set (Set α)} →
    {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop} →
      {a : Set α} → Filter.CountableGenerateSets g a → Prop
-- Mathlib.CategoryTheory.Sites.Monoidal
/-- The monoidal category structure on `Sheaf J A` obtained in `Sheaf.monoidalCategory` is
braided when `A` is braided.  -/
CategoryTheory.Sheaf.braidedCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.MonoidalCategory A] →
            [inst_3 : J.W.IsMonoidal] →
              [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                [CategoryTheory.BraidedCategory A] → CategoryTheory.BraidedCategory (CategoryTheory.Sheaf J A)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatIso_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] [inst_5 : LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F),
  (LF'.leftDerivedNatIso LF α' α W τ).hom = LF'.leftDerivedNatTrans LF α' α W τ.hom
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.trans : ∀ {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β}, H.IsSubgraph G → G.IsSubgraph G₁ → H.IsSubgraph G₁
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.countP_nsmul : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) (n : ℕ),
  Multiset.countP p (n • s) = n * Multiset.countP p s
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_one : ∀ (f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}), Ordinal.blsub 1 f = Order.succ (f 0 ⋯)
-- Lean.Data.Lsp.Internal
/-- Start line of selection range.  -/
Lean.Lsp.DeclInfo.selectionRangeStartPosLine : Lean.Lsp.DeclInfo → ℕ
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.projective_quotient : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  (self : Module.Grassmannian R M k), Module.Projective R (M ⧸ self.toSubmodule)
-- Mathlib.FieldTheory.SplittingField.Construction
/-- [Stacks Tag 09HU](https://stacks.math.columbia.edu/tag/09HU) (Splitting part) -/
Polynomial.SplittingField.splits : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), (Polynomial.map (algebraMap K f.SplittingField) f).Splits
-- Init.Data.List.Monadic
List.zipWithM'.match_1.congr_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 : List α) (x_3 : List β),
  x = x_2 →
    x_1 = x_3 →
      (∀ (x : α) (xs : List α) (y : β) (ys : List β), x_2 = x :: xs → x_3 = y :: ys → False) →
        (match x, x_1 with
          | x :: xs, y :: ys => h_1 x xs y ys
          | x, x_5 => h_2 x x_5) ≍
          h_2 x_2 x_3
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_eval_eq_map : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix n n (Polynomial R)) (r : R),
  Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = M.map (Polynomial.eval r)
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {version? : Option ℕ} {uri_1 : Lean.Lsp.DocumentUri} {version?_1 : Option ℕ},
  { uri := uri, version? := version? } = { uri := uri_1, version? := version?_1 } → uri = uri_1 ∧ version? = version?_1
-- Mathlib.Order.SuccPred.Limit
WithBot.isPredPrelimit_iff : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] {x : WithBot α},
  Order.IsPredPrelimit x ↔ x = ⊥ ∨ ∃ y, x = ↑y ∧ Order.IsPredPrelimit y
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (bs : List β) (h_1 : (bs : List β) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `nnnorm_le_nnnorm_add_nnnorm_sub'`. -/
nnnorm_le_insert' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps.mk.injEq : ∀ (html html_1 : ProofWidgets.Html), ({ html := html } = { html := html_1 }) = (html = html_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty =
    ((t.isEmpty || t.size == 1 && Std.DTreeMap.Internal.Impl.contains k t) &&
      (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone)
-- Mathlib.Analysis.Quaternion
Quaternion.inner_def : ∀ (a b : Quaternion ℝ), inner ℝ a b = (a * star b).re
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_le_iff_le_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N}
  {S : L.Substructure M} {T : L.Substructure N},
  FirstOrder.Language.Substructure.map f S ≤ T ↔ S ≤ FirstOrder.Language.Substructure.comap f T
-- Mathlib.GroupTheory.Subgroup.Simple
MulEquiv.isSimpleGroup_congr : ∀ {G : Type u_1} [inst : Group G] {H : Type u_3} [inst_1 : Group H] (e : G ≃* H), IsSimpleGroup G ↔ IsSimpleGroup H
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.fvar.inj : ∀ {moduleName id moduleName_1 id_1 : String},
  Lean.Lsp.RefIdent.fvar moduleName id = Lean.Lsp.RefIdent.fvar moduleName_1 id_1 →
    moduleName = moduleName_1 ∧ id = id_1
-- Mathlib.Topology.Constructions
Filter.eventually_nhdsSet_prod_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y}
  {p : X × Y → Prop},
  (∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in nhds x, px x') ∧
            ∃ py, (∀ᶠ (y' : Y) in nhds y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {t : Set α},
  MeasureTheory.IntegrableOn f t μ →
    (∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ) → 0 ≤ᵐ[μ.restrict t] f
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α},
  AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∩ t)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.of_subsingleton : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [Subsingleton ι],
  ProbabilityTheory.iCondIndepFun m' hm' f μ
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderCobaseChangeTrivialCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCobaseChange
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.top_eq : ∀ (C : Type u) [inst : CategoryTheory.CategoryStruct.{v, u} C], ⊤ = fun x x_1 x_2 => True
-- Mathlib.Order.Atoms
IsCoatom.ne_iff_eq_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → a ≤ b → (b ≠ a ↔ b = ⊤)