mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.CharP.isNat_pow : ∀ {α : Type u_1} [inst : Semiring α] {f : α → ℕ → α} {a : α} {a' b b' c n n' : ℕ},
  CharP α n →
    f = HPow.hPow →
      Mathlib.Meta.NormNum.IsNat a a' →
        Mathlib.Meta.NormNum.IsNat b b' →
          Mathlib.Meta.NormNum.IsNat n n' → (a'.pow b').mod n' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_vert_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} [CategoryTheory.IsIso snd] [CategoryTheory.IsIso f],
  CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_pair : ∀ {x y z : PSet.{u_1}}, x ∈ {y, z} ↔ x.Equiv y ∨ x.Equiv z
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_normalizer_iff' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {g : G},
  g ∈ Subgroup.normalizer ↑H ↔ ∀ (n : G), n * g ∈ H ↔ g * n ∈ H
-- Mathlib.Algebra.Order.Hom.Basic
/-- `NonarchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms.  -/
NonarchimedeanHomClass : (F : Type u_7) →
  (α : outParam (Type u_8)) → (β : outParam (Type u_9)) → [Add α] → [LinearOrder β] → [FunLike F α β] → Prop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.skipSuffix? pat = Option.map String.Pos.toSlice (s.skipSuffix? pat)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a : α), Finset.Icc a a = {a}
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_ofMul_eq_orderOf : ∀ {G : Type u_1} [inst : Monoid G] (x : G), addOrderOf (Additive.ofMul x) = orderOf x
-- Mathlib.Data.PNat.Factors
instOrderedSubPrimeMultiset : OrderedSub PrimeMultiset
-- Mathlib.Data.Vector.Basic
/-- If `a : α` and `l : Vector α n`, then `cons a l`, is the vector of length `n + 1`
whose first element is a and with l as the rest of the list.  -/
List.Vector.«term_::ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_id : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G],
  ContinuousLinearMap.rTensor G (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 (TensorProduct 𝕜 E G)
-- Batteries.Data.AssocList
Batteries.AssocList.any.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.any p (Batteries.AssocList.cons a b es) = (p a b || Batteries.AssocList.any p es)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Antitone fun n => f n x) →
      ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
          Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype.eq_1 : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p],
  Equiv.Perm.ofSubtype = { toFun := fun f => f.extendDomain (Equiv.refl (Subtype p)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (e' : N → M)
  (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : M),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e
-- Mathlib.RingTheory.Nilpotent.Lemmas
LinearMap.isNilpotent_mulLeft_iff : ∀ (R : Type u_1) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  IsNilpotent (LinearMap.mulLeft R a) ↔ IsNilpotent a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.d_def : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  (groupHomology.inhomogeneousChains A).d (n + 1) n = groupHomology.inhomogeneousChains.d A n
-- Mathlib.Analysis.Normed.Ring.Units
/-- In a normed ring with summable geometric series, a perturbation of a unit `x` by an
element `t` of distance less than `‖x⁻¹‖⁻¹` from `x` is a unit.
Here we construct its `Units` structure.  -/
Units.add : {R : Type u_1} → [inst : NormedRing R] → [HasSummableGeomSeries R] → (x : Rˣ) → (t : R) → ‖t‖ < ‖↑x⁻¹‖⁻¹ → Rˣ
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec_recOn' : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
  Primrec c →
    ∀ {z : α → σ},
      Primrec z →
        ∀ {s : α → σ},
          Primrec s →
            ∀ {l : α → σ},
              Primrec l →
                ∀ {r : α → σ},
                  Primrec r →
                    ∀ {pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                      Primrec₂ pr →
                        ∀ {co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                          Primrec₂ co →
                            ∀ {pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                              Primrec₂ pc →
                                ∀ {rf : α → Nat.Partrec.Code × σ → σ},
                                  Primrec₂ rf →
                                    have PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
                                    have CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
                                    have PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
                                    have RF := fun a cf hf => rf a (cf, hf);
                                    have F := fun a c =>
                                      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
                                    Primrec fun a => F a (c a)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.false : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  {map : Std.HashMap α ℕ},
  Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map →
    ∀ (hlt : idx < decls.size),
      decls[idx] = Std.Sat.AIG.Decl.false → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSimpleRing.isIsotypic : ∀ (R : Type u) [inst : Ring R] [IsSimpleRing R] [IsArtinianRing R] (M : Type u_2) [inst_3 : AddCommGroup M]
  [inst_4 : Module R M], IsIsotypic R M
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.op_l : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l : sq.LiftStruct), l.op.l = l.l.op
-- Mathlib.Order.Hom.Order
OrderHom.orderTop : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [OrderTop β] → OrderTop (α →o β)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.fixedTermElabs : Lean.Elab.Term.SavedContext → Array Lean.Elab.Term.FixedTermElabRef
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.haar.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.Measure.haar = MeasureTheory.Measure.haar
-- Mathlib.RingTheory.Radical.NatInt
Nat.dvd_radical_pow_self : ∀ {n : ℕ}, n ≠ 0 → n ∣ UniqueFactorizationMonoid.radical n ^ n
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- **Alias** of `LinearMap.toMatrix_innerₛₗ_apply`.

---

The matrix representation of `innerSL 𝕜 x` given by an orthonormal basis `b` and `b₂`
is equal to `vecMulVec (star b₂) (star (b.repr x))`.  -/
toMatrix_innerSL_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {m : Type u_7} {n : Type u_8} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : Fintype m]
  (b : OrthonormalBasis n 𝕜 E) (b₂ : OrthonormalBasis m 𝕜 𝕜) (x : E),
  (LinearMap.toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) = Matrix.vecMulVec (star ⇑b₂) (star (b.repr x).ofLp)
-- Mathlib.Algebra.Group.Hom.Defs
/-- The underlying function  -/
ZeroHom.toFun : {M : Type u_10} → {N : Type u_11} → [inst : Zero M] → [inst_1 : Zero N] → ZeroHom M N → M → N
-- Mathlib.Order.Filter.Partial
Filter.rcomap.eq_1 : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (f : Filter β),
  Filter.rcomap r f =
    { sets := SetRel.image {(s, t) | r.core s ⊆ t} f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSeparatedFor_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {f : X ⟶ Y},
  CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Presieve.singleton f) ↔
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (P.map f.op))
-- Mathlib.Topology.Algebra.MulAction
ContinuousWithinAt.fun_vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y},
  ContinuousWithinAt f s b → ContinuousWithinAt g s b → ContinuousWithinAt (fun i => f i +ᵥ g i) s b
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- The image of a local diffeomorphism is open.  -/
IsLocalDiffeomorph.image : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} → IsLocalDiffeomorph I J n f → TopologicalSpace.Opens N
-- Mathlib.Order.RelSeries
RelSeries.take.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)),
  p.take i =
    { length := ↑i,
      toFun := fun x =>
        match x with
        | ⟨j, h⟩ => p.toFun ⟨j, ⋯⟩,
      step := ⋯ }
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.instCoeLinearEquiv : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → Coe (M₁ ≃SL[σ₁₂] M₂) (M₁ ≃ₛₗ[σ₁₂] M₂)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x y : αᵒᵈ},
  Set.Icc (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Icc x y
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAdjointPair.smul : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} {B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂} {f : M → M₁} {g : M₁ → M} (c : R),
  B.IsAdjointPair B' f g → B.IsAdjointPair B' (c • f) (c • g)
-- Mathlib.Data.Vector.Basic
List.Vector.toList_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : List.Vector α n)
  (hp : ∀ x ∈ v.toList, p x), (List.Vector.pmap f v hp).toList = List.pmap f v.toList hp
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle between three points is π if and only if the second point is strictly
between the other two.  -/
EuclideanGeometry.oangle_eq_pi_iff_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Sbtw ℝ p₁ p₂ p₃
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A version of the layer cake formula for bounded continuous functions and finite measures:
`∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt`.  -/
MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le : ∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  (f : BoundedContinuousFunction α ℝ) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  0 ≤ᵐ[μ] ⇑f → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a | t ≤ f a}
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_1.eq : ∀ {α : Type u} {β : Type v} {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1}
  {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1}
  (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (F_1 : (t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Node.below_3 t → motive_4 t),
  Lean.PersistentHashMap.Node.brecOn_1 t F_1 F_2 F_3 F_4 =
    F_2 t (Lean.PersistentHashMap.Node.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Lean.Elab.InfoTree.Main
/-- Similar to `realizeGlobalName`, but it also adds the resolved name to the info tree.  -/
Lean.Elab.realizeGlobalNameWithInfos : Lean.Syntax → Lean.Name → Lean.CoreM (List (Lean.Name × List String))
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- Given a box `I₀` in `ℝⁿ⁺¹`, `f x : Box (Fin n) → G` is a family of functions indexed by a real
`x` and for `x ∈ [I₀.lower i, I₀.upper i]`, `f x` is box-additive on subboxes of the `i`-th face of
`I₀`, then `fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)` is box-additive on subboxes
of `I₀`.  -/
BoxIntegral.BoxAdditiveMap.upperSubLower : {n : ℕ} →
  {G : Type u} →
    [inst : AddCommGroup G] →
      (I₀ : BoxIntegral.Box (Fin (n + 1))) →
        (i : Fin (n + 1)) →
          (f : ℝ → BoxIntegral.Box (Fin n) → G) →
            (fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(I₀.face i)) →
              (∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)),
                  f x J = (fb ⟨x, hx⟩) J) →
                BoxIntegral.BoxAdditiveMap (Fin (n + 1)) G ↑I₀
-- Mathlib.Order.SymmDiff
bihimp_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : GeneralizedHeytingAlgebra α] [inst_1 : GeneralizedHeytingAlgebra β]
  (a b : α × β), (bihimp a b).2 = bihimp a.2 b.2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] [Inhabited α]
  {k k' : α} {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toCycle.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f f_1 : Equiv.Perm α) (e_f : f = f_1) (hf : f.IsCycle),
  f.toCycle hf = f_1.toCycle ⋯
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.dist_eq_zero_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → (G.dist u v = 0 ↔ u = v)
-- Std.Tactic.Do.Syntax
/-- `mexists` is like `exists`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mexists 42
```
 -/
