mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isMinFilter_dual_iff`. -/
IsMaxFilter.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsMinFilter (⇑OrderDual.toDual ∘ f) l a
-- Mathlib.Data.PFun
PFun.asSubtype_eq_of_mem : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β}, y ∈ f x → ∀ (domx : x ∈ f.Dom), f.asSubtype ⟨x, domx⟩ = y
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
/-- The spectral object with values in `(HomotopyCategory C (.up ℤ)` that
is indexed by `CochainComplex C ℤ`.  -/
HomotopyCategory.spectralObjectMappingCone : (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.Limits.HasBinaryBiproducts C] →
          CategoryTheory.Triangulated.SpectralObject (HomotopyCategory C (ComplexShape.up ℤ)) (CochainComplex C ℤ)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₄ : UInt8 → UInt8 → UInt8 → UInt8 → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instAlgebra : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → Algebra R W'.CoordinateRing
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal_rightUnitor : ∀ (M : Type u) [inst : Monoid M] (X : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {L : Filter (𝕜 × 𝕜)} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F}
  {g₁' : F} {L' : Filter (𝕜' × 𝕜')},
  HasDerivAtFilter g₁ g₁' L' →
    HasDerivAtFilter h h' L → Filter.Tendsto (Prod.map h h) L L' → HasDerivAtFilter (g₁ ∘ h) (h' • g₁') L
-- Std.Do.SPred.Laws
Std.Do.SPred.pure_elim' : ∀ {σs : List (Type u)} {φ : Prop} {P : Std.Do.SPred σs}, (φ → ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P
-- Mathlib.Order.Defs.LinearOrder
_private.Mathlib.Order.Defs.LinearOrder.0.Ordering.Compares.match_1.splitter : {α : Type u_2} →
  (motive : Ordering → α → α → Sort u_1) →
    (x : Ordering) →
      (x_1 x_2 : α) →
        ((a b : α) → motive Ordering.lt a b) →
          ((a b : α) → motive Ordering.eq a b) → ((a b : α) → motive Ordering.gt a b) → motive x x_1 x_2
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_def : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R), v.restrict x = (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapComp_inv : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Under.mapComp f g).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare),
  S.shortComplex.X₁ =
    (CategoryTheory.presheafToSheaf J AddCommGrpCat).obj ((CategoryTheory.yoneda.obj S.X₁).comp AddCommGrpCat.free)
-- Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
/-- A C⋆-algebra is spanned by nonnegative strict contractions.  -/
CStarAlgebra.span_nonneg_inter_unitBall : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Submodule.span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 1) = ⊤
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.lt_rank_iff : ∀ {x : ZFSet.{u}} {o : Ordinal.{u}}, o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_of_not_prime : ∀ (n p : ℕ), ¬Nat.Prime p → p ^ n.factorization p = 1
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One γ] (f : α → β), Function.extend f 1 1 = 1
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The range of `spectralValue_terms p` is a finite set.  -/
spectralValueTerms_finite_range : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R), (Set.range (spectralValueTerms p)).Finite
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.fold.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_1 ()
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.dfinsuppSumAddHom : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : Mul M]
  [inst_3 : (i : ι) → AddCommMonoid (β i)] (c : RingCon M) (h h' : (i : ι) → β i →+ M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))) → c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)
-- Mathlib.Analysis.MellinInversion
/-- The inverse Mellin transform of the Mellin transform applied to `x > 0` is x.  -/
mellinInv_mellin_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] (σ : ℝ) (f : ℝ → E) {x : ℝ},
  0 < x →
    MellinConvergent f ↑σ →
      Complex.VerticalIntegrable (mellin f) σ MeasureTheory.volume → ContinuousAt f x → mellinInv σ (mellin f) x = f x
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.ext_iff : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {x y : ChartedSpace H M},
  x = y ↔ ChartedSpace.atlas = ChartedSpace.atlas ∧ ChartedSpace.chartAt = ChartedSpace.chartAt
-- Mathlib.NumberTheory.Dioph
/-- A version of **Matiyasevic's theorem**  -/
Dioph.pow_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v ^ g v
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.decomposeAux_coe : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : CommSemiring R] (f : M →+ ι) {i : ι} (x : ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)),
  (AddMonoidAlgebra.decomposeAux f) ↑x = (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) i) x
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.find?_prop_eq_find?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String}, s.find? p = s.find? fun x => decide (p x)
-- Mathlib.Order.Cover
Set.covBy_insert : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s ⋖ insert a s
-- Init.Data.Array.Lemmas
Array.foldl.eq_1 : ∀ {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start stop : ℕ),
  Array.foldl f init as start stop = (Array.foldlM (fun x1 x2 => pure (f x1 x2)) init as start stop).run
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsOpen.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  IsOpen s → MeasurableSet s
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.mkQ)
      (ModuleCat.cokernelIsoRangeQuotient f).inv =
    CategoryTheory.Limits.cokernel.π f
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
ContinuousMapZero.aeStronglyMeasurable_mkD_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [CompactSpace Y] [inst_4 : Zero Y] [inst_5 : TopologicalSpace X]
  [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)] (f : X → Y → E) (g : ContinuousMapZero Y E),
  Continuous (Function.uncurry f) →
    (∀ᵐ (x : X) ∂μ, f x 0 = 0) → MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMapZero.mkD (f x) g) μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter!_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      k ∈ t → (f (t.get? k)).isNone = true → (Std.DTreeMap.Internal.Impl.alter! k f t).size = t.size - 1
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.mem_compPartialSumSource_iff : ∀ (m M N : ℕ) (i : (n : ℕ) × (Fin n → ℕ)),
  i ∈ FormalMultilinearSeries.compPartialSumSource m M N ↔
    (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N
-- Mathlib.GroupTheory.Coxeter.Inversion
/-- The proposition that `t` is a left inversion of `w`; i.e., `t` is a reflection and
$\ell (t w) < \ell(w)$.  -/
CoxeterSystem.IsLeftInversion : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → W → Prop
-- Mathlib.NumberTheory.FLT.Four
Fermat42.not_minimal : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → a % 2 = 1 → 0 < c → False
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeSortType : CoeSort CommGrpCat (Type u)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.symm_target : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y), f.symm.target = f.source
-- Mathlib.Algebra.Quandle
/-- This is the natural rack homomorphism to the conjugation quandle of the group `R ≃ R`
that acts on the rack.  -/
Rack.toConj : (R : Type u_1) → [inst : Rack R] → ShelfHom R (Quandle.Conj (R ≃ R))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.isEmpty = t.isEmpty
-- Lean.Data.Options
Lean.OptionDecl.descr : Lean.OptionDecl → String
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) =
    g
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.trans_eventuallyLE : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g g' : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [inst_2 : PartialOrder β] [IsOrderedRing β] [OrderTopology β],
  0 ≤ᶠ[l] k →
    Asymptotics.SuperpolynomialDecay l k g →
      Asymptotics.SuperpolynomialDecay l k g' → g ≤ᶠ[l] f → f ≤ᶠ[l] g' → Asymptotics.SuperpolynomialDecay l k f
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exists_forall_signedInfDist_eq_iff_eq_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) → ((∃ r, ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r) ↔ p = s.incenter)
-- Mathlib.CategoryTheory.Functor.Flat
/-- (Implementation)
The evaluation of `F.lan` at `X` is the colimit over the costructured arrows over `X`.
 -/
CategoryTheory.lanEvaluationIsoColim : {C D : Type u₁} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.SmallCategory D] →
      (E : Type u₂) →
        [inst_2 : CategoryTheory.Category.{u₁, u₂} E] →
          (F : CategoryTheory.Functor C D) →
            (X : D) →
              [inst_3 : ∀ (X : D), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow F X) E] →
                F.lan.comp ((CategoryTheory.evaluation D E).obj X) ≅
                  ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.CostructuredArrow F X) C E).obj
                        (CategoryTheory.CostructuredArrow.proj F X)).comp
                    CategoryTheory.Limits.colim
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.add_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C} (f g : P ⟶ Q), f + g = { f := f.f + g.f, comm := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v w : P`, we have `f.lift hg z + w = v ↔ g x + w = g y + v`, where `x : M, y ∈ S` are such
that `z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.lift_spec_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N)
  (w v : P), (f.lift hg) z + w = v ↔ g (f.sec z).1 + w = g ↑(f.sec z).2 + v
-- Mathlib.Order.Filter.Basic
Filter.Eventually.forall_mem : ∀ {α : Type u_2} {f : Filter α} {s : Set α} {P : α → Prop},
  (∀ᶠ (x : α) in f, P x) → Filter.principal s ≤ f → ∀ x ∈ s, P x
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_comp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F G H : CategoryTheory.Functor (A ⊕ A') B}
  (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ⟶ (CategoryTheory.Sum.inl_ A A').comp G)
  (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ⟶ (CategoryTheory.Sum.inr_ A A').comp G)
  (ν₁ : (CategoryTheory.Sum.inl_ A A').comp G ⟶ (CategoryTheory.Sum.inl_ A A').comp H)
  (ν₂ : (CategoryTheory.Sum.inr_ A A').comp G ⟶ (CategoryTheory.Sum.inr_ A A').comp H),
  CategoryTheory.Sum.natTransOfWhiskerLeftInlInr (CategoryTheory.CategoryStruct.comp η₁ ν₁)
      (CategoryTheory.CategoryStruct.comp η₂ ν₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Sum.natTransOfWhiskerLeftInlInr η₁ η₂)
      (CategoryTheory.Sum.natTransOfWhiskerLeftInlInr ν₁ ν₂)
-- Mathlib.Topology.WithTopology
WithTopology.toTopology_surjective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Surjective (WithTopology.toTopology t)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- if `f` is integrable, then `fun x ↦ g x + f x` is integrable iff `g` is.
See `integrable_add_iff_integrable_left'` for the same statement with `g + f` instead
of `fun x ↦ g x + f x`.  -/
MeasureTheory.integrable_add_iff_integrable_left' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β},
  MeasureTheory.Integrable f μ → (MeasureTheory.Integrable (fun x => g x + f x) μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.Tactic.ITauto
/-- A variant on `Proof.exfalso'` that performs opportunistic simplification.  -/
Mathlib.Tactic.ITauto.Proof.exfalso : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt g g' s x → HasDerivWithinAt (f - g) (f' - g') s x
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.id d) c =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.central_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {r : R} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar r * a) (a * FreeAlgebra.Pre.ofScalar r)
-- Mathlib.Data.Num.Lemmas
Num.cast_pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] (n : PosNum), ↑(Num.pos n) = ↑n
-- Mathlib.Data.DFinsupp.Lex
/-- `DFinsupp.Lex r s` is the lexicographic relation on `Π₀ i, α i`, where `ι` is ordered by `r`,
and `α i` is ordered by `s i`.

The type synonym `Lex (Π₀ i, α i)` has an order given by `DFinsupp.Lex (· < ·) (· < ·)`, whereas
`Colex (Π₀ i, α i)` has an order given by `DFinsupp.Lex (· > ·) (· < ·)`.
 -/
DFinsupp.Lex : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      (ι → ι → Prop) → ((i : ι) → α i → α i → Prop) → (Π₀ (i : ι), α i) → (Π₀ (i : ι), α i) → Prop
-- Lean.Parser.Tactic
Lean.Parser.Tactic.introMatch.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.Choose
_private.Mathlib.Tactic.Choose.0.Mathlib.Tactic.Choose.parseChooseArg.parseBinderIdent : Lean.TSyntax `Lean.binderIdent → Mathlib.Tactic.Choose.ChooseArg
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp₂_obj_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [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]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {F₀ : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {F₁ : CategoryTheory.Functor D H} (L' : CategoryTheory.Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁),
  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj X).right = X.right
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.univ_pi : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [Countable δ] {t : (i : δ) → Set (X i)},
  (∀ (i : δ), MeasurableSet (t i)) → MeasurableSet (Set.univ.pi t)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, a ∉ m → m[a]! = default
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_hom_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj W
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          (CategoryTheory.CategoryStruct.id Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
              Z).hom
          h))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.max?.isSome = true
-- Mathlib.FieldTheory.Galois.NormalBasis
IsGalois.normalBasis_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : IsGalois K L] (e : Gal(L/K)),
  (IsGalois.normalBasis K L) e = e ((IsGalois.normalBasis K L) 1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map (SSet.N.monoOfLE h)) (SSet.yonedaEquiv.symm y.simplex) =
    SSet.yonedaEquiv.symm x.simplex
-- Mathlib.Order.BooleanAlgebra.Basic
BooleanAlgebra.toGeneralizedBooleanAlgebra : {α : Type u} → [BooleanAlgebra α] → GeneralizedBooleanAlgebra α
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.leftUnitor_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor M₁).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M₁.obj X)).inv
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.liftPropOn_univ : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'},
  ChartedSpace.LiftPropOn P g Set.univ ↔ ChartedSpace.LiftProp P g
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] [IsEmpty ι], ContinuousAlternatingMap.fderivCompContinuousLinearMap = 0
-- Mathlib.Data.Int.Init
Int.inductionOn'.pos.eq_1 : ∀ {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)),
  Int.inductionOn'.pos b zero succ 0 = cast ⋯ zero
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.deterministic_prod_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g),
  (ProbabilityTheory.Kernel.deterministic f hf).prod (ProbabilityTheory.Kernel.deterministic g hg) =
    ProbabilityTheory.Kernel.deterministic (fun a => (f a, g a)) ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{max u u_1, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : groupCohomology.shortComplexH1 C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 (MonoidHom.id G) ψ) h)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  Std.ExtDHashMap.Const.get! (m₁ \ m₂) k = if k ∈ m₂ then default else Std.ExtDHashMap.Const.get! m₁ k