mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α) (q : ℚ) {A : Set β},
      MeasurableSet A → ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega0_lt_omega_one : Ordinal.omega0 < Ordinal.omega 1
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f n` is bounded in absolute value by a constant times `n^(x-1)` and `re s > x`,
then the `LSeries` of `f` is summable at `s`.  -/
LSeriesSummable_of_le_const_mul_rpow : ∀ {f : ℕ → ℂ} {x : ℝ} {s : ℂ}, x < s.re → (∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)) → LSeriesSummable f s
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- **Alias** of the forward direction of `hasFDerivAt_iff_hasGradientAt`. -/
HasFDerivAt.hasGradientAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : StrongDual 𝕜 F},
  HasFDerivAt f frechet x → HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) x
-- Mathlib.Analysis.RCLike.Basic
/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are star ordered rings.
(That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)

Note this is only an instance with `open scoped ComplexOrder`.  -/
RCLike.toStarOrderedRing : ∀ {K : Type u_1} [inst : RCLike K], StarOrderedRing K
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i},
  HasFDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
    HasFDerivAt φ (ContinuousLinearMap.proj 0 ∘SL φ') x ∧ HasFDerivAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') x
-- Mathlib.Order.Antichain
IsAntichain.swap : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → IsAntichain (Function.swap r) s
-- Init.Prelude
instInhabitedRaw_1 : Inhabited Substring.Raw
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_disjoint_Ico : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  b ≤ c → Disjoint (Multiset.Ico a b) (Multiset.Ico c d)
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.ext : ∀ {α : Type u_1} {f : α → α} {x y : IterateAddAct f}, x.val = y.val → x = y
-- Mathlib.Analysis.Normed.Field.Lemmas
DilationEquiv.mulLeft_apply : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α), (DilationEquiv.mulLeft a ha) x = a * x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (k, v) ∈ Std.DTreeMap.Raw.Const.toArray t ↔ Std.DTreeMap.Raw.Const.get? t k = some v
-- Mathlib.Data.List.Sort
List.sortedGT_iff_strictAnti_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT ↔ StrictAnti l.get
-- Mathlib.Algebra.Ring.Defs
CommSemiring.toNonAssocCommSemiring : {α : Type u} → [CommSemiring α] → NonAssocCommSemiring α
-- Mathlib.Order.Monotone.Basic
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright.  -/
not_monotone_not_antitone_iff_exists_lt_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablySeparated_subtype_of_hasCountableSeparatingOn : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [h : HasCountableSeparatingOn α MeasurableSet s],
  MeasurableSpace.CountablySeparated ↑s
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of the reverse direction of `Matroid.indep_singleton`. -/
Matroid.IsNonloop.indep : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → M.Indep {e}
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S],
  Function.Injective (LinearEquiv.restrictScalars R)
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.mk.injEq : ∀ {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 : B ⟶ X)
  (fac_left :
    autoParam (CategoryTheory.CategoryStruct.comp i l = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam)
  (fac_right :
    autoParam (CategoryTheory.CategoryStruct.comp l p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam)
  (l_1 : B ⟶ X)
  (fac_left_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i l_1 = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam)
  (fac_right_1 :
    autoParam (CategoryTheory.CategoryStruct.comp l_1 p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam),
  ({ l := l, fac_left := fac_left, fac_right := fac_right } =
      { l := l_1, fac_left := fac_left_1, fac_right := fac_right_1 }) =
    (l = l_1)
-- Mathlib.Control.Monad.Writer
/-- Creates an instance of `Monad`, with explicitly given `empty` and `append` operations.

Previously, this would have used an instance of `[Monoid ω]` as input.
In practice, however, `WriterT` is used for logging and creating lists so restricting to
monoids with `Mul` and `One` can make `WriterT` cumbersome to use.

This is used to derive instances for both `[EmptyCollection ω] [Append ω]` and `[Monoid ω]`.
 -/
WriterT.monad : {M : Type u → Type v} → {ω : Type u} → [Monad M] → ω → (ω → ω → ω) → Monad (WriterT ω M)
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.pathEquivList_nil : ∀ {α : Type u_1}, Quiver.SingleObj.pathEquivList Quiver.Path.nil = []
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
OrderIso.mulRight₀.congr_simp : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a a_1 : G₀)
  (e_a : a = a_1) (ha : 0 < a), OrderIso.mulRight₀ a ha = OrderIso.mulRight₀ a_1 ⋯
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_zero : ∀ {E : Type u_3} [inst : EMetricSpace E] (A : Set E), Metric.externalCoveringNumber 0 A = A.encard
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ A ⟹ Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g))) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Data.List.Sublists
List.mem_sublists : ∀ {α : Type u} {s t : List α}, s ∈ t.sublists ↔ s.Sublist t
-- Mathlib.CategoryTheory.CatCommSq
/-- Vertical inverse of a 2-commutative square  -/
CategoryTheory.CatCommSq.vInv : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : C₁ ≌ C₃) →
                    (R : C₂ ≌ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) →
                        CategoryTheory.CatCommSq T L.functor R.functor B →
                          CategoryTheory.CatCommSq B L.inverse R.inverse T
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_filterMap : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → Option γ) (s : Multiset α),
  Multiset.filterMap g (Multiset.filterMap f s) = Multiset.filterMap (fun x => (f x).bind g) s
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainTermGoalParams : Lean.FromJson Lean.Lsp.PlainTermGoalParams
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.norm_integral_le_integral_norm : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G), ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
-- Init.System.ST
ST.Prim.Ref.take : {σ α : Type} → ST.Ref σ α → ST σ α
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.compl_F_eq_I : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), (↑IF.F)ᶜ = ↑IF.I
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instSMulProd : (D : Type u_1) →
  (Q : Type u_2) → [inst : Group D] → [Group Q] → (Λ : Type u_3) → [MulAction D Λ] → SMul (D ≀ᵣ Q) (Λ × Q)
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.start_v : ∀ (a b : ℕ+), (PNat.XgcdType.start a b).v = (↑a, ↑b)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.coe_X_compare : ∀ (K : Type u_2) [inst : Field K],
  (LaurentSeries.ratfuncAdicComplRingEquiv K)
      {
        toCompletion :=
          ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K))).symm
              RatFunc.X) } =
    (HahnSeries.ofPowerSeries ℤ K) PowerSeries.X
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_iUnion₂ : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (a : α) (s : (i : ι) → κ i → Set β),
  a +ᵥ ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a +ᵥ s i j
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_left_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg) g)
        CategoryTheory.AddMonObj.add =
      h ↔
    g =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h)
        CategoryTheory.AddMonObj.add
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (t.insertManyIfNewUnit l).getKey? k = t.getKey? k
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The diagram in `Opens X` indexed by pairwise intersections from `U` is isomorphic
(in fact, equal) to the diagram factored through `OpensLeCover U`.
 -/
TopCat.Presheaf.SheafCondition.pairwiseDiagramIso : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      CategoryTheory.Pairwise.diagram U ≅
        (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).comp
          (CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ U i)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instNontrivialSubtypeMemTop : ∀ {G : Type u_1} [inst : Group G] [Nontrivial G], Nontrivial ↥⊤
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.faceOppositeCentroid.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i = (s.faceOpposite i).centroid
-- Mathlib.Topology.Constructions
/-- Suppose `A i` is a family of topological spaces indexed by `i : ι`, and `X` is a type
endowed with a family of maps `f i : X → A i` for every `i : ι`, hence inducing a
map `g : X → Π i, A i`. This lemma shows that infimum of the topologies on `X` induced by
the `f i` as `i : ι` varies is simply the topology on `X` induced by `g : X → Π i, A i`
where `Π i, A i` is endowed with the usual product topology.  -/
inducing_iInf_to_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {X : Type u_9} (f : (i : ι) → X → A i),
  Topology.IsInducing fun x i => f i x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
ModuleCat.shortExact_projectiveShortComplex : ∀ {R : Type u} [inst : Ring R] [inst_1 : Small.{v, u} R] (M : ModuleCat R), M.projectiveShortComplex.ShortExact
-- Mathlib.RingTheory.Ideal.Maps
Module.mem_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R},
  r ∈ Module.annihilator R M ↔ ∀ (m : M), r • m = 0
-- Init.Data.SInt.Lemmas
Int8.lt_or_eq_of_le : ∀ {a b : Int8}, a ≤ b → a < b ∨ a = b
-- Mathlib.Analysis.ODE.Basic
/-- `γ` is an integral curve for `v` at `t₀` iff `γ` is an integral curve on some interval
containing `t₀`.  -/
isIntegralCurveAt_iff_exists_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B]
  (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C] [inst_4 : CategoryTheory.FinitaryExtensive C]
  [∀ (X : C), CategoryTheory.Projective X] [CategoryTheory.Limits.PreservesFiniteProducts s],
  (CategoryTheory.coherentTopology C).HasSheafCompose s
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_sum : ∀ {R : Type u} {M : Type v} {ι : Type u_3} [inst : AddCommMonoid R] [inst_1 : AddCommMonoid M] (s : Finset ι)
  (f : ι → TrivSqZeroExt R M), (∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂ₛₗ_apply : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
  (g : P →ₛₗ[σ₃₄] Q) (m : M) (n : N), ((f.compr₂ₛₗ g) m) n = g ((f m) n)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc_union_Ioc_cycle : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α},
  Set.Ioc a b ∪ Set.Ioc b c ∪ Set.Ioc c a = Set.Ioc (min a (min b c)) (max a (max b c))
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} [inst_1 : SizeOf 𝒮] (toFunctor : CategoryTheory.Functor 𝒳.obj 𝒴.obj)
  (w : autoParam (toFunctor.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam),
  sizeOf { toFunctor := toFunctor, w := w } = 1 + sizeOf toFunctor + sizeOf w
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.pred'.match_1.eq_3 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit1 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_3 n
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] {I : FractionalIdeal S P} {g : P →ₐ[R] P'} {y : P'},
  y ∈ FractionalIdeal.map g I ↔ ∃ x ∈ I, g x = y
-- Init.Data.Array.Lemmas
Array.filterMap_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {ys zs : Array β} {f : α → Option β},
  Array.filterMap f xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Array.filterMap f as = ys ∧ Array.filterMap f bs = zs
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.Functor.closedSieves_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) (X : Cᵒᵖ),
  (CategoryTheory.Functor.closedSieves J₁).obj X = {S | J₁.IsClosed S}
-- Aesop.Forward.State
/-- Complete matches for this cluster.  -/
Aesop.ClusterState.completeMatches : Aesop.ClusterState → Lean.PHashSet Aesop.Match
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfcₙ_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A),
  cfcₙ f a ∈ NonUnitalStarAlgebra.elemental 𝕜 a
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `deriv_fun_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
deriv_fun_const_smul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), deriv (fun y => c • f y) x = c • deriv f x
-- Mathlib.Tactic.ITauto
/-- The search phase, which deals with the level 3 rules, which are rules that are not validity
preserving and so require proof search. One obvious one is the or-introduction rule: we prove
`A ∨ B` by proving `A` or `B`, and we might have to try one and backtrack.

There are two rules dealing with implication in this category: `p, p → C ⊢ B` where `p` is an
atom (which is safe if we can find it but often requires the right search to expose the `p`
assumption), and `(A₁ → A₂) → C ⊢ B`. We decompose the double implication into two subgoals: one to
prove `A₁ → A₂`, which can be written `A₂ → C, A₁ ⊢ A₂` (where we used `A₁` to simplify
`(A₁ → A₂) → C`), and one to use the consequent, `C ⊢ B`. The search here is that there are
potentially many implications to split like this, and we have to try all of them if we want to be
complete.  -/
Mathlib.Tactic.ITauto.search : Mathlib.Tactic.ITauto.Context → Mathlib.Tactic.ITauto.IProp → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)
-- Mathlib.NumberTheory.Ostrowski
/-- Given two natural numbers `n, m` greater than 1 we have `f n ≤ f m ^ logb m n`.  -/
Rat.AbsoluteValue.le_pow_log : ∀ {f : AbsoluteValue ℚ ℝ} {m n : ℕ}, 1 < m → 1 < n → (¬∀ (n : ℕ), f ↑n ≤ 1) → f ↑n ≤ f ↑m ^ Real.logb ↑m ↑n
-- Init.Data.Array.Lemmas
Array.getElem_modify_of_ne : ∀ {α : Type u_1} {j : ℕ} {xs : Array α} {i : ℕ},
  i ≠ j → ∀ (f : α → α) (hj : j < (xs.modify i f).size), (xs.modify i f)[j] = xs[j]
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonAssocSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonAssocSemiring β] → [IsTopologicalSemiring β] → NonAssocSemiring C(α, β)
-- Mathlib.Topology.Separation.Hausdorff
R1Space.t2Space_iff_t0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], T2Space X ↔ T0Space X
-- Mathlib.Data.List.Chain
List.IsChain.dropLast : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l → List.IsChain R l.dropLast
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyEq.countable_iUnion`. -/
EventuallyEq.countable_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋃ i, s i =ᶠ[l] ⋃ i, t i
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.IsConvexDist.subtype : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] (s : Set X)
  (hs : Convexity.IsConvexSet ℝ s), Convexity.IsConvexDist ↑s
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_smul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} {α : Type u_12} [inst : SMul R α] (x : R)
  (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α),
  x • Matrix.fromBlocks A B C D = Matrix.fromBlocks (x • A) (x • B) (x • C) (x • D)
-- Init.Data.SInt.Basic
instAndOpISize : AndOp ISize
-- Mathlib.Geometry.Diffeology.Basic
/-- The locality axiom of diffeologies, phrased in terms of `isPlotOn`.  -/
DiffeologicalSpace.CorePlotsOn.locality : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u)
  {p : EuclideanSpace ℝ (Fin n) → X}, (∀ x ∈ u, ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ self.isPlotOn hv p) → self.isPlotOn hu p
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α},
  s * t = Finset.image (fun p => p.1 * p.2) (s ×ˢ t)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.RankFinite.isRkFinite : ∀ {α : Type u_1} {M : Matroid α} [M.RankFinite] (X : Set α), M.IsRkFinite X
-- Mathlib.AlgebraicGeometry.Restrict
/-- The stalks of an open subscheme are isomorphic to the stalks of the original scheme.  -/
AlgebraicGeometry.Scheme.Opens.stalkIso : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (x : ↥U) → (↑U).presheaf.stalk x ≅ X.presheaf.stalk ↑x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.IsRepresentable.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)},
  (∃ Y, Nonempty (F.RepresentableBy Y)) → F.IsRepresentable
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.ofNat_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).comp p = ↑n
-- Lean.Hygiene
Lean.Unhygienic.Context.mk : Lean.Syntax → Lean.MacroScope → Lean.Unhygienic.Context
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.countP` as a bundled additive monoid homomorphism.  -/
FreeAddMonoid.countP : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → FreeAddMonoid α →+ ℕ