mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`.  -/
CategoryTheory.preservesLimit_of_lan_preservesLimit : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor C D) (J : Type u) [inst_2 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.PreservesLimitsOfShape J F.op.lan], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_zero : EReal.exp 0 = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.string : Lean.Lsp.SemanticTokenType
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueLinearEquiv_symm_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [inst : Unique m] [inst_1 : Unique n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Module R A] (a : A),
  Matrix.uniqueLinearEquiv.symm a = Matrix.uniqueAddEquiv.invFun a
-- Mathlib.Topology.Order.PartialSups
ContinuousAt.partialSups_apply : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {x : X},
  (∀ k ≤ n, ContinuousAt (f k) x) → ContinuousAt (fun a => (partialSups fun x => f x a) n) x
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel.trans : ∀ {R : Type u} [inst : Rack R] {a b c : Rack.PreEnvelGroup R},
  Rack.PreEnvelGroupRel R a b → Rack.PreEnvelGroupRel R b c → Rack.PreEnvelGroupRel R a c
-- Batteries.Data.List.Lemmas
List.idxOf_add_mem_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} [inst : BEq α] (s : ℕ),
  List.idxOf x xs < xs.length → List.idxOf x xs + s ∈ List.idxsOf x xs s
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.unStM : Lean.Elab.Do.ControlStack → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.toSubsemiring_le_iff : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {S₁ S₂ : StarSubsemiring R},
  S₁.toSubsemiring ≤ S₂.toSubsemiring ↔ S₁ ≤ S₂
-- Init.Data.SInt.Lemmas
Int32.le_or_lt : ∀ (a b : Int32), a ≤ b ∨ b < a
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_apply : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)) (x : X),
  (ContinuousMap.realToRCLike 𝕜 f) x = ↑(f x)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).p =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv φ.τ₂) h.p
-- Lean.Linter.UnusedVariables
/-- Visit a `PersistentHashMap.Node`, collecting all fvars in it into `fvarUses`  -/
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.visitAssignments.visitNode : IO.Ref (Std.HashSet USize) →
  IO.Ref (Std.HashSet Lean.FVarId) →
    Lean.PersistentHashMap.Node Lean.MVarId Lean.Expr → Lean.MonadCacheT Lean.Expr Unit IO Unit
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_dite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι)
  (b : (x : ι) → a = x → M), (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The identity function has bounded variation on every interval `Icc a b`.  -/
BoundedVariationOn.id_Icc : ∀ (a b : ℝ), BoundedVariationOn id (Set.Icc a b)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal},
  Measurable f →
    ∀ {s : Set β},
      MeasurableSet s →
        ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Geometry.Manifold.DerivationBundle
instAlgebraPointedContMDiffMap : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_2) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → (n : WithTop ℕ∞) → (x : M) → Algebra 𝕜 (PointedContMDiffMap 𝕜 I M n x)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Pullback an additive monoid object along a fully faithful oplax monoidal functor.  -/
CategoryTheory.Functor.FullyFaithful.addMonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.OplaxMonoidal] →
                F.FullyFaithful → (X : C) → [CategoryTheory.AddMonObj (F.obj X)] → CategoryTheory.AddMonObj X
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.below.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure' x → Prop} {x y : C} (f : x ⟶ y) (hf : W f),
  CategoryTheory.MorphismProperty.multiplicativeClosure'.below ⋯
-- Batteries.Data.Fin.Coding
Fin.decodeSubtype_encodeSubtype : ∀ {n : ℕ} (P : Fin n → Prop) [inst : DecidablePred P] (x : { x // P x }),
  Fin.decodeSubtype P (Fin.encodeSubtype P x) = x
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instAdd : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → Add (LieDerivation R L M)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The bifibrant resolution functor from the homotopy category of
cofibrant objects to the homotopy category of bifibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject.HoCat C) (HomotopicalAlgebra.BifibrantObject.HoCat C)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.of_nat_of_neg : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℤ → G},
  (Summable fun n => f ↑n) → (Summable fun n => f (-↑n)) → Summable f
-- Mathlib.Topology.Algebra.Valued.WithVal
NumberField.RingOfIntegers.withValEquiv_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [inst_1 : Field K] (v : Valuation K Γ₀)
  (R : Type u_4) [inst_2 : CommRing R] [inst_3 : Algebra R K] [inst_4 : IsIntegralClosure R ℤ K]
  (a : NumberField.RingOfIntegers (WithVal v)),
  (NumberField.RingOfIntegers.withValEquiv v R) a =
    { toEquiv := ↑(IsIntegralClosure.equiv ℤ R (WithVal v) (NumberField.RingOfIntegers (WithVal v))).symm,
        map_mul' := ⋯, map_add' := ⋯ }
      a
-- Mathlib.Data.Finsupp.Basic
/-- When `g` preserves addition, `mapRange` and `mapDomain` commute.  -/
Finsupp.mapDomain_mapRange : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  (f : α → β) (v : α →₀ M) (g : M → N) (h0 : g 0 = 0),
  (∀ (x y : M), g (x + y) = g x + g y) →
    Finsupp.mapDomain f (Finsupp.mapRange g h0 v) = Finsupp.mapRange g h0 (Finsupp.mapDomain f v)
-- Mathlib.RingTheory.Ideal.IsPrimary
/-- A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`.  -/
Ideal.isPrimary_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R},
  I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_false_mid : ∀ {a c : Bool}, a.atLeastTwo false c = (a && c)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_injective : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V], Function.Injective DFunLike.coe