Lean.Parser.Tactic.mexists : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Monoid
continuous_one : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : One M], Continuous 1
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.bullet : Lean.Parser.ParserFn
-- Mathlib.Order.Filter.Extr
IsMinOn.sub : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {s : Set α}, IsMinOn f s a → IsMaxOn g s a → IsMinOn (fun x => f x - g x) s a
-- Lean.CoreM
/-- State for the CoreM monad.  -/
Lean.Core.State : Type
-- Mathlib.Logic.Equiv.List
/-- An equivalence between `α` and `β` generates an equivalence between `List α` and `List β`.  -/
Equiv.listEquivOfEquiv : {α : Type u_1} → {β : Type u_2} → α ≃ β → List α ≃ List β
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt32
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssocProd_apply_snd_snd : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : (a : α × β) × γ a.1 a.2),
  (Equiv.sigmaAssocProd a).snd.snd = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a).snd
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_ofList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, k ∈ Std.DHashMap.ofList l ↔ (List.map Sigma.fst l).contains k = true
-- Mathlib.Order.CompleteLattice.Defs
/-- A complete lattice is a bounded lattice which has suprema and infima for every subset.  -/
CompleteLattice : Type u_8 → Type u_8
-- Mathlib.Algebra.Ring.Parity
/-- **Alias** of the forward direction of `even_iff_two_dvd`. -/
Even.two_dvd : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → 2 ∣ a
-- Mathlib.Data.List.Intervals
List.Ico.filter_lt_of_top_le : ∀ {n m l : ℕ}, m ≤ l → List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n m
-- Init.Data.Rat.Lemmas
Rat.inv_inv : ∀ (a : ℚ), a⁻¹⁻¹ = a
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The measurable equivalence defined by an orthonormal basis is volume preserving.  -/
OrthonormalBasis.measurePreserving_measurableEquiv : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F]
  (b : OrthonormalBasis ι ℝ F),
  MeasureTheory.MeasurePreserving (⇑b.measurableEquiv) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_sup_nhds_apply : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeSup L] [inst_2 : OrderBot L] [ContinuousSup L],
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (fun a => s.sup fun x => f x a) l (nhds (s.sup g))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (β_ Z Y).inv h) =
    CategoryTheory.CategoryStruct.comp (β_ Z X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h)
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.distribMulAction : {M : Type u_1} →
  {N : Type u_2} →
    {R : Type u_5} →
      [inst : Monoid R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : AddMonoid N] → [DistribMulAction R M] → [DistribMulAction R N] → DistribMulAction R (M × N)
-- Std.Time.DateTime.Timestamp
Std.Time.instLawfulEqOrdTimestamp : Std.LawfulEqOrd Std.Time.Timestamp
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- the underlying functor.  -/
CategoryTheory.MonoidalCategory.DayFunctor.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            CategoryTheory.MonoidalCategory.DayFunctor C V → CategoryTheory.Functor C V
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Aesop.Util.Basic
Aesop.forEachExprInGoal : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          [MonadControlT Lean.MetaM m] → [MonadLiftT Lean.MetaM m] → Lean.MVarId → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.think.eq_1 : ∀ {α : Type u}, Stream'.WSeq.think = Stream'.Seq.cons none
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearEquiv_apply : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i)
  (x : Π₀ (i : ι), β₁ i), (DFinsupp.mapRange.linearEquiv e) x = DFinsupp.mapRange (fun i x => (e i) x) ⋯ x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_roc : ∀ {a b : ℤ}, (a<...=b).size = (b - a).toNat
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.q : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} →
          (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w) → self.aig.RefVec w
-- Batteries.Data.List.Basic
/-- Quinary version of `List.zipWith`.  -/
List.zipWith₅ : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {ε : Type u_5} → {ζ : Type u_6} → (α → β → γ → δ → ε → ζ) → List α → List β → List γ → List δ → List ε → List ζ
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongLimit.isStrongPrelimit : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → c.IsStrongPrelimit
-- Mathlib.Order.RelSeries
RelSeries.last_mem : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.last ∈ x