mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Util
/-- Returns `Grind.PreMatchCond e`.
Recall that `Grind.PreMatchCond` is an identity function,
but the simproc `reducePreMatchCond` is used to prevent the term `e` from being simplified.
`Grind.PreMatchCond` is later converted into `Grind.MatchCond`.
See comment at `MatchCond.lean`.
 -/
Lean.Meta.Grind.markAsPreMatchCond : Lean.Expr → Lean.Expr
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_left_iff : ∀ {a b : Cardinal.{u_1}}, a * b = a ↔ max Cardinal.aleph0 b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupMap_apply_coe : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H : Subgroup G)
  (x : ↥H.toSubmonoid), ↑((f.subgroupMap H) x) = f ↑x
-- Mathlib.Algebra.Lie.Quotient
/-- `LieSubmodule.Quotient.mk` as a `LieModuleHom`.  -/
LieSubmodule.Quotient.mk' : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (N : LieSubmodule R L M) → [inst_5 : LieAlgebra R L] → [inst_6 : LieModule R L M] → M →ₗ⁅R,L⁆ M ⧸ N
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_symm_neg : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f : X ⟶ G.obj Y),
  (adj.homEquiv X Y).symm (-f) = -(adj.homEquiv X Y).symm f
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.mk : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        (succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))) →
          (∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
              (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ j hj x) = x) →
            (lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)) →
              (∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
                  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift j hj x) =
                    ↑x (Opposite.op ⟨i, hi⟩)) →
                F.WellOrderInductionData
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_bound : ∀ {x : ℂ},
  ‖x‖ ≤ 1 →
    ∀ {n : ℕ},
      0 < n → ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.differentiableWithinAt_Iio_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ}, ConvexOn ℝ S f → x ∈ interior S → DifferentiableWithinAt ℝ f (Set.Iio x) x
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.mem_iff_eq_image : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y) (a : Function.Fiber f), y ∈ ↑a ↔ f y = Function.Fiber.image f a
-- Mathlib.GroupTheory.Index
AddSubgroup.index_eq_card : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.index = Nat.card (G ⧸ H)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {W : ι → CategoryTheory.MorphismProperty C}
  [∀ (i : ι), (W i).ContainsIdentities], (⨅ i, W i).ContainsIdentities
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.continuous_deriv_one : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, ContDiff 𝕜 1 f → Continuous (deriv f)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- The natural functor from `R`-coalgebras to comonoid objects in the category of `R`-modules.  -/
CoalgCat.toComon : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (CoalgCat R) (CategoryTheory.Comon (ModuleCat R))
-- Mathlib.Algebra.Homology.TotalComplex
/-- The vertical differential in the total complex on a given summand.  -/
HomologicalComplex₂.d₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁ : I₁) →
                            (i₂ : I₂) → (i₁₂ : I₁₂) → (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂
-- Mathlib.Topology.Homeomorph.Lemmas
Fin.appendHomeomorph_toEquiv : ∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ), (Fin.appendHomeomorph m n).toEquiv = Fin.appendEquiv m n
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.widget.sizeOf_spec : ∀ (wi : Lean.Widget.WidgetInstance) (alt : Std.Format),
  sizeOf (Lean.Widget.EmbedFmt.widget✝ wi alt) = 1 + sizeOf wi + sizeOf alt
-- Init.Tactics
/-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations.  -/
Lean.Parser.Tactic.eqRefl : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mem_or_subset : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → x ∈ y ∨ y ⊆ x
-- Init.Data.Array.Lemmas
Array.size_modify : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {f : α → α}, (xs.modify i f).size = xs.size
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddCommMonCatIso_hom : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (e : X ≃+ Y),
  e.toAddCommMonCatIso.hom = AddCommMonCat.ofHom e.toAddMonoidHom
