mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Net.Addr
Std.Net.InterfaceAddress.mk : String → Std.Net.MACAddr → Bool → Std.Net.IPAddr → Std.Net.IPAddr → Std.Net.InterfaceAddress
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.hasDerivAt_cos : ∀ (x : ℝ), HasDerivAt Real.cos (-Real.sin x) x
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_sub' : ∀ {m n : ℤ}, Even (m - n) ↔ (Odd m ↔ Odd n)
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofInt : ∀ (i : ℤ), (Int8.ofInt i).toBitVec = BitVec.ofInt 8 i
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpNatIso_inv_app : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] [inst_2 : CategoryTheory.CategoryWithHomology V] (i : ι)
  (X : (HomologicalComplex V c)ᵒᵖ),
  (HomologicalComplex.cyclesOpNatIso V c i).inv.app X = ((Opposite.unop X).cyclesOpIso i).inv
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.get : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m],
  MonadStateOf.get = monadLift MonadStateOf.get
-- Mathlib.Tactic.FieldSimp
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), construct another such term `l`, which will have the property that in
the field `$M`, the quotient of the "multiplicative linear combinations" represented by `l₁` and
`l₂` is the multiplicative linear combination represented by `l`.

The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly decreasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.

The construction is as follows: merge the first list and the negation of the second list, except
that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with the same
`ℕ`-component `k`, then contribute a term `(a₁ - a₂, x₁)` to the output list with `ℕ`-component `k`.
 -/
Mathlib.Tactic.FieldSimp.qNF.div : {v : Lean.Level} →
  {M : Q(Type v)} → Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSubtype_symm_apply_coe_snd : ∀ {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a), (↑((Equiv.sigmaSubtype a).symm b)).snd = b
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedCommGroup : {E : Type u_2} → [SeminormedCommGroup E] → SeminormedCommGroup (ULift.{u_5, u_2} E)
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeTC.coe : {α : Sort u} → {β : Sort v} → [self : CoeTC α β] → α → β
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Given a function `f : E → F`, we say that `f` is continuously polynomial (cpolynomial)
at `x` if it admits a finite power series expansion around `x`.  -/
CPolynomialAt : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → E → Prop
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover
of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls
so that each of the new balls has strictly smaller radius than the old one.  -/
exists_iUnion_ball_eq_radius_pos_lt : ∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [ProperSpace α] {c : ι → α} {r : ι → ℝ},
  (∀ (i : ι), 0 < r i) →
    (∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
      ⋃ i, Metric.ball (c i) (r i) = Set.univ →
        ∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)
-- Mathlib.Algebra.Field.Basic
OrderDual.instField : {K : Type u_1} → [Field K] → Field Kᵒᵈ
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.le_rank_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ v, LinearIndependent R v
-- Mathlib.Data.PFun
/-- If advancing one step from `a` on `f` leads to `a' : α`, then `f.fix a = f.fix a'`  -/
PFun.fix_fwd_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a a' : α}, Sum.inr a' ∈ f a → f.fix a = f.fix a'
-- Mathlib.Data.PFun
PFun.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {f g : α →. β}, f = g ↔ ∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a
-- Mathlib.Control.Monad.Cont
ExceptT.mkLabel : {m : Type u → Type v} →
  [Monad m] → {α β ε : Type u} → MonadCont.Label (Except ε α) m β → MonadCont.Label α (ExceptT ε m) β
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.sub : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {f g : X → E},
  MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable g μ → MeasureTheory.LocallyIntegrable (f - g) μ