-- Lean.Data.NameTrie
Lean.instBEqNamePart : BEq Lean.NamePart
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.essentiallySmall_monoOver_iff_small_subobject : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (X : C),
  CategoryTheory.EssentiallySmall.{w, v, max u₁ v} (CategoryTheory.MonoOver X) ↔
    Small.{w, max u₁ v} (CategoryTheory.Subobject X)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y)
  [inst : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.toHom = X
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.comp₂ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Z : Type u_7} {f : X → Y₁} {g : X → Y₂},
  IsLocallyConstant f → IsLocallyConstant g → ∀ (h : Y₁ → Y₂ → Z), IsLocallyConstant fun x => h (f x) (g x)
-- Mathlib.Order.Basic
Decidable.ne_iff_lt_iff_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableEq α], (a ≠ b ↔ a < b) ↔ a ≤ b
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- The exponential of a convergent sum of real logs is the corresponding infinite product.  -/
Real.rexp_tsum_eq_tprod : ∀ {ι : Type u_1} {f : ι → ℝ},
  (∀ (i : ι), 0 < f i) → (Summable fun i => Real.log (f i)) → Real.exp (∑' (i : ι), Real.log (f i)) = ∏' (i : ι), f i
-- Mathlib.Order.Cover
Pi.covBy_iff_exists_right_eq : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i}
  [inst_1 : DecidableEq ι], a ⋖ b ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.truth_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Sheaf.truth J).hom = CategoryTheory.Subfunctor.lift (CategoryTheory.Presheaf.truth C) ⋯
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.ae_of_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} ⦃f : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) → ∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable f (η x)
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Server.mk : Std.Http.Internal.Mock.SharedState✝ → Std.Http.Internal.Mock.Server
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
QuadraticModuleCat.instSymmetricCategory : {R : Type u} → [inst : CommRing R] → [inst_1 : Invertible 2] → CategoryTheory.SymmetricCategory (QuadraticModuleCat R)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.bijective_left : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst : AddCommGroup M} {inst_1 : AddCommGroup N} {inst_2 : CommRing R}
  {inst_3 : Module R M} {inst_4 : Module R N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsPerfPair], Function.Bijective ⇑p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_inter_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.Equilateral.dist_eq : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  {s : Affine.Simplex R P n},
  s.Equilateral →
    ∀ {i₁ i₂ i₃ i₄ : Fin (n + 1)},
      i₁ ≠ i₂ → i₃ ≠ i₄ → dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions.toWorkDoneProgressOptions : Lean.Lsp.DocumentColorOptions → Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Rewrite.mk.inj : ∀ {symm : Bool} {proof replacement : Lean.Expr} {stringLength : ℕ} {extraGoals : Array (Lean.MVarId × Lean.BinderInfo)}
  {makesNewMVars symm_1 : Bool} {proof_1 replacement_1 : Lean.Expr} {stringLength_1 : ℕ}
  {extraGoals_1 : Array (Lean.MVarId × Lean.BinderInfo)} {makesNewMVars_1 : Bool},
  { symm := symm, proof := proof, replacement := replacement, stringLength := stringLength, extraGoals := extraGoals,
        makesNewMVars := makesNewMVars } =
      { symm := symm_1, proof := proof_1, replacement := replacement_1, stringLength := stringLength_1,
        extraGoals := extraGoals_1, makesNewMVars := makesNewMVars_1 } →
    symm = symm_1 ∧
      proof = proof_1 ∧
        replacement = replacement_1 ∧
          stringLength = stringLength_1 ∧ extraGoals = extraGoals_1 ∧ makesNewMVars = makesNewMVars_1
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffWithinAt_of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E}
  {n : WithTop ℕ∞} [Subsingleton F], ContDiffWithinAt 𝕜 n f s x
