mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.induct_unfolding : ∀ (motive : ℕ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering → Prop),
  (∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), motive 0 m₁ m₂ (m₁.revlexWF m₂)) →
    (∀ (fuel : ℕ), motive fuel.succ Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit Ordering.eq) →
      (∀ (fuel : ℕ) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          motive fuel.succ Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m) Ordering.gt) →
        (∀ (fuel : ℕ) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
            motive fuel.succ (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit Ordering.lt) →
          (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
              (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon),
              (pw₁.x == pw₂.x) = true →
                motive fuel m₁ m₂ (Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂) →
                  motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                    ((Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂).then
                      (Lean.Grind.CommRing.powerRevlex pw₁.k pw₂.k))) →
            (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
                (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon),
                (pw₁.x == pw₂.x) = false →
                  Nat.blt pw₁.x pw₂.x = true →
                    motive fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                        (Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
                      motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                        ((Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)).then
                          Ordering.lt)) →
              (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
                  (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon),
                  (pw₁.x == pw₂.x) = false →
                    Nat.blt pw₁.x pw₂.x = false →
                      motive fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂
                          (Lean.Grind.CommRing.Mon.revlexFuel fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂) →
                        motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                          ((Lean.Grind.CommRing.Mon.revlexFuel fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂).then
                            Ordering.gt)) →
                ∀ (fuel : ℕ) (m₁ m₂ : Lean.Grind.CommRing.Mon),
                  motive fuel m₁ m₂ (Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂)
-- Mathlib.Order.WellFoundedSet
Finset.isPWO_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (s : Finset ι) {f : ι → Set α},
  (s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO
-- Std.Data.Iterators.Lemmas.Producers.Repeat
_private.Std.Data.Iterators.Lemmas.Producers.Repeat.0.Nat.repeat.match_1.splitter : {α : Type u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((n : ℕ) → (a : α) → motive n.succ a) → motive x x_1
-- Batteries.Lean.NameMapAttribute
/-- Look up a value in the given extension in the environment.  -/
Lean.NameMapExtension.find? : {α : Type} → Lean.NameMapExtension α → Lean.Environment → Lean.Name → Option α
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_range_eq_span_range_support : ∀ {α : Type u} [inst : Semiring α] {ι : Type u_1} (x : ι → α),
  Ideal.span (Set.range x) = Ideal.span (Set.range fun i => x ↑i)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHomClass.eq_1 : ∀ (F : Type u_8) (M : Type u_9) (X : Type u_10) (Y : Type u_11) [inst : SMul M X] [inst_1 : SMul M Y]
  [inst_2 : FunLike F X Y], MulActionHomClass F M X Y = MulActionSemiHomClass F id X Y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constInsertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ (l : List (α × β)),
        m₁.Equiv m₂ → (Std.DHashMap.Raw.Const.insertMany m₁ l).Equiv (Std.DHashMap.Raw.Const.insertMany m₂ l)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filterM : ∀ {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.filterM f it) =
    Std.Iter.foldM
      (fun d b => do
        let __do_lift ← liftM (f b)
        if __do_lift.down = true then g d b else pure d)
      init it
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (α : G ≅ H) (K : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor B E} (h : (F.comp H).comp K ≅ Z),
  CategoryTheory.Functor.isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ h =
    F.associator G K ≪≫ F.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight α K) ≪≫ (F.associator H K).symm ≪≫ h
-- Mathlib.Algebra.Homology.DifferentialObject
/-- The functor from homological complexes to differential graded objects.
 -/
HomologicalComplex.homologicalComplexToDGO : {β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            CategoryTheory.Functor (HomologicalComplex V (ComplexShape.up' b))
              (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.containerName? : Lean.Lsp.SymbolInformation → Option String
-- Mathlib.Data.Fin.Tuple.Basic
/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality.  -/
Fin.insertNthEquiv_last : ∀ (n : ℕ) (α : Type u_3), Fin.insertNthEquiv (fun x => α) (Fin.last n) = Fin.snocEquiv fun x => α
-- Mathlib.Data.Int.Init
Int.inductionOn'_add_one : ∀ {motive : ℤ → Sort u_1} {z b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)}
  {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} (hz : b ≤ z),
  Int.inductionOn' (z + 1) b zero succ pred = succ z hz (Int.inductionOn' z b zero succ pred)
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_deterministic' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β}
  (hg : Measurable g),
  MeasureTheory.StronglyMeasurable f → ∫ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The comultiplication morphism of a comonoid object.  -/
CategoryTheory.ComonObj.comul : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.ComonObj X] → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.e : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Limits.MonoFactorisation f) → X ⟶ self.I
-- Init.Data.List.MinMax
List.min_singleton : ∀ {α : Type u_1} [inst : Min α] {x : α}, [x].min ⋯ = x
-- Mathlib.Data.Multiset.Bind
Multiset.zero_product : ∀ {α : Type u_1} {β : Type v} (t : Multiset β), 0 ×ˢ t = 0
-- Mathlib.Analysis.Convex.Cone.Closure
PointedCone.mem_closure : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] {E : Type u_2}
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : ContinuousAdd E] [inst_6 : Module 𝕜 E]
  [inst_7 : ContinuousConstSMul 𝕜 E] {K : PointedCone 𝕜 E} {a : E}, a ∈ K.closure ↔ a ∈ closure ↑K
-- Mathlib.Logic.Encodable.Basic
Directed.le_sequence : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] [inst_2 : Preorder β] {f : α → β}
  (hf : Directed (fun x1 x2 => x1 ≤ x2) f) (a : α), f a ≤ f (Directed.sequence f hf (Encodable.encode a + 1))
-- Batteries.Data.List.Basic
List.tailsTR.go.eq_def : ∀ {α : Type u_1} (l : List α) (acc : Array (List α)),
  List.tailsTR.go l acc =
    match l with
    | [] => acc.toListAppend [[]]
    | head :: xs => List.tailsTR.go xs (acc.push l)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.mk : {R : Type u} →
  [inst : CommRing R] →
    (carrier : Type v) → [instRing : Ring carrier] → [instBialgebra : Bialgebra R carrier] → BialgCat R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_maxD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.trans_wSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SOppSide x y → s.WSameSide y z → s.WOppSide x z
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] (g : SupBotHom β γ) (f : SupBotHom α β),
  SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)
-- Mathlib.NumberTheory.Divisors
Nat.mem_divisors_self : ∀ (n : ℕ), n ≠ 0 → n ∈ n.divisors
-- Mathlib.RingTheory.PowerSeries.Exp
/-- Shows that $(e^{X})^k = e^{kX}$.  -/
PowerSeries.exp_pow_eq_rescale_exp : ∀ {A : Type u_4} [inst : CommRing A] [inst_1 : Algebra ℚ A] (k : ℕ),
  PowerSeries.exp A ^ k = (PowerSeries.rescale ↑k) (PowerSeries.exp A)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.eq_symm_comp : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : α → M) (g : α → N), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- A `P`-cover of a scheme `X` over `S` is a cover, where the components are over `S` and the
component maps commute with the structure morphisms.  -/
AlgebraicGeometry.Scheme.Cover.Over : (S : AlgebraicGeometry.Scheme) →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    [P.IsStableUnderBaseChange] →
      [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X : AlgebraicGeometry.Scheme} →
          [X.Over S] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X → Type (max u u_1)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.preimage_image_mk : ∀ {α : Type u_1} [inst : Group α] (N : Subgroup α) (s : Set α),
  QuotientGroup.mk ⁻¹' QuotientGroup.mk '' s = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.exact : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R} {t s : ↥(ValuativeRel.posSubmonoid R)},
  ValuativeRel.ValueGroupWithZero.mk x t = ValuativeRel.ValueGroupWithZero.mk y s → x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s
-- Std.Data.DTreeMap.Internal.Model
Ordering.swap.eq_3 : Ordering.gt.swap = Ordering.lt