-- Mathlib.Order.Lattice
inf_rotate : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = b ⊓ c ⊓ a
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ'_assoc : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1))
  (hi' : autoParam (n + i = m) SimplexCategory.δ₀Iter_σ'._auto_1),
  autoParam (↑j = ↑j' + i) SimplexCategory.δ₀Iter_σ'._auto_3 →
    ∀ {Z : SimplexCategory} (h : { len := m } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i ⋯)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j')
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i hi') h)
-- Lean.Syntax
Lean.Syntax.MonadTraverser.getIdx : {m : Type → Type} → [Monad m] → [t : Lean.Syntax.MonadTraverser m] → m ℕ
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_map : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8}
  [inst_7 : AddCommMonoid N₁] [inst_8 : AddCommMonoid N₂] [inst_9 : AddCommMonoid N] [inst_10 : Module R N₁]
  [inst_11 : Module R N₂] [inst_12 : Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10}
  {P : Type u_11} [inst_13 : AddCommMonoid P₁] [inst_14 : AddCommMonoid P₂] [inst_15 : AddCommMonoid P]
  [inst_16 : Module R P₁] [inst_17 : Module R P₂] [inst_18 : Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P}
  (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁)
  (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂) (x : M),
  (hg.map hp i₁ i₂) ((hf.map hg j₁ j₂) x) = (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.lift.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] (x : m α), Std.Iterators.HetT.lift x = liftM x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.tprod_subtype' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  ∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.LimitBicone.mk.injEq : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (bicone : CategoryTheory.Limits.Bicone F)
  (isBilimit : bicone.IsBilimit) (bicone_1 : CategoryTheory.Limits.Bicone F) (isBilimit_1 : bicone_1.IsBilimit),
  ({ bicone := bicone, isBilimit := isBilimit } = { bicone := bicone_1, isBilimit := isBilimit_1 }) =
    (bicone = bicone_1 ∧ isBilimit ≍ isBilimit_1)
-- Plausible.Functions
/-- Compose a total function with a regular function on the left  -/
Plausible.TotalFunction.comp : {α : Type u} → {β : Type v} → {γ : Type w} → (β → γ) → Plausible.TotalFunction α β → Plausible.TotalFunction α γ
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_eq : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E) (w : V), FourierTransform.fourier f w = ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v
-- Mathlib.Order.Interval.Basic
/-- Turn an interval into an interval in the dual order.  -/
Interval.dual : {α : Type u_1} → [inst : LE α] → Interval α ≃ Interval αᵒᵈ
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_mul_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.divConst B * ↑A.card = ↑(A / B).card
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_compl_iInter_compl : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β), ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ
-- Batteries.Lean.EStateM
EStateM.dummySave_apply : ∀ {σ : Type u_1} (s : σ), EStateM.dummySave s = PUnit.unit
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_zero : ∀ {α : Type u} [inst : Lean.Grind.Semiring α], ↑0 = 0
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.face.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s s_1 : Affine.Simplex k P n),
  s = s_1 → ∀ {fs fs_1 : Finset (Fin (n + 1))} (e_fs : fs = fs_1) {m : ℕ} (h : fs.card = m + 1), s.face h = s_1.face ⋯
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- There is a final functor from a small category.  -/
CategoryTheory.FinallySmall.final_smallCategory : ∀ {J : Type u} {inst : CategoryTheory.Category.{v, u} J} [self : CategoryTheory.FinallySmall J], ∃ S x F, F.Final
-- Init.Data.Int.Order
Int.max_lt : ∀ {a b c : ℤ}, max a b < c ↔ a < c ∧ b < c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst.inj : ∀ {x : Int.Internal.Linear.Var} {c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr}
  {x_1 : Int.Internal.Linear.Var} {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr}
  {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.coe_orthogonalDecomposition : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  ↑↑K.orthogonalDecomposition =
    ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ).symm ∘SL K.orthogonalProjectionOnto.prod Kᗮ.orthogonalProjectionOnto
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_comp_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : α → M) (g : α → N), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_div : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] (f g : ι → G₀),
  (Function.support fun a => f a / g a) = Function.support f ∩ Function.support g
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_injective_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)),
  Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f x = f y ↔ g x = g y