-- Mathlib.Algebra.Order.Floor.Defs
FloorSemiring.instCharZero : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [FloorSemiring α], CharZero α
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntryIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l) = k
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∃ s, Submodule.span R ↑s = ⊤ ∧ (Finsupp.linearCombination R Subtype.val).ker.FG) → Module.FinitePresentation R M
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAddGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → AddGroup (ZeroAtInftyContinuousMap α β)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ofPiFork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left}
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L),
  (CategoryTheory.Limits.Multifork.ofPiFork a).ι i = CategoryTheory.CategoryStruct.comp a.ι (c.proj i)
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`.  -/
AntitoneOn : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Set α → Prop
-- Mathlib.Topology.Separation.Basic
R1Space.iInf : ∀ {ι : Type u_3} {X : Type u_4} {t : ι → TopologicalSpace X}, (∀ (i : ι), R1Space X) → R1Space X
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.exact_iff_of_hasForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology],
  S.Exact ↔
    ∀ (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)),
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.f)) x₁ = x₂
-- Mathlib.Algebra.Central.Defs
Algebra.IsCentral.out : ∀ {K : Type u} {inst : CommSemiring K} {D : Type v} {inst_1 : Semiring D} {inst_2 : Algebra K D}
  [self : Algebra.IsCentral K D], Subalgebra.center K D ≤ ⊥
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorHom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.δ_lift_assoc : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [inst : HomotopicalAlgebra.Fibration p]
  (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y)
  (comm :
    ∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b)
  (j : Fin (n + 2)) (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_lift._auto_1) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp (hf.lift p b comm) h) =
    CategoryTheory.CategoryStruct.comp (f j hj) h
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
/-- The nontrivial implication of Kaplansky's criterion: an integral domain is a UFD if every
nonzero prime ideal contains a prime element.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.of_exists_prime_mem_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R],
  (∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_1 : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_3 =>
      h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) =
    h_1 size k v l x
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundancyIndex_le_of_dvd : ∀ {n m : ℕ}, n ≠ 0 → m ∣ n → m.abundancyIndex ≤ n.abundancyIndex
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instSMul : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    {R : Type u_2} →
      [inst_1 : SMul R NNReal] →
        [inst_2 : SMul R ENNReal] →
          [IsScalarTower R NNReal ENNReal] → [IsScalarTower R ENNReal ENNReal] → SMul R (MeasureTheory.FiniteMeasure Ω)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.minKey ⋯) k).isLE = true
-- Lean.Server.GoTo
Lean.Server.GoToContext.mk : Lean.Server.DocumentMeta →
  Lean.Server.GoToKind →
    Option Lean.Elab.InfoTree →
      Option Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Server.GoToContext
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W.map f).polynomialY = Polynomial.map (Polynomial.mapRingHom f) W.polynomialY
-- Mathlib.Algebra.Group.End
MulAut.coe_inv : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M), ⇑e⁻¹ = ⇑(MulEquiv.symm e)
-- Init.Data.List.Scan.Lemmas
List.scanl_ne_nil : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β}, List.scanl f b l ≠ []
-- Init.Data.List.Sort.Lemmas
List.cons_merge_cons : ∀ {α : Type u_1} (s : α → α → Bool) (a b : α) (l r : List α),
  (a :: l).merge (b :: r) s = if s a b = true then a :: l.merge (b :: r) s else b :: (a :: l).merge r s
-- Mathlib.Order.Filter.Finite
Filter.EventuallyLE.iUnion : ∀ {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋃ i, s i ≤ᶠ[l] ⋃ i, t i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  m.WF → ((Std.DHashMap.Raw.filterMap f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = none)
-- Lean.Meta.Basic
Lean.Meta.Cache.mk.inj : ∀ {inferType : Lean.Meta.InferTypeCache} {funInfo : Lean.Meta.FunInfoCache}
  {synthInstance : Lean.Meta.SynthInstanceCache} {whnf : Lean.Meta.WhnfCache}
  {defEqTrans defEqPerm : Lean.Meta.DefEqCache} {inferType_1 : Lean.Meta.InferTypeCache}
  {funInfo_1 : Lean.Meta.FunInfoCache} {synthInstance_1 : Lean.Meta.SynthInstanceCache} {whnf_1 : Lean.Meta.WhnfCache}
  {defEqTrans_1 defEqPerm_1 : Lean.Meta.DefEqCache},
  { inferType := inferType, funInfo := funInfo, synthInstance := synthInstance, whnf := whnf, defEqTrans := defEqTrans,
        defEqPerm := defEqPerm } =
      { inferType := inferType_1, funInfo := funInfo_1, synthInstance := synthInstance_1, whnf := whnf_1,
        defEqTrans := defEqTrans_1, defEqPerm := defEqPerm_1 } →
    inferType = inferType_1 ∧
      funInfo = funInfo_1 ∧
        synthInstance = synthInstance_1 ∧ whnf = whnf_1 ∧ defEqTrans = defEqTrans_1 ∧ defEqPerm = defEqPerm_1
-- Mathlib.Data.Fin.SuccPred
Fin.ne_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p ≠ p.succAbove i
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A "diagonal" morphism from the right object of `u` to the left object of `v`.  -/
CategoryTheory.Arrow.RightHomotopy.hom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → {f g : u ⟶ v} → CategoryTheory.Arrow.RightHomotopy f g → (u.right ⟶ v.left)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom.congr_simp : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a a_1 : σ → MvPowerSeries τ S} (e_a : a = a_1) (ha : MvPowerSeries.HasSubst a),
  MvPowerSeries.substAlgHom ha = MvPowerSeries.substAlgHom ⋯
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.lt₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (self : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y),
  W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → self.deg Y < self.deg X
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The key that is used for sorting and deduplicating `rw` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.RwKey : Type
-- Mathlib.Order.RelSeries
/-- The underlying function of a relation series  -/
RelSeries.toFun : {α : Type u_1} → {r : SetRel α α} → (self : RelSeries r) → Fin (self.length + 1) → α
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_zero_eval_zero : ∀ (R : Type u) [inst : Ring R], Polynomial.eval 0 (descPochhammer R 0) = 1
-- Mathlib.Order.Heyting.Basic
lt_hnot_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α} [Nontrivial α], ￢a < a ↔ a = ⊤
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The key lemma: the sequence of integrals `I` can be written as a linear combination of `sin` and
`cos`, with coefficients given by the polynomials `sinPoly` and `cosPoly`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly_add_cosPoly_eval : ∀ (θ : ℝ) (n : ℕ),
  I✝ n θ * θ ^ (2 * n + 1) =
    ↑n.factorial *
      (Polynomial.eval₂ (Int.castRingHom ℝ) θ (sinPoly✝ n) * Real.sin θ +
        Polynomial.eval₂ (Int.castRingHom ℝ) θ (cosPoly✝ n) * Real.cos θ)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The submodule `genEigenspace f μ k` for a linear map `f`, a scalar `μ`,
and a number `k : ℕ∞` is the kernel of `(f - μ • id) ^ k` if `k` is a natural number,
or the union of all these kernels if `k = ∞`. (`k = ∞` corresponds to Def 8.19 of [axler2024].)
A generalized eigenspace for some exponent `k` is contained in
the generalized eigenspace for exponents larger than `k`.  -/
Module.End.genEigenspace : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ∞ →o Submodule R M
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- Alternative constructor for `W.IsMonoidal` given that `W` is multiplicative and stable under
tensoring morphisms.  -/
CategoryTheory.MorphismProperty.IsMonoidal.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [W.IsMultiplicative],
  (∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂),
      W f → W g → W (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) →
    W.IsMonoidal
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRev (fun d a x => f d a) init ↑m = Array.foldr (fun a b => f b a) init (↑m).keysArray
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addETransformLeft e x = (x.1 ∩ (AddOpposite.op e +ᵥ x.1), x.2 ∪ (-e +ᵥ x.2))
-- Mathlib.Order.Lattice
Pi.instMinForall_mathlib : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → Min (α' i)] → Min ((i : ι) → α' i)
-- Mathlib.RingTheory.RingInvo
RingInvo.mk.injEq : ∀ {R : Type u_2} [inst : Semiring R] (toRingEquiv : R ≃+* Rᵐᵒᵖ)
  (involution' : ∀ (x : R), MulOpposite.unop (toRingEquiv.toFun (MulOpposite.unop (toRingEquiv.toFun x))) = x)
  (toRingEquiv_1 : R ≃+* Rᵐᵒᵖ)
  (involution'_1 : ∀ (x : R), MulOpposite.unop (toRingEquiv_1.toFun (MulOpposite.unop (toRingEquiv_1.toFun x))) = x),
  ({ toRingEquiv := toRingEquiv, involution' := involution' } =
      { toRingEquiv := toRingEquiv_1, involution' := involution'_1 }) =
    (toRingEquiv = toRingEquiv_1)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.DiscrInfo.mk.sizeOf_spec : ∀ (hName? : Option Lean.Name), sizeOf { hName? := hName? } = 1 + sizeOf hName?
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.summable_nat_add : ∀ (f : ℕ → NNReal), Summable f → ∀ (k : ℕ), Summable fun i => f (i + k)
-- Mathlib.Order.Filter.Map
Filter.biSup_pure_eq_principal : ∀ {α : Type u_1} (s : Set α), ⨆ a ∈ s, pure a = Filter.principal s
-- Init.Core
/-- The **quotient axiom**, which asserts the equality of elements related in the setoid.

Because `Quotient` is built on a lower-level type `Quot`, `Quotient.sound` is implemented as a
theorem. It is derived from `Quot.sound`, the soundness axiom for the lower-level quotient type
`Quot`.
 -/
Quotient.sound : ∀ {α : Sort u} {s : Setoid α} {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_mem_vadd_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s : Finset β}
  {b : β} (a : α), a +ᵥ b ∈ a +ᵥ s ↔ b ∈ s
-- Init.Prelude
/-- `False.elim : False → C` says that from `False`, any desired proposition
`C` holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.

The target type is actually `C : Sort u` which means it works for both
propositions and types. When executed, this acts like an "unreachable"
instruction: it is **undefined behavior** to run, but it will probably print
"unreachable code". (You would need to construct a proof of false to run it
anyway, which you can only do using `sorry` or unsound axioms.)
 -/
False.elim : {C : Sort u} → False → C
-- Mathlib.GroupTheory.Divisible
/-- An `AddMonoid A` is `α`-divisible iff `n • x = a` has a solution for all `n ≠ 0 ∈ α` and `a ∈ A`.
Here we adopt a constructive approach where we ask an explicit `div : A → α → A` function such that
* `div a 0 = 0` for all `a ∈ A`
* `n • div a n = a` for all `n ≠ 0 ∈ α` and `a ∈ A`.
 -/
DivisibleBy : (A : Type u_1) → (α : Type u_2) → [AddMonoid A] → [SMul α A] → [Zero α] → Type (max u_1 u_2)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.range_coe_principal : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {S : Set ι}, Set.range DFunLike.coe = S.pi A
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none
-- Init.Data.List.MinMaxOn
List.lt_apply_maxOn_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β}, b < f (List.maxOn f xs h) ↔ ∃ x ∈ xs, b < f x