-- Mathlib.Data.Set.Monotone
Set.EqOn.congr_monotoneOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Set.EqOn f₁ f₂ s → (MonotoneOn f₁ s ↔ MonotoneOn f₂ s)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Icc_left_eq_Icc_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a - 1 ≤ b → insert (a - 1) (Finset.Icc a b) = Finset.Icc (a - 1) b
-- Mathlib.Data.Finsupp.Option
Finsupp.sum_option_index_smul : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Option α →₀ R) (b : Option α → M),
  (f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (some a)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : MonoidAlgebra R N), MonoidAlgebra.comapDomain f hf x = MonoidAlgebra.ofCoeff (Finsupp.comapDomain f x.coeff ⋯)
-- Mathlib.Order.WithBot
WithTop.strictMono_map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono (WithTop.map f) ↔ StrictMono f
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.unique_lift : ∀ {G : Type u_1} {inst : CategoryTheory.Groupoid G} [self : IsFreeGroupoid G] {X : Type v} [inst_1 : Group X]
  (f : Quiver.Labelling (IsFreeGroupoid.Generators G) X),
  ∃! F, ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (IsFreeGroupoid.of g) = f g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.h : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.go.eq_1 : ∀ (k k_1 : ℤ),
  Lean.Grind.CommRing.Poly.addConst.go k (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.num (k_1 + k)
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_inv_eq_mul_inv_iff : ∀ {α : Type u} [inst : CommMonoid α] (a c : α) (b d : αˣ), a * ↑b⁻¹ = c * ↑d⁻¹ ↔ a * ↑d = c * ↑b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N O : CategoryTheory.Mod D A} (f : M.Hom N) (g : N.Hom O),
  (CategoryTheory.Mod.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (f : Y ⟶ h.pullback)
  (f_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam)
  (f_p₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam)
  (f_p :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam)
  (f_1 : Y ⟶ h.pullback)
  (f_p₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam)
  (f_p₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam)
  (f_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam),
  ({ f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p } = { f := f_1, f_p₁ := f_p₁_1, f_p₂ := f_p₂_1, f_p := f_p_1 }) =
    (f = f_1)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral value of a polynomial is nonnegative.  -/
spectralValue_nonneg : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R), 0 ≤ spectralValue p
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv
      (CategoryTheory.Limits.coprod.desc
        (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f))
        (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f))) =
    AlgebraicGeometry.Scheme.Hom.fromNormalization f
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_one : Real.Gamma 1 = 1
-- Init.Core
/-- The highest regular priority for spawned tasks: `8`.

Spawning a task with a priority higher than `Task.Priority.max` is not an error but will spawn a
dedicated worker for the task. This is indicated using `Task.Priority.dedicated`. Regular priority
tasks are placed in a thread pool and worked on according to their priority order.
 -/
Task.Priority.max : Task.Priority
-- Init.Data.Float.Model.Float32
/-- Converts an `ISize` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofISize : ISize → Float32.Model
-- Init.Data.Order.Ord
Std.instReflCmpCompareOnOfReflOrd : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Ord β] [Std.ReflOrd β], Std.ReflCmp (compareOn f)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictFDerivAt_iff_hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.OplaxTrans.Modification η θ)
  {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f) h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) h)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b c : ℤ)
  (h : a + b = c),
  CategoryTheory.shiftFunctorAdd' (CategoryTheory.Pretriangulated.Triangle C) a b c h =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b c h
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Unicode symbols in mathlib that have no restrictions on whether they are followed by a selector
or which selector they are followed by.  -/
Mathlib.Linter.TextBased.UnicodeLinter.unrestricted : Array Char
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.ker_le_fixedSubmodule_transvection : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hfv : f v = 0), LinearMap.ker f ≤ (↑(LinearEquiv.transvection hfv)).fixedSubmodule
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get? (m₁.diff m₂) k = none
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.mersenne_int_ne_zero : ∀ (p : ℕ), p ≠ 0 → 2 ^ p - 1 ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.iSup_eq_closure : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} (p : ι → AddSubgroup G),
  ⨆ i, p i = AddSubgroup.closure (⋃ i, ↑(p i))
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsClosedMap f
-- Init.Data.Vector.Lemmas
/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array.  -/
Vector.getElem_append_left' : ∀ {α : Type u_1} {m i n : ℕ} {xs : Vector α m} (hi : i < m) (ys : Vector α n), xs[i] = (xs ++ ys)[i]