mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_le_neg_one_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, ⌊a⌋ ≤ -1 ↔ a < 0
-- Mathlib.Data.List.Lemmas
/-- **Alias** of `List.setOfPred_mem_eq_empty_iff`. -/
List.setOf_mem_eq_empty_iff : ∀ {α : Type u_1} {l : List α}, {x | x ∈ l} = ∅ ↔ l = []
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_neg : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Ring R],
  (∀ (x : R), v (-x) = v x) →
    ∀ (f : MvPowerSeries σ R), MvPowerSeries.gaussNorm v c (-f) = MvPowerSeries.gaussNorm v c f
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents'.app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app' : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    ∀ {X Y : C} (f : Y ⟶ X),
      CategoryTheory.CategoryStruct.comp (app' Y).inv (F.map f) =
        CategoryTheory.CategoryStruct.comp (G.map f) (app' X).inv)
  (X : C), (CategoryTheory.NatIso.ofComponents' app' naturality).app X = app' X
-- Mathlib.Order.Hom.Bounded
/-- Copy of a `BoundedOrderHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
BoundedOrderHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : BoundedOrder α] →
          [inst_3 : BoundedOrder β] → (f : BoundedOrderHom α β) → (f' : α → β) → f' = ⇑f → BoundedOrderHom α β
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.instInhabitedPair : {ι : Type u_1} →
  (M : ι → Type u_2) → [inst : (i : ι) → Monoid (M i)] → (i : ι) → Inhabited (Monoid.CoprodI.Word.Pair M i)
-- Mathlib.RingTheory.Morita.Matrix
moritaEquivalenceMatrix_eqv : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (R₀ : Type u_1)
  [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] (i : ι),
  (moritaEquivalenceMatrix R R₀ i).eqv = ModuleCat.matrixEquivalence R i
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanUnit_desc_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g)
  {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f s.extension ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.lanDesc s)) h) =
    CategoryTheory.CategoryStruct.comp s.unit h
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.coe_toIntermediateField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : Subfield L)
  (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ S), ↑(S.toIntermediateField algebra_map_mem) = ↑S
-- Mathlib.Probability.Moments.ComplexMGF
MeasureTheory.Measure.ext_of_complexMGF_id_eq : ∀ {μ μ' : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'],
  ProbabilityTheory.complexMGF id μ = ProbabilityTheory.complexMGF id μ' → μ = μ'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.monotone_arcsin : Monotone Real.arcsin
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- The range of a finite group under a group homomorphism is finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
presence of `Fintype N`.  -/
MonoidHom.fintypeRange : {G : Type u_1} →
  [inst : Group G] →
    {N : Type u_3} → [inst_1 : Group N] → [Fintype G] → [DecidableEq N] → (f : G →* N) → Fintype ↥f.range
-- Mathlib.NumberTheory.Cyclotomic.Basic
IntermediateField.isCyclotomicExtension_eq : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension S K ↥F₁] [h₂ : IsCyclotomicExtension S K ↥F₂], F₁ = F₂
-- Init.Data.Int.Lemmas
Int.beq'.eq_1 : ∀ (a b : ℤ),
  a.beq' b =
    Int.rec (fun a => Int.rec (fun b => a.beq b) (fun x => false) b)
      (fun a => Int.rec (fun x => false) (fun b => a.beq b) b) a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.unop_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ Dᵒᵖ), e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_2}
  [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms D]
  [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms]
  [∀ {X Y : D} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F],
  F.PreservesEpimorphisms
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_nonpos : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, ⌈a⌉ ≤ 0 ↔ a ≤ 0
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `Multiplicative α →* β` as `α →+ Additive β`.  -/
MonoidHom.toAdditiveRight : {α : Type u_3} →
  {β : Type u_4} → [inst : AddZeroClass α] → [inst_1 : MulOneClass β] → (Multiplicative α →* β) ≃ (α →+ Additive β)
-- Mathlib.Data.Sum.Interval
_private.Mathlib.Data.Sum.Interval.0.Finset.sumLift₂.match_1.eq_2 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) (val : α₁)
  (val_1 : β₂) (h_1 : (a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (val : α₁) → (val_2 : β₂) → motive (Sum.inl val) (Sum.inr val_2))
  (h_3 : (val : α₂) → (val_2 : β₁) → motive (Sum.inr val) (Sum.inl val_2))
  (h_4 : (a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)),
  (match Sum.inl val, Sum.inr val_1 with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl val, Sum.inr val_2 => h_2 val val_2
    | Sum.inr val, Sum.inl val_2 => h_3 val val_2
    | Sum.inr a, Sum.inr b => h_4 a b) =
    h_2 val val_1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] (X Y : C) {Z : C}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)) h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → P 1 = W.negY P → (W.Nonsingular P ↔ W.Equation P ∧ (MvPolynomial.eval P) W.polynomialX ≠ 0)
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_iff_of_equiv : ∀ {X : Type u} {Y : Type u'} (e : X ≃ Y) (κ : Cardinal.{v}), HasCardinalLT X κ ↔ HasCardinalLT Y κ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsTopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [inst_2 : IsTopologicalRing R],
  IsTopologicalRing (SeparationQuotient R)
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `fallback` if no such element exists.
 -/
Std.TreeSet.getGTD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α → α
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeOutRequestMessageOfToJson : {α : Type u_1} → [Lean.ToJson α] → CoeOut (Lean.JsonRpc.Request α) Lean.JsonRpc.Message
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (r : R), (v.intAdicAbv hb) r < 1 ↔ r ∈ v.asIdeal
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating compatibility between `PatternModel` and `BackwardPattern`.

This extends `LawfulBackwardPattern`, but it is much stronger because it forces the
`BackwardPattern` to match the longest prefix of the given slice that matches the property
supplied by the `PatternModel` instance.
 -/
String.Slice.Pattern.Model.LawfulBackwardPatternModel : {ρ : Type} →
  (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → [String.Slice.Pattern.Model.PatternModel pat] → Prop
-- Lean.Compiler.ExternAttr
Lean.expandExternPatternAux : List String → (pattern : String) → pattern.Pos → String → String
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.ofFactorizationData_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i = h.i
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Taking a sum over `s : Finset ι` is the same as adding the value on a single
element `f a` to the sum over `s.erase a`.

See `Multiset.sum_map_erase` for the `Multiset` version.  -/
Finset.add_sum_erase : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
  a ∈ s → f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x
-- Mathlib.Topology.SmallInductiveDimension
_private.Mathlib.Topology.SmallInductiveDimension.0.hasSmallInductiveDimensionLT_of_smallInductiveDimension_lt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ}, smallInductiveDimension X < ↑n → HasSmallInductiveDimensionLT X n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.isEmpty.eq_2 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (x : RBTree.RBSet α cmp),
  (∀ (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil), x = ⟨RBTree.RBNode.nil, property⟩ → False) → x.isEmpty = false
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsGE X n],
  ∀ j ≤ WithBotTop.coe n, CategoryTheory.Limits.IsZero ((t.eTruncLT.obj j).obj X)
-- Lean.Elab.DefView
Lean.Elab.DefViewElabHeaderData.mk.sizeOf_spec : ∀ (shortDeclName declName : Lean.Name) (levelNames : List Lean.Name) (binderIds : Array Lean.Syntax) (numParams : ℕ)
  (type : Lean.Expr),
  sizeOf
      { shortDeclName := shortDeclName, declName := declName, levelNames := levelNames, binderIds := binderIds,
        numParams := numParams, type := type } =
    1 + sizeOf shortDeclName + sizeOf declName + sizeOf levelNames + sizeOf binderIds + sizeOf numParams + sizeOf type
-- Mathlib.Topology.UnitInterval
/-- The unit interval `[0,1]` in ℝ.  -/
unitInterval : Set ℝ
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `LinearEquivClass F R M M₂` asserts `F` is a type of bundled `R`-linear equivs `M → M₂`.
This is an abbreviation for `SemilinearEquivClass F (RingHom.id R) M M₂`.
 -/
LinearEquivClass : (F : Type u_14) →
  (R : outParam (Type u_15)) →
    (M : outParam (Type u_16)) →
      (M₂ : outParam (Type u_17)) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [EquivLike F M M₂] → Prop
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_quotient_succ_le_of_nonZeroDivisor : ∀ {R : Type u_1} [inst : CommRing R] {r : R},
  r ∈ nonZeroDivisors R → ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R
-- Mathlib.Topology.Sion
/-- The set of parameters `z` in the segment `[y, y']` such that `f b z ≤ f b' y`.  -/
_private.Mathlib.Topology.Sion.0.Sion.setOfPred_sublevelLeft_subset : {E : Type u_1} →
  {F : Type u_2} →
    {β : Type u_3} →
      [LinearOrder β] →
        Set E →
          (Y : Set F) →
            (E → F → β) →
              [inst : AddCommGroup F] → [inst_1 : Module ℝ F] → β → β → (y y' : ↑Y) → Set ↑(segment ℝ ↑y ↑y')
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelOpUnop_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.cokernelOpUnop f).inv =
    (CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯).unop
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates an `OfNat.ofNat` literal.
`@OfNat.ofNat _ n _` ~> `n`.
 -/
Lean.PrettyPrinter.Delaborator.delabOfNat : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.GradedAlgebra.RingHom
DirectSum.decompose_map : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : DecidableEq ι] [inst_5 : AddMonoid ι]
  [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] {F : Type u_10} [inst_10 : FunLike F A B] [inst_11 : GradedFunLike F 𝒜 ℬ]
  [inst_12 : RingHomClass F A B] (f : F) {x : A},
  (DirectSum.decompose ℬ) (f x) = (DirectSum.map (↑f).gradedAddHom) ((DirectSum.decompose 𝒜) x)
-- Mathlib.Analysis.Convex.Function
/-- A strictly concave function on an open segment is strictly lower-bounded by the min of its
endpoints.  -/
StrictConcaveOn.lt_on_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → x ≠ y → z ∈ openSegment 𝕜 x y → min (f x) (f y) < f z
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → IntCast (SlashInvariantForm Γ 0)
-- Init.Data.Option.Attach
Option.attachWith_eq_some_iff : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), o = some a → p a) {x : { x // p x }},
  o.attachWith p H = some x ↔ o = some ↑x
-- Init.Tactics
/-- `fail msg` is a tactic that always fails, and produces an error using the given message.  -/
Lean.Parser.Tactic.fail : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_coe_finset : ∀ {X : Type u_2} [inst : EMetricSpace X] (s : Finset X), dimH ↑s = 0
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.sizeOf_eq : ∀ (i : ByteArray.Iterator), sizeOf i = i.array.size - i.idx
-- Mathlib.Order.WithBot
WithBot.unbotD_eq_self_iff : ∀ {α : Type u_1} {d : α} {x : WithBot α}, WithBot.unbotD d x = d ↔ x = ↑d ∨ x = ⊥
-- Mathlib.Order.Partition.Equipartition
Finpartition.top_isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) [inst_1 : Decidable (s = ∅)], ⊤.IsEquipartition
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of the identity in a topological monoid, as a submonoid.  -/
Submonoid.pathComponentOne : (M : Type u_4) → [inst : Monoid M] → [inst_1 : TopologicalSpace M] → [ContinuousMul M] → Submonoid M
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.cospanUnop_inv_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).inv.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)).inv
-- Mathlib.Algebra.Ring.Ext
Distrib.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : Distrib R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get! (t₁ ∩ t₂) k = default
-- 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 α] {f : α → β → Bool} {k : α},
  (Std.HashMap.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.intCast.inj : ∀ {k k_1 : ℤ}, Lean.Grind.CommRing.Expr.intCast k = Lean.Grind.CommRing.Expr.intCast k_1 → k = k_1
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.instIsRightDerivedFunctorLiftInvFac : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (hF : W.IsInvertedBy F),
  (CategoryTheory.Localization.lift F hF L).IsRightDerivedFunctor (CategoryTheory.Localization.fac F hF L).inv W
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
/-- The action on a subalgebra corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Subalgebra.pointwiseMulAction : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {R' : Type u_3} →
            [inst_3 : Semiring R'] →
              [inst_4 : MulSemiringAction R' A] → [SMulCommClass R' R A] → MulAction R' (Subalgebra R A)
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.isClassicalTriangulatedGenerator_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.IsClassicalTriangulatedGenerator ↔ P.triangEnvelope = ⊤
-- Mathlib.Algebra.Group.Nat.Even
/-- `IsSquare` can be decided on `ℕ` by checking against the square root.  -/
Nat.instDecidablePredIsSquare : DecidablePred IsSquare
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.memLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [SecondCountableTopologyEither α E]
  [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] [Fact (1 ≤ p)] (𝕜' : Type u_5) [inst_7 : NormedField 𝕜']
  [NormedSpace 𝕜' E] (f : C(α, E)), MeasureTheory.MemLp (⇑f) p μ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
ContinuousLinearMap.cont : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂] (self : M →SL[σ] M₂),
  Continuous (↑self).toFun
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.prod : ∀ {R : Type u_1} (M : Type u_2) (N : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FinitePresentation R M] [Module.FinitePresentation R N],
  Module.FinitePresentation R (M × N)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a semiring `R` is a subset `s` that is both a multiplicative and an additive
submonoid.  -/
Subsemiring : (R : Type u) → [NonAssocSemiring R] → Type u
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.contains.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.contains k t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => false
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.contains k l
      | Ordering.gt => Std.DTreeMap.Internal.Impl.contains k r
      | Ordering.eq => true
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ`-valued variance of the real-valued random variable `X` according to the measure `μ`.

It is set to `0` if `X` has infinite variance.  -/
ProbabilityTheory.«termVar[_;_]» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc_w : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc_w._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc_w._auto_3),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).d pq pq')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀
            n₁ n₂ hn₁' ⋯ ⋯).hom
        (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)) =
    0