mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ordered_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a.fst b.fst = Ordering.lt) t.toList
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isDominant : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f] [AlgebraicGeometry.IsReduced Y],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant f
-- Batteries.Recycling.RBTree.Basic
RBTree.instReprRBColor.repr : RBTree.RBColor → ℕ → Std.Format
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι),
  c.prev j = i →
    ∀ (hk : c.next j = k) {A : C} (x₂ : A ⟶ K.X j) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0),
      CategoryTheory.CategoryStruct.comp (K.liftCycles x₂ k hk hx₂) (K.homologyπ j) = 0 ↔
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j)
-- Std.Async.Basic
Std.Async.EAsync.instInhabited : {ε α : Type} → [Inhabited ε] → Inhabited (Std.Async.EAsync ε α)
-- Lean.Attributes
Lean.ParametricAttributeImpl : Type → Type
-- Mathlib.Data.Nat.ModEq
Nat.chineseRemainder_lt_mul : ∀ {m n : ℕ} (co : n.Coprime m) (a b : ℕ), n ≠ 0 → m ≠ 0 → ↑(Nat.chineseRemainder co a b) < n * m
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ext : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, (∀ (x : P₁), e x = e' x) → e = e'
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∈ m₂ → (m₁ \ m₂)[k]! = default
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.feature : Lean.Parser.Category
-- Mathlib.Geometry.Manifold.ChartedSpace
modelProd_range_prod_id : ∀ {H : Type u_5} {H' : Type u_6} {α : Type u_7} (f : H → α), (Set.range fun p => (f p.1, p.2)) = Set.range f ×ˢ Set.univ
-- Mathlib.Data.Int.Order.Units
Int.units_mul_self : ∀ (u : ℤˣ), u * u = 1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_apply_apply : ∀ {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁), e.symm (e b) = b
-- Lean.Parser.Term
Lean.Parser.Term.negConfigItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.vertical_apply : ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ι → α) (l : Combinatorics.Line α ι') (x : α),
  ↑(Combinatorics.Line.vertical v l) x = Sum.elim v (↑l x)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).unitIso =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso
-- Init.Data.UInt.Lemmas
UInt8.toNat.inj : ∀ {a b : UInt8}, a.toNat = b.toNat → a = b
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
      h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.Computability.RecursiveIn
ComputableIn.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {O : Set (ℕ →. ℕ)},
  ComputableIn O Prod.snd
-- Mathlib.Data.NNReal.Defs
/-- A `Module` over `ℝ` restricts to a `Module` over `ℝ≥0`.  -/
NNReal.instModuleOfReal : {M : Type u_1} → [inst : AddCommMonoid M] → [Module ℝ M] → Module NNReal M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)} {hc : k' ∈ t.alter k f},
  (t.alter k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ ((f (t.get? k)).get ⋯) else t.get k' ⋯
-- Mathlib.Data.Seq.Basic
/-- Coinductive principle for `Pairwise` that assumes that `R` is transitive. Compared to
`Pairwise.coind`, this allows you to prove `R hd tl.head` instead of `tl.All (R hd ·)` in `step`.
 -/
Stream'.Seq.Pairwise.coind_trans : ∀ {α : Type u} {R : α → α → Prop} [IsTrans α R] {s : Stream'.Seq α} (motive : Stream'.Seq α → Prop),
  motive s →
    (∀ (hd : α) (tl : Stream'.Seq α), motive (Stream'.Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl) →
      Stream'.Seq.Pairwise R s
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.congrTheorem.sizeOf_spec : ∀ (thm : Lean.Meta.CongrTheorem), sizeOf (Lean.Meta.Sym.CongrInfo.congrTheorem thm) = 1 + sizeOf thm
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial (over `K`) of `σ : L ≃ₐ[K] L` is `X ^ (orderOf σ) - 1`.  -/
minpoly_algEquiv_toLinearMap : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  (σ : L ≃ₐ[K] L), IsOfFinOrder σ → minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
-- Mathlib.Algebra.Group.Shrink
equivShrink_smul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] {M : Type u_3} [inst_1 : SMul M α] (m : M) (x : α),
  (equivShrink α) (m • x) = m • (equivShrink α) x
-- Init.Data.String.Basic
/-- The slice from the beginning of `s` up to `p` (exclusive).  -/
String.sliceTo : (s : String) → s.Pos → String.Slice
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X ⟶ Y),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.functor.map α).hom =
    α.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.disjoint_coe : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, Disjoint ↑I ↑J ↔ Disjoint ↑I ↑J
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `iInf_iSup_of_antitone`. -/
Set.iInf_iSup_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Antitone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
-- Mathlib.Data.Sum.Order
Sum.inl_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone Sum.inl
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀]
  (x : MvPolynomial ι R₀),
  (Algebra.Presentation.tensorModelOfHasCoeffsEquiv R₀).symm ((MvPolynomial.aeval P.val) x) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) x
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y) =
    CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_csSup_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] (e : α ≃o β) {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → e (sSup s) = ⨆ x, e ↑x
-- Mathlib.Data.Analysis.Filter
/-- `Unit` is a realizer for the bottom filter  -/
Filter.Realizer.bot : {α : Type u_1} → ⊥.Realizer
-- Mathlib.Topology.Irreducible
eq_irreducibleComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {x : X},
  IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x
-- Init.Data.List.Scan.Lemmas
List.getElem_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} {b : β} {l : List α} {f : β → α → β} (h : i + 1 < (List.scanl f b l).length),
  (List.scanl f b l)[i + 1] = f (List.scanl f b l)[i] l[i]
-- Mathlib.Order.CompleteLattice.Basic
Prop.instCompleteLattice : CompleteLattice Prop
-- Mathlib.Probability.Process.Adapted
/-- The norm of a progressive process is progressive.  -/
MeasureTheory.IsProgressive.norm : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : NormedAddCommGroup β]
  [OpensMeasurableSpace β], MeasureTheory.IsProgressive f u → MeasureTheory.IsProgressive f fun t ω => ‖u t ω‖
-- Mathlib.Algebra.Order.Field.Basic
/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_neg_of_lt` and
`lt_of_one_div_lt_one_div`  -/
one_div_le_one_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (1 / a ≤ 1 / b ↔ b ≤ a)
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticM.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.RuleTacDescr.tacticM decl = Aesop.RuleTacDescr.tacticM decl_1) = (decl = decl_1)
-- Mathlib.Data.List.Duplicate
List.not_duplicate_singleton : ∀ {α : Type u_1} (x y : α), ¬List.Duplicate x [y]
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_comp_right : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  {D : V} (h : C ⟶ D) (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel f (CategoryTheory.CategoryStruct.comp g h) ⋯ =
    CategoryTheory.CategoryStruct.comp (imageToKernel f g w)
      ((CategoryTheory.Limits.kernelSubobject g).ofLE
        (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)) ⋯)
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- On functions of the form `(x, y) ↦ f x * g y`, the measure `prodMk μ ν` agrees with the
algebraic tensor product of `μ` and `ν`.  -/
AbstractMeasure.prodMk_prod_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : LocallyCompactSpace X] [inst_6 : LocallyCompactSpace Y] (f : C(X, R))
  (g : C(Y, R)), ((AbstractMeasure.prodMk μ) ν) (f.comp ContinuousMap.fst * g.comp ContinuousMap.snd) = μ f * ν g
-- Lean.Data.Json.Basic
Lean.JsonNumber.instToString : ToString Lean.JsonNumber
-- Lean.Structure
_private.Lean.Structure.0.Lean.StructureState.mk.inj : ∀ {map map_1 : Lean.PersistentHashMap Lean.Name Lean.StructureInfo}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_sin_eq_of_two_nsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → |θ.sin| = |ψ.sin|
-- Mathlib.Topology.Bases
TopologicalSpace.SecondCountableTopology.to_separableSpace : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α], TopologicalSpace.SeparableSpace α
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context : Type
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.functoriality_faithful`. -/
CategoryTheory.Limits.Cones.functoriality_faithful : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Faithful], (CategoryTheory.Limits.Cone.functoriality F G).Faithful
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- Helper when we need some `c.rel i j` (i.e. `ComplexShape.down ℕ`),
e.g. `c_mk n (n+1) rfl`  -/
AlgebraicTopology.DoldKan.c_mk : ∀ (i j : ℕ), j + 1 = i → AlgebraicTopology.DoldKan.c.Rel i j
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `assoc_comp_map_assoc` that only fires when `f₃ ≠ id`.  -/
CoassocSimps.assoc_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^64 - 1` for natural numbers greater than or equal to `2^64`.
 -/
UInt64.ofNatClamp : ℕ → UInt64
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid Mᵃᵒᵖ], DomAddAct.instAddCommMonoidOfAddOpposite = inst
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffEDist_union_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s₁ s₂ t₁ t₂ : Set α},
  Metric.hausdorffEDist (s₁ ∪ s₂) (t₁ ∪ t₂) ≤ max (Metric.hausdorffEDist s₁ t₁) (Metric.hausdorffEDist s₂ t₂)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toFun_eq_coe : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : ContDiffMapSupportedIn E F n K},
  f.toFun = ⇑f
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordMonoidHom.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R],
  Ring.ordMonoidHom = { toFun := fun x => Multiplicative.ofAdd (Ring.ord R ↑x).toNat, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.weaken : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {K' : NNReal}, K ≤ K' → LipschitzWith K' f
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Any measurable space is equivalent to itself.  -/
MeasurableEquiv.refl : (α : Type u_6) → [inst : MeasurableSpace α] → α ≃ᵐ α
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.prod_map_le_prod_map₀ : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {ι : Type u_2} {s : List ι} (f g : ι → R),
  (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → (List.map f s).prod ≤ (List.map g s).prod
-- Init.Data.Vector.OfFn
Vector.toList_ofFnM : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {f : Fin n → m α},
  Vector.toList <$> Vector.ofFnM f = List.ofFnM f
-- Mathlib.Tactic.Widget.Conv
/-- Given an `e : Expr` and `pos : SubExpr.Pos`, `Path.ofSubExprPos expr pos` generates
the `Path` corresponding to traversing `pos` starting at the reference expression `e`.
 -/
Mathlib.Tactic.Conv.Path.ofSubExprPos : Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM Mathlib.Tactic.Conv.Path
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- If all edge weights are positive, then the weight of any path is positive.  -/
Quiver.Path.weight_pos : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {w : {i j : V} → (i ⟶ j) → R},
  (∀ {i j : V} (e : i ⟶ j), 0 < w e) → ∀ {i j : V} (p : Quiver.Path i j), 0 < Quiver.Path.weight (fun {i j} => w) p
-- Mathlib.Computability.DFA
/-- Set of acceptance states.  -/
DFA.accept : {α : Type u} → {σ : Type v} → DFA α σ → Set σ
-- Mathlib.Data.Set.Basic
Set.not_subset_iff_exists_mem_notMem : ∀ {α : Type u_1} {s t : Set α}, ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.copy_eq_empty_iff : ∀ {s : String.Slice}, s.copy = "" ↔ s.isEmpty = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLE_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂),
  Std.DTreeMap.Const.getEntryLE t₁ k h' = Std.DTreeMap.Const.getEntryLE t₂ k ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β)
  (t : Std.DTreeMap.Internal.Impl α fun x => β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.alter k f t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      match f none with
      | none =>
        { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some v =>
        {
          impl :=
            Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
          balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl =>
      match compare k k' with
      | Ordering.lt =>
        match Std.DTreeMap.Internal.Impl.Const.alter k f l' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.gt =>
        match Std.DTreeMap.Internal.Impl.Const.alter k f r' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balance k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.eq =>
        match f (some v') with
        | none => { impl := l'.glue r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
        | some v =>
          { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_mem_of_mem_ofUnits : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} {h₁ : IsUnit x}, x ∈ S.ofUnits → h₁.unit ∈ S
-- Init.SimpLemmas
beq_true : ∀ (b : Bool), (b == true) = b
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The short complex `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₁' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.iSup_range_lsingle : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι], ⨆ i, (DFinsupp.lsingle i).range = ⊤
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
summable_pow_mul_cexp : ∀ (k : ℕ) (e : ℕ+) (z : UpperHalfPlane),
  Summable fun c => ↑c ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑e * ↑z) ^ c
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_trinomial_subset : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (k m n : ℕ) (x y z : R),
  (SkewPolynomial.C x * SkewPolynomial.X ^ k + SkewPolynomial.C y * SkewPolynomial.X ^ m +
        SkewPolynomial.C z * SkewPolynomial.X ^ n).support ⊆
    {k, m, n}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSetWalkLengthLT : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype ↑{p | p.length < n}
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : LinearMap.GeneralLinearGroup R M), ↑((LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ↑f
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.card_mul_card : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → Nat.card ↑S * Nat.card ↑T = Nat.card G
-- Mathlib.Analysis.Convex.Quasiconvex
quasiconcaveOn_iff_min_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.mk : {G : Type u} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      (toAddSubgroup : AddSubgroup G) → IsClosed toAddSubgroup.carrier → ClosedAddSubgroup G
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_sum : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : Zero N] {f : α → β}
  {s : α →₀ N} {v : α → N → α →₀ M}, Finsupp.mapDomain f (s.sum v) = s.sum fun a b => Finsupp.mapDomain f (v a b)
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.corecShape.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {β : Type v} (g₀ : β → P.A) (g₂ : (b : β) → P.last.B (g₀ b) → β),
  MvPFunctor.M.corecShape P g₀ g₂ = PFunctor.M.corec fun b => ⟨g₀ b, g₂ b⟩
-- Lean.SubExpr
Lean.SubExpr.Pos.pushProj : Lean.SubExpr.Pos → Lean.SubExpr.Pos