mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.const_smul : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : SMul γ β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), c • f =ᶠ[l] c • g
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.isPushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A}
  (self : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂), CategoryTheory.IsPushout p₁ p₂ self.π self.π
-- Init.System.IO
IO.FS.Mode.read.sizeOf_spec : sizeOf IO.FS.Mode.read = 1
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.isColimitWhiskerEquiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.Cocone G),
  CategoryTheory.Functor.Final.isColimitWhiskerEquiv F t = CategoryTheory.Functor.Final.isColimitWhiskerEquiv F t
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.replayKernel : Lean.Environment.RealizeConstResult✝ →
  Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isAddUnit_iff_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {s : Set α}, IsAddUnit s ↔ ∃ a, s = {a}
-- Mathlib.Data.Sign.Defs
SignType.instZero : Zero SignType
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.clm_postcomp : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {s : Set M},
  MDiff[s] f → MDiff[s] fun y => ContinuousLinearMap.postcomp F₁ (f y)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_34 : HAdd Std.Time.Day.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.logPatternWhen : Bool → Lean.Meta.Grind.Origin → List Lean.Expr → Lean.MetaM Unit
-- Mathlib.Data.Finsupp.Interval
/-- Pointwise `Singleton.singleton` bundled as a `Finsupp`.  -/
Finsupp.rangeSingleton : {ι : Type u_1} → {α : Type u_2} → [inst : Zero α] → (ι →₀ α) → ι →₀ Finset α
-- Mathlib.Analysis.Calculus.MeanValue
/-- Variant of the mean value inequality on a convex set. Version with `fderiv`.  -/
Convex.norm_image_sub_le_of_norm_fderiv_le' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {φ : E →L[𝕜] G},
  (∀ x ∈ s, DifferentiableAt 𝕜 f x) →
    (∀ x ∈ s, ‖fderiv 𝕜 f x - φ‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
-- Init.SizeOf
instSizeOfNat : SizeOf ℕ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isParabolic_iff_of_upperTriangular : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R} [IsReduced R],
  m 1 0 = 0 → (m.IsParabolic ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
-- Init.Data.String.Modify
String.set : String → String.Pos.Raw → Char → String
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousVAdd : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace R] [inst_3 : VAdd R M] [inst_4 : ContinuousVAdd R M], ContinuousVAdd R C(α, M)
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticOn.zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOn 𝕜 f s → (∀ z ∈ s, f z ≠ 0) → AnalyticOn 𝕜 (f ^ n) s
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.index.congr_simp : ∀ {X : SSet} {x x_1 : X.S} (e_x : x = x_1) {y y_1 : X.S} (e_y : y = y_1) (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ}
  (hd : x.dim = d), hxy.index hd = ⋯.index ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.csSup_eq_max' : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty), sSup ↑s = s.max' h
-- Mathlib.Topology.Algebra.Group.Basic
Topology.IsInducing.topologicalAddGroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {F : Type u_1}
  [inst_3 : AddGroup H] [inst_4 : TopologicalSpace H] [inst_5 : FunLike F H G] [AddMonoidHomClass F H G] (f : F),
  Topology.IsInducing ⇑f → IsTopologicalAddGroup H
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.contentModified.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.contentModified = 1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.induction : ∀ {α : Type u_1} {p : Multiset α → Prop},
  p 0 → (∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) → ∀ (s : Multiset α), p s
-- Init.Data.UInt.Lemmas
USize.lt_iff_toFin_lt : ∀ {a b : USize}, a < b ↔ a.toFin < b.toFin
-- Mathlib.Topology.ContinuousOn
Set.MapsTo.closure_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, Set.MapsTo f s t → (∀ x ∈ closure s, ContinuousWithinAt f s x) → Set.MapsTo f (closure s) (closure t)
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_ric : ∀ {α : Type u_1} {xs : List α} {hi : ℕ}, Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) xs
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.match_1.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (pw₁ : Lean.Grind.CommRing.Power) (m₁_1 : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
  (m₂_1 : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.mult pw₁ m₁_1 →
    m₂ = Lean.Grind.CommRing.Mon.mult pw₂ m₂_1 →
      (match m₁, m₂ with
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
        | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) ≍
        h_4 pw₁ m₁_1 pw₂ m₂_1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_preNormEDS : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ), f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The given element `t` of `P.obj (op X)` is an *amalgamation* for the family of elements `x` if every
restriction `P.map f.op t = x_f` for every arrow `f` in the presieve `R`.

This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents,
and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4,
equation (2).
 -/
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} → CategoryTheory.Presieve.FamilyOfElements P R → P.obj (Opposite.op X) → Prop
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapIso_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y),
  (CategoryTheory.Over.mapIso f).functor = CategoryTheory.Over.map f.hom
-- Mathlib.Data.LawfulXor.Equiv
Equiv.isFixedPt_xor : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] {a b : α},
  Function.IsFixedPt (⇑(Equiv.xor a)) b ↔ a = 0
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_union_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, μ s = 0 → μ t = 0 → μ (s ∪ t) = 0
-- Mathlib.Algebra.Order.Ring.NNRat
NNRat.instOrderedSub : OrderedSub ℚ≥0
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instTopologicalSpace : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → TopologicalSpace (A →ₜ* B)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_pos_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x ≠ 0#w → 0 < x.toNat
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddCommClass_finset' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddCommClass α β γ], VAddCommClass α (Finset β) (Finset γ)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_singleton_iff : ∀ {k n : ℕ}, (*...n).toList = [k] ↔ n = 1 ∧ 0 = k
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.comap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] {μ : MeasureTheory.Measure β} [μ.InnerRegular]
  (f : α ≃ₜ β), (MeasureTheory.Measure.comap (⇑f) μ).InnerRegular
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.ofIsoI_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.ImageFactorisation f) {I' : C} (e : F.F.I ≅ I'), (F.ofIsoI e).F = F.F.ofIsoI e
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.widePushoutShape_connected : ∀ (J : Type v₁), CategoryTheory.IsConnected (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
/-- The binary product of probability measures.  -/
MeasureTheory.ProbabilityMeasure.prod : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    {β : Type u_2} →
      [inst_1 : MeasurableSpace β] →
        MeasureTheory.ProbabilityMeasure α →
          MeasureTheory.ProbabilityMeasure β → MeasureTheory.ProbabilityMeasure (α × β)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_appTop : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.appTop U.ι = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
/-- A functor preserves injective objects if it maps injective objects to injective objects.  -/
CategoryTheory.Functor.PreservesInjectiveObjects : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.instCategory : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → CategoryTheory.Category.{v_1, max u_1 v_2} (Φ.LeftResolution X₂)
-- Mathlib.Algebra.Group.Nat.Even
Nat.instDecidablePredEven : DecidablePred Even
-- Std.Async.Basic
/-- Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
`AsyncTask` resolves to that error.
 -/
Std.Async.AsyncTask.bindIO : {α β : Type} →
  Std.Async.AsyncTask α →
    (α → IO (Std.Async.AsyncTask β)) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Std.Async.AsyncTask β)
-- Std.Internal.UV.Signal
/-- This creates a `Signal` in the initial state and doesn't start listening yet.
- If `repeating` is `false` this constructs a signal handler that resolves once when the specified
  signal `signum` is received, then automatically stops listening.
- If `repeating` is `true` this constructs a signal handler that resolves each time the specified
  signal `signum` is received and continues listening. A repeating signal handler will only be
  freed after `Signal.stop` is called.
 -/
Std.Internal.UV.Signal.mk : Int32 → Bool → IO Std.Internal.UV.Signal
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
pos_iff_neg_of_mul_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], a * b < 0 → (0 < a ↔ b < 0)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.meas_biInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)},
  ProbabilityTheory.Kernel.iIndepSets π κ μ →
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
-- Init.Data.BitVec.Lemmas
BitVec.mul_comm : ∀ {w : ℕ} (x y : BitVec w), x * y = y * x
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.congr_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M ≃ₗ[R] N) (x : AdicCompletion I N),
  (AdicCompletion.congr I f).symm x = (AdicCompletion.map I ↑f.symm) x
-- Mathlib.Algebra.Field.Rat
NNRat.instInv : Inv ℚ≥0
-- Mathlib.Dynamics.Flow
/-- Convert a flow to an additive monoid action.  -/
Flow.toAddAction : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddMonoid τ] → Flow τ α → AddAction τ α
-- Mathlib.Order.Filter.Lift
Filter.lift_iInf_of_map_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → Filter α} {g : Set α → Filter β},
  (∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t) → g Set.univ = ⊤ → (iInf f).lift g = ⨅ i, (f i).lift g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Mathlib.Order.OrderDual
OrderDual.Preorder.dual_dual : ∀ (α : Type u_2) [H : Preorder α], OrderDual.instPreorder αᵒᵈ = H
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_le_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsZeroOrMarkovKernel κ], κ.bound ≤ 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.BinaryRefVec w → Sort u_1) (lhs rhs : aig.RefVec w)
  (h_1 : (lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }),
  (match { lhs := lhs, rhs := rhs } with
    | { lhs := lhs, rhs := rhs } => h_1 lhs rhs) =
    h_1 lhs rhs
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.re_complexMGF_ofReal' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  (fun x => (ProbabilityTheory.complexMGF X μ ↑x).re) = ProbabilityTheory.mgf X μ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_cons₂ : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp k.cons₂ =
    Turing.PartrecToTM2.trStmts₁
        (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
      Turing.PartrecToTM2.contSupp k
-- Mathlib.Analysis.SpecificLimits.Normed
summable_pow_mul_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R},
  ‖r‖ < 1 → Summable fun n => ↑n ^ k * r ^ n
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
/-- The weight 2 Eisenstein series `E2` is MDifferentiable  -/
E2_mdifferentiable : MDiff EisensteinSeries.E2
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.isoMk_inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S}
  (Φ : (HasFibers.ι S).obj a ≅ (HasFibers.ι S).obj b) (hΦ : p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom),
  (HasFibers.Fib.isoMk Φ hΦ).inv = HasFibers.Fib.homMk Φ.inv
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.filter_of_true : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop},
  (∀ J ∈ π, p J) → π.filter p = π
-- Init.Grind.Interactive
/-- Performs the next case-split. The case-split is selected using the same heuristic used by `finish`.
 -/
Lean.Parser.Tactic.Grind.casesNext : Lean.ParserDescr
-- Mathlib.Computability.Language
Language.iSup_mul : ∀ {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α), (⨆ i, l i) * m = ⨆ i, l i * m
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_zero : ∀ {ι : Type u_1} (R : Type u_5) [inst : Zero R] [inst_1 : One R] [NeZero 1], Function.mulSupport 0 = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (G :
    CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)),
  ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_X_of_ne : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {i j : σ} (f : MvPolynomial σ R),
  i ≠ j → MvPolynomial.degreeOf i (f * MvPolynomial.X j) = MvPolynomial.degreeOf i f
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablySeparated.subtype_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α},
  MeasurableSpace.CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s
-- Mathlib.Data.Num.Bitwise
/-- The successor of a `SNum` (i.e. the operation adding one).  -/
SNum.succ : SNum → SNum
-- Mathlib.Data.ENNReal.Holder
ENNReal.holderTriple_iff : ∀ (p q : ENNReal) (r : semiOutParam ENNReal), p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFullCompPreLeft : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [F.Full], (CategoryTheory.Comma.preLeft F L R).Full
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : ModuleCat.of k ↑B ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) h)
-- Batteries.Classes.RatCast
/-- Type class for the canonical homomorphism `Rat → K`.  -/
RatCast : Type u → Type u
-- Lean.Server.AsyncList
Lean.AsyncList.nil : {ε : Type u} → {α : Type v} → Lean.AsyncList ε α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.ChosenPullbacksAlong.fst Y.hom (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id Y.left
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.foldlIdx.match_1.eq_2 : ∀ {β : Type u_1} (motive : List β → ℕ → Sort u_2) (b : β) (l : List β) (s : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (b : β) → (l : List β) → (s : ℕ) → motive (b :: l) s),
  (match b :: l, s with
    | [], x => h_1 x
    | b :: l, s => h_2 b l s) =
    h_2 b l s
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_neg : ∀ {R' : Type u_2} [inst : Ring R'] (f' : PowerSeries R'),
  (HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_int16ToInt : ∀ (x : Int16) {h₁ : Int8.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int8.maxValue.toInt},
  Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_empty : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R], MvPolynomial.supported R ∅ = ⊥
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.needsNoEscape : (s : String) → s.utf8ByteSize > 0 → Bool
-- Mathlib.Topology.MetricSpace.Cover
/-- A totally bounded set has finite `ε`-covers for all `ε > 0`.  -/
Metric.exists_finite_isCover_of_totallyBounded : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X},
  ε ≠ 0 → TotallyBounded s → ∃ N ⊆ s, N.Finite ∧ Metric.IsCover ε s N
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.parallelepiped_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E) (e : ι ≃ ι'), (b.reindex e).parallelepiped = b.parallelepiped
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd