mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_d_ne_zero' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], d ≠ 0 → { a := 0, b := 0, c := 0, d := d }.toPoly.degree = 0
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- Uniformizers exist in a DVR.  -/
IsDiscreteValuationRing.exists_prime : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], ∃ ϖ, Prime ϖ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Closure of a subsemiring `S` equals `S`.  -/
Subsemiring.closure_eq : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), Subsemiring.closure ↑s = s
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.subtype_apply : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubsemiringClass S R] {s : S} (x : ↥s), (NonUnitalSubsemiringClass.subtype s) x = ↑x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
CategoryTheory.Abelian.Ext.subsingleton_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (P Y : C) [CategoryTheory.Projective P] (n : ℕ),
  Subsingleton (CategoryTheory.Abelian.Ext P Y (n + 1))
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_div : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Div α] (x y : Shrink.{v, u_2} α),
  (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_inf : ∀ {R : Type u_2} [inst : NonAssocRing R] (S₁ S₂ : Subring R), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafification_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q), (J.sheafification D).map η = J.sheafifyMap η
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.Mor₁) →
    ((t : Mathlib.Tactic.BicategoryLike.Mor₁) → Mathlib.Tactic.BicategoryLike.Mor₁.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.Mor₁.below t
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The isomorphism `opZ^n(f, 𝟙 _) ≅ H^n(f)`.  -/
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i₀ i₁ : ι} →
              (f : i₀ ⟶ i₁) →
                (n₀ n₁ : ℤ) →
                  autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIsoH._auto_1 →
                    (X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁ ≅
                      (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_sup : ∀ {M : Type u_2} [inst : Add M] (S₁ S₂ : AddSubsemigroup M), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} (c : M), a ≡ b [PMOD p] → c + a ≡ c + b [PMOD p]
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [hJ : J.HasSheafCompose (CategoryTheory.forget A)] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G)
      [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A],
      J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.seminormedAddGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)],
  Pi.seminormedAddGroup =
    { norm := fun f => ↑(Finset.univ.sup fun b => ‖f b‖₊), toAddGroup := Pi.addGroup,
      toPseudoMetricSpace := pseudoMetricSpacePi, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_epi_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {h : Y ⟶ Y},
  CategoryTheory.CategoryStruct.comp f h = f ↔ h = CategoryTheory.CategoryStruct.id Y
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_i_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.symm.i h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i) h
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.meas_le_lintegral₀ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∀ {s : Set α}, (∀ x ∈ s, 1 ≤ f x) → μ s ≤ ∫⁻ (a : α), f a ∂μ
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.foldl_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {fallback : β a},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getValueCastD a l fallback = Std.Internal.List.getValueCastD a l' fallback
-- Mathlib.Data.Multiset.ZeroCons
Multiset.pmap_zero : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (h : ∀ a ∈ 0, p a), Multiset.pmap f 0 h = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 3], W.b₂ = 0 → W.j = 0
-- Lean.Elab.PreDefinition.Basic
/-- Adds the docstring, if relevant.

This should be done just after compilation so the predefinition can be executed in examples in its
docstring. If code generation will not occur, then it should be done after adding the declaration
to the environment.
 -/
Lean.Elab.addPreDefDocs : Lean.LocalContext × Lean.LocalInstances → Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The `stalkToFiber` map is surjective at `x` if
every point in the fiber `T x` has an allowed section passing through it.
 -/
TopCat.stalkToFiber_surjective : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T) (x : ↑X),
  (∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t) →
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.stalkToFiber P x))
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coeFn_mk : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsFiniteMeasure μ),
  ⇑⟨μ, hμ⟩ = fun s => (μ s).toNNReal
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.mem_eqLocusField : ∀ {K : Type u} [inst : DivisionRing K] {L : Type v} [inst_1 : Semiring L] {f g : K →+* L} {x : K},
  x ∈ f.eqLocusField g ↔ f x = g x
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `H^n(f₁) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃) ⟶ 0`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ : ι} →
              (f₁ : i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (i₂ ⟶ i₃) →
                    (f₁₂ : i₀ ⟶ i₂) →
                      CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
                        (n₀ n₁ n₂ : ℤ) →
                          autoParam (n₀ + 1 = n₁)
                              CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1 →
                            autoParam (n₁ + 1 = n₂)
                                CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3 →
                              CategoryTheory.ShortComplex C
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure of a polynomial is the absolute value of its leading coefficient times
the product of the absolute values of its roots lying outside the unit disk.  -/
Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots : ∀ (p : Polynomial ℂ), p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.sproj.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (n offset : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11),
  sizeOf (Lean.Compiler.LCNF.LetValue.sproj n offset var h) = 1 + sizeOf n + sizeOf offset + sizeOf var + sizeOf h
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The constructor for W-types  -/
PFunctor.W.mk : {P : PFunctor.{uA, uB}} → ↑P P.W → P.W
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_pos : ∀ {c : Cardinal.{u}}, 0 < Cardinal.toNat c ↔ c ≠ 0 ∧ c < Cardinal.aleph0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instAddLeftMono : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] [AddLeftMono M] [inst_4 : ContinuousAdd M], AddLeftMono (MeasureTheory.VectorMeasure α M)
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.abs_det_basis_change : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K] [inst_8 : Algebra ℚ K] [IsDomain K]
  {ι : Type u_3} [inst_10 : Fintype ι] [inst_11 : DecidableEq ι] (b : Module.Basis ι ℤ R)
  (I : FractionalIdeal (nonZeroDivisors R) K) (bI : Module.Basis ι ℤ ↥↑I),
  |(Module.Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K b).det (Subtype.val ∘ ⇑bI)| =
    FractionalIdeal.absNorm I
-- Init.Data.UInt.Lemmas
UInt16.lt_iff_toFin_lt : ∀ {a b : UInt16}, a < b ↔ a.toFin < b.toFin
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.add_inv_add_mul_eq_zero : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ),
  (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0
-- Lean.Data.Position
Lean.FileMap.mk.sizeOf_spec : ∀ (source : String) (positions : Array String.Pos.Raw),
  sizeOf { source := source, positions := positions } = 1 + sizeOf source + sizeOf positions
-- Lean.DocString.Types
Lean.Doc.Inline.other.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (container : i) (content : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Inline.other container content) = 1 + sizeOf container + sizeOf content
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_3.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_4 t (Lean.Elab.Term.Do.Code.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the
adjunction to an equivalence.
 -/
CategoryTheory.Adjunction.toEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] →
                [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] → C ≌ D
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt.info : Lean.Elab.Tactic.ElimApp.Alt → Lean.Meta.ElimAltInfo
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.le_saturation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid}, s ≤ s.saturation M H
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- **Alias** of the forward direction of `SimpleGraph.Subgraph.isSpanning_iff`. -/
SimpleGraph.Subgraph.IsSpanning.verts_eq_univ : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.IsSpanning → G'.verts = Set.univ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
  (nodup : [l].Nodup) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val)),
  (match some { clause := [l], nodupkey := nodupkey, nodup := nodup } with
    | none => h_1 ()
    | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
    | some val => h_3 val) =
    h_2 l nodupkey nodup
-- Aesop.EMap
Aesop.EMap.instEmptyCollection : {α : Type u_1} → EmptyCollection (Aesop.EMap α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_5.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1) (val : Bool)
  (h_1 : (var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var))
  (h_2 : (val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val))
  (h_3 : (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not)
  (h_4 : (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs))
  (h_5 :
    (g : Std.Tactic.BVDecide.Gate) →
      (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
        motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)),
  (match Std.Tactic.BVDecide.BoolExpr.const val with
    | Std.Tactic.BVDecide.BoolExpr.literal var => h_1 var
    | Std.Tactic.BVDecide.BoolExpr.const val => h_2 val
    | expr.not => h_3 expr
    | discr.ite lhs rhs => h_4 discr lhs rhs
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs => h_5 g lhs rhs) =
    h_2 val
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ioo : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {a b : R},
  f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - ↑f a)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instRatCast : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → RatCast (CauSeq.Completion.Cauchy abv)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryMidLinearEquiv_apply : ∀ (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂),
  (MultilinearMap.curryMidLinearEquiv R M M₂ p) f = MultilinearMap.curryMid p f
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.mk.sizeOf_spec : ∀ (expr type : Lean.Expr) (modified : Bool),
  sizeOf { expr := expr, type := type, modified := modified } = 1 + sizeOf expr + sizeOf type + sizeOf modified
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Reinterpreting an `F`-costructured arrow `F.obj d ⟶ X` as an arrow over `X` induces a functor
`CostructuredArrow F X ⥤ Over X`.  -/
CategoryTheory.CostructuredArrow.toOver : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          (X : T) → CategoryTheory.Functor (CategoryTheory.CostructuredArrow F X) (CategoryTheory.Over X)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- `LevyProkhorov.toMeasure` as an equiv.  -/
MeasureTheory.LevyProkhorov.toMeasureEquiv : {α : Type u_2} → MeasureTheory.LevyProkhorov α ≃ α
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_functor_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t₁ t₂ : CategoryTheory.Limits.Cocone K}
  (f : t₁ ⟶ t₂), (CategoryTheory.WithInitial.coconeEquiv.functor.map f).hom = CategoryTheory.Under.Hom.right f.hom
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_distrib_right : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a b c : α), a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_map_comp : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15}
  {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : AddCommMonoid N₂]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂)
  (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂),
  ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂ ∘ₗ f₁₂) f₃ =
    TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {s : Set M} {x : M} {g : M → G},
  ContMDiffWithinAt I' I n g s x → ∀ (m : ℕ), ContMDiffWithinAt I' I n (fun x => g x ^ m) s x
-- Mathlib.Data.Finsupp.Basic
Int.cast_finsuppProd : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : CommRing R] (g : α → M → ℤ),
  ↑(f.prod g) = f.prod fun a b => ↑(g a b)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapAlgHom_residue : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : CommRing T] [inst_4 : IsLocalRing T] [inst_5 : Algebra R S] [inst_6 : Algebra R T] (e : S →ₐ[R] T)
  [inst_7 : IsLocalHom e] (x : S),
  (IsLocalRing.ResidueField.mapAlgHom e) ((IsLocalRing.residue S) x) = (IsLocalRing.residue T) (e x)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.instDecidablePartialMatch : {pat s : ByteArray} →
  {needlePos stackPos : ℕ} →
    Decidable (String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.lintegralPowLePowLIntegralFDerivConst.congr_simp : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1)
  [inst_5 : μ.IsAddHaarMeasure] (p p_1 : ℝ),
  p = p_1 →
    MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p =
      MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ_1 p_1
-- Mathlib.Algebra.Group.Basic
sub_eq_iff_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - b = c ↔ a = c + b
-- Mathlib.Data.Seq.Computation
Computation.Results.len_unique : ∀ {α : Type u} {s : Computation α} {a b : α} {m n : ℕ}, s.Results a m → s.Results b n → m = n
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.mk.injEq : ∀ (ns ns_1 : Array Aesop.RuleSetName), ({ ns := ns } = { ns := ns_1 }) = (ns = ns_1)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Std.Async.Basic
Std.Async.EAsync.instMonadExcept : {ε : Type} → MonadExcept ε (Std.Async.EAsync ε)
-- Mathlib.Algebra.Module.PUnit
PUnit.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} [inst : SMul R S], IsScalarTower PUnit.{u_3 + 1} R S
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionCont : Type