mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.isUnit_toMatrix : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (b₂ : AffineBasis ι k P)
  [inst_5 : DecidableEq ι], IsUnit (b.toMatrix ⇑b₂)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE_eq_getEntryGE : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  {hto : t.Ordered} {he : ∃ a ∈ t, (compare a k).isGE = true},
  Std.DTreeMap.Internal.Impl.getKeyGE k t hto he = (Std.DTreeMap.Internal.Impl.getEntryGE k t hto he).fst
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_ne_coe : ∀ {x y : ℝ}, ↑x ≠ ↑y ↔ x ≠ y
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_subset_iUnion_closedBall_of_lt : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (E : Set α) {δ δ' : ℝ},
  0 < δ' → δ < δ' → Metric.cthickening δ E ⊆ ⋃ x ∈ E, Metric.closedBall x δ'
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PrespectralSpace Y]
  (f : X → Y), Topology.IsClosedEmbedding f → PrespectralSpace X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.RingTheory.Polynomial.Basic
/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`.  -/
Ideal.isPrime_map_C_iff_isPrime : ∀ {R : Type u} [inst : CommRing R] (P : Ideal R), (Ideal.map Polynomial.C P).IsPrime ↔ P.IsPrime
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne.congr_simp : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H H_1 : Subgroup G)
  (e_H : H = H_1) [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H],
  LinearOrderedCommGroup.Subgroup.genLTOne H = LinearOrderedCommGroup.Subgroup.genLTOne H_1
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (A B : Matrix m n α) (x : m → α), Matrix.vecMul x (A + B) = Matrix.vecMul x A + Matrix.vecMul x B
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.conj : ∀ {α : Type u_2} {f g : Equiv.Perm α} {s : Set α}, f.IsCycleOn s → (g * f * g⁻¹).IsCycleOn (⇑g '' s)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] (u : α), G.eccent u ≠ 0
-- Mathlib.Analysis.Seminorm
Seminorm.instMulAction : {R : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_7} →
      [inst : SeminormedRing 𝕜] →
        [inst_1 : AddGroup E] →
          [inst_2 : SMul 𝕜 E] →
            [inst_3 : Monoid R] →
              [inst_4 : MulAction R ℝ] →
                [inst_5 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → MulAction R (Seminorm 𝕜 E)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivRight_apply : ∀ {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x // p x }), (Equiv.subtypeEquivRight e) z = ⟨↑z, ⋯⟩
-- Init.Data.Array.Perm
Array.Perm.pairwise_iff : ∀ {α : Type u_1} {R : α → α → Prop},
  (∀ {x y : α}, R x y → R y x) →
    ∀ {xs ys : Array α}, xs.Perm ys → (List.Pairwise R xs.toList ↔ List.Pairwise R ys.toList)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Q W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (hP.desc h k w)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q h) h_1
-- Init.Data.List.Attach
List.unattach_nil : ∀ {α : Type u_1} {p : α → Prop}, [].unattach = []
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.nonzero_mem_of_bot_lt : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, ⊥ < p → ∃ a, a ≠ 0
-- Mathlib.Order.Lattice
/-- A type endowed with `⊔` and `⊓` is a `DistribLattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `DistribLattice`.
See note [reducible non-instances].  -/
Function.Injective.distribLattice : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : DistribLattice β] →
              (f : α → β) →
                Function.Injective f →
                  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                    (∀ {x y : α}, f x < f y ↔ x < y) →
                      (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) → (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → DistribLattice α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
AddSubmonoidWithOneClass.toAddSubmonoidClass : ∀ {S : Type u_1} {R : outParam (Type u_2)} {inst : AddMonoidWithOne R} {inst_1 : SetLike S R}
  [self : AddSubmonoidWithOneClass S R], AddSubmonoidClass S R
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.differentiableAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {x : E},
  f₀ =ᶠ[nhds x] f₁ → (DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.post_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.post L R F).obj X).right = X.right
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_top_piecewise : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f g : α → ε) [inst_2 : DecidablePred fun x => x ∈ s],
  MeasurableSet s →
    MeasureTheory.eLpNorm (s.piecewise f g) ⊤ μ =
      max (MeasureTheory.eLpNorm f ⊤ (μ.restrict s)) (MeasureTheory.eLpNorm g ⊤ (μ.restrict sᶜ))
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_zero : ∀ {n : ℕ}, (finSuccEquiv n) 0 = none
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforward_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X),
  (CategoryTheory.PreZeroHypercover.pushforward f E).I₀ = E.I₀
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ.IsThreeCycle = (σ.cycleType = {3})
-- Init.Data.SInt.Lemmas
Int8.add_eq_left : ∀ {a b : Int8}, a + b = a ↔ b = 0