-- Mathlib.Algebra.Group.Invertible.Basic
Invertible.mulRight_symm_apply : ∀ {α : Type u} [inst : Monoid α] (a : α) {b : α} (x : Invertible b) (x_1 : Invertible (a * b)),
  (Invertible.mulRight a x).symm x_1 = invertibleOfMulInvertible a b
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ.eq_1 : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal} (hc : c ≠ ⊤)
  (h : μ ≤ c • ν),
  MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ hc h =
    { toFun := fun f => MeasureTheory.MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
/-- The preimage under the projection from the tangent bundle of a set with unique differential in
the basis also has unique differential.  -/
UniqueMDiffOn.tangentBundle_proj_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {s : Set M},
  UniqueMDiff[s] → UniqueMDiff[Bundle.TotalSpace.proj ⁻¹' s]
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.epi_iff_epi_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasPushouts C]
  {f g : CategoryTheory.Over X} (h : f ⟶ g), CategoryTheory.Epi h ↔ CategoryTheory.Epi (CategoryTheory.Over.Hom.left h)
-- Init.Data.Nat.Dvd
Nat.decidable_dvd : DecidableRel fun x1 x2 => x1 ∣ x2
-- Init.Data.UInt.Lemmas
USize.left_eq_add : ∀ {a b : USize}, a = a + b ↔ b = 0
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) [inst_2 : Semiring T]
  (g : S →+* T) (p : Polynomial R), Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp f) p
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instLattice : {G : Type u_1} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousMul G] → Lattice (OpenSubgroup G)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- Coercion from nonnegative simple functions of Lp to nonnegative functions of Lp.  -/
MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    (p : ENNReal) →
      (μ : MeasureTheory.Measure α) →
        (G : Type u_7) → [inst_1 : NormedAddCommGroup G] → [inst_2 : PartialOrder G] → { g // 0 ≤ g } → { g // 0 ≤ g }
-- Batteries.Util.ProofWanted
/-- Whether the surfaced binder is class-valued, so it becomes an instance binder `[…]` on the
enclosing declaration (rather than implicit `{…}`). Only ever `true` for the leaf holes of a
*transparent* reference, where every hole — class-valued or not — must be threaded explicitly into
the inlined application; the opaque path keeps class deps quantified inside the `.Val` binder.  -/
_private.Batteries.Util.ProofWanted.0.WantedDep.isClass : WantedDep✝ → Bool
-- Mathlib.RingTheory.Perfectoid.BDeRham
/-- The de Rham period ring $\mathbb{B}_{dR}$ for general perfectoid ring.
It is defined as $\mathbb{B}_{dR}^+$ inverting the generators of the ideal `ker θ`.
Mathematically, this is equivalent to inverting *a* generator of the ideal `ker θ`
after we show that it is principal.
When $R = \mathcal{O}_{\mathbb{C}_p}$, it coincides
with the classical de Rham period ring.
Note that if `p = 0` in `R`, then this definition is the zero ring.
 -/
BDeRham : (R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) → [Fact (Nat.Prime p)] → [Fact ¬IsUnit ↑p] → [IsAdicComplete (Ideal.span {↑p}) R] → Type u
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context.mk.inj : ∀ {bvars bvars_1 : List Lean.FVarId}, { bvars := bvars } = { bvars := bvars_1 } → bvars = bvars_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The truncation functor on simplicial sets.  -/
SSet.truncation : (n : ℕ) → CategoryTheory.Functor SSet (SSet.Truncated n)
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.liftHom.match_1.eq_2 : ∀ {B : Type u_1} [inst : Quiver B] (motive : (x x_1 : CategoryTheory.FreeBicategory B) → (x ⟶ x_1) → Sort u_3) (a : B)
  (h_1 : (x x_1 : B) → (f : x ⟶ x_1) → motive x x_1 (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a))
  (h_3 :
    (x x_1 b : B) →
      (f : CategoryTheory.FreeBicategory.Hom x b) →
        (g : CategoryTheory.FreeBicategory.Hom b x_1) → motive x x_1 (f.comp g)),
  (match a, a, CategoryTheory.FreeBicategory.Hom.id a with
    | x, x_1, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_1 f
    | a, .(a), CategoryTheory.FreeBicategory.Hom.id .(a) => h_2 a
    | x, x_1, f.comp g => h_3 x x_1 b f g) =
    h_2 a
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.notMem_of_lt_hittingBtwn : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m k : ι}, k < MeasureTheory.hittingBtwn u s n m ω → n ≤ k → u k ω ∉ s
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- **Alias** of `LipschitzWith.mapsTo_closedEBall`. -/
LipschitzWith.mapsTo_emetric_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) (↑K * r))
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.commMonoid : {R : Type u} →
  {M : Type v} →
    [inst : CommMonoid R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : DistribMulAction R M] →
          [inst_3 : DistribMulAction Rᵐᵒᵖ M] → [IsCentralScalar R M] → CommMonoid (TrivSqZeroExt R M)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] [inst_3 : Inhabited α] {k k' : α},
  (↑m).WF →
    ∀ {f : Option (β k) → Option (β k)},
      (m.alter k f).getKey! k' =
        if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts_trans : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {M : Λ → Turing.TM1.Stmt Γ Λ σ} {S : Finset Λ}
  {q₁ q₂ : Turing.TM1.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM1.stmts₁ q₂ → some q₂ ∈ Turing.TM1.stmts M S → some q₁ ∈ Turing.TM1.stmts M S
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.coe_trans : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : Star A] [inst_5 : Star B] [inst_6 : Add C] [inst_7 : Mul C] [inst_8 : Star C] (e₁ : A ≃⋆+* B)
  (e₂ : B ≃⋆+* C), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Init.Sym.DSimp.DSimprocDSL
Lean.Parser.Command.sym_dsimp_field.quot : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Mul
ConvexOn.mul' : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConvexOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → AntivaryOn f g s → ConcaveOn 𝕜 s (f * g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCallHierarchyItem.beq : Lean.Lsp.CallHierarchyItem → Lean.Lsp.CallHierarchyItem → Bool
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
NNRatCast.toOfScientific_def : ∀ {K : Type u_1} [inst : NNRatCast K] (m : ℕ) (b : Bool) (d : ℕ),
  OfScientific.ofScientific m b d = ↑⟨OfScientific.ofScientific m b d, ⋯⟩
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂)[k]? = none
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_neg_iff_add_nonpos_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, a ≤ -b ↔ b + a ≤ 0
-- Mathlib.Analysis.Complex.Order
/-- **Alias** of the reverse direction of `Complex.zero_lt_real`. -/
Mathlib.Meta.Positivity.ofReal_pos : ∀ {x : ℝ}, 0 < x → 0 < ↑x
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.mk.injEq : ∀ (fromDeclName toDeclName thmName fromDeclName_1 toDeclName_1 thmName_1 : Lean.Name),
  ({ fromDeclName := fromDeclName, toDeclName := toDeclName, thmName := thmName } =
      { fromDeclName := fromDeclName_1, toDeclName := toDeclName_1, thmName := thmName_1 }) =
    (fromDeclName = fromDeclName_1 ∧ toDeclName = toDeclName_1 ∧ thmName = thmName_1)
-- Init.Data.SInt.Basic
/-- Strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
 -/
Int64.lt : Int64 → Int64 → Prop
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ} [ProbabilityTheory.IsFiniteKernel ν],
  κ.fst ≤ ν →
    ∀ (a : α) {s : Set β},
      MeasurableSet s →
        ∀ (A : Set γ),
          Filter.Tendsto
            (fun n =>
              MeasureTheory.eLpNorm
                ((fun x => κ.densityProcess ν n a x s) -
                  MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s)
                    (ProbabilityTheory.countableFiltration γ) (ν a))
                1 ((ν a).restrict A))
            Filter.atTop (nhds 0)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m γ}
  (it : Std.IterM Id β), (Std.IterM.mapM f it).toList = List.mapM f it.toList.run
-- Mathlib.Algebra.Group.Units.Defs
/-- For `a, b` in a Dedekind-finite additive monoid such that `a + b = 0`,
makes an addUnit out of `a`.  -/
AddUnits.mkOfAddEqZero : {α : Type u} → [inst : AddMonoid α] → [IsDedekindFiniteAddMonoid α] → (a b : α) → a + b = 0 → AddUnits α
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t₁ t₂ : Finset β},
  s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.forget₂Group_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.trans_sOppSide : ∀ {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.SSameSide x y → s.SOppSide y z → s.SOppSide x z
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.instIsLeftAdjointReflector : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.Reflective i], (CategoryTheory.reflector i).IsLeftAdjoint