mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the right: This is the isomorphism
`∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ X i)
      (q₂ : (i : ι) → P i ⟶ B),
      (∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) (f i) v) →
        ∀ {Z : C} {p₁ : Z ⟶ a.pt} {p₂ : Z ⟶ B},
          CategoryTheory.IsPullback p₁ p₂ u v →
            ∀ (d : CategoryTheory.Limits.Cofan P) (e : d.pt ≅ Z),
              autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                  CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right._auto_1 →
                autoParam
                    (∀ (i : ι),
                      CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₁) =
                        CategoryTheory.CategoryStruct.comp (q₁ i) (a.inj i))
                    CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right._auto_3 →
                  autoParam
                      (∀ (i : ι),
                        CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₂) =
                          q₂ i)
                      CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right._auto_5 →
                    Nonempty (CategoryTheory.Limits.IsColimit d)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackSymmetry
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
            ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j) ≪≫
          CategoryTheory.Limits.pullbackRightPullbackFstIso (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)
            ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j)).hom
      (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsRadical.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), I.IsRadical = (I.radical ≤ I)
-- Mathlib.RingTheory.LocalProperties.Semilocal
Module.Finite.of_localized_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M],
  (∀ (P : Ideal R) [inst_4 : P.IsMaximal], Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl M)) →
    Module.Finite R M
-- Mathlib.Data.Set.Prod
Equiv.piCongrLeft_preimage_pi : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (s : Set ι') (t : (i : ι) → Set (α i)),
  ⇑(Equiv.piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i => t (f i)
-- Mathlib.Tactic.FindSyntax
/-- `extractSymbols descr acc` takes as input a `ParserDescr`iptor `descr` and an accumulator array
`acc`. It accumulates all symbols in `descr` corresponding to `Lean.ParserDescr.symbol`,
`Lean.ParserDescr.nonReservedSymbol` or `Lean.ParserDescr.unicodeSymbol`.

The output array serves as a way of regenerating what the syntax tree of the input parser is.
 -/
Mathlib.FindSyntax.extractSymbols : Lean.ParserDescr → Array String → Array String
-- Mathlib.Data.Vector.Snoc
List.Vector.mapAccumr_nil : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {f : α → σ → σ × β} {s : σ},
  List.Vector.mapAccumr f List.Vector.nil s = (s, List.Vector.nil)
-- Mathlib.Algebra.Category.Grp.Adjunctions
CommMonCat.units_obj_coe : ∀ (R : CommMonCat), ↑(CommMonCat.units.obj R) = (↑R)ˣ
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also `ContinuousLinearEquiv.arrowCongr`.  -/
ContinuousLinearEquiv.arrowCongrEquiv : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : Semiring R₁] →
        [inst_1 : Semiring R₂] →
          [inst_2 : Semiring R₃] →
            {σ₁₂ : R₁ →+* R₂} →
              {σ₂₁ : R₂ →+* R₁} →
                [inst_3 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_4 : RingHomInvPair σ₂₁ σ₁₂] →
                    {σ₂₃ : R₂ →+* R₃} →
                      {σ₁₃ : R₁ →+* R₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          {M₁ : Type u_4} →
                            [inst_6 : TopologicalSpace M₁] →
                              [inst_7 : AddCommMonoid M₁] →
                                {M₂ : Type u_5} →
                                  [inst_8 : TopologicalSpace M₂] →
                                    [inst_9 : AddCommMonoid M₂] →
                                      {M₃ : Type u_6} →
                                        [inst_10 : TopologicalSpace M₃] →
                                          [inst_11 : AddCommMonoid M₃] →
                                            {M₄ : Type u_7} →
                                              [inst_12 : TopologicalSpace M₄] →
                                                [inst_13 : AddCommMonoid M₄] →
                                                  [inst_14 : Module R₁ M₁] →
                                                    [inst_15 : Module R₂ M₂] →
                                                      [inst_16 : Module R₃ M₃] →
                                                        {R₄ : Type u_8} →
                                                          [inst_17 : Semiring R₄] →
                                                            [inst_18 : Module R₄ M₄] →
                                                              {σ₃₄ : R₃ →+* R₄} →
                                                                {σ₄₃ : R₄ →+* R₃} →
                                                                  [inst_19 : RingHomInvPair σ₃₄ σ₄₃] →
                                                                    [inst_20 : RingHomInvPair σ₄₃ σ₃₄] →
                                                                      {σ₂₄ : R₂ →+* R₄} →
                                                                        {σ₁₄ : R₁ →+* R₄} →
                                                                          [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] →
                                                                            [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] →
                                                                              [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] →
                                                                                (M₁ ≃SL[σ₁₂] M₂) →
                                                                                  (M₄ ≃SL[σ₄₃] M₃) →
                                                                                    (M₁ →SL[σ₁₄] M₄) ≃ (M₂ →SL[σ₂₃] M₃)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.eq_1 : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal),
  MeasureTheory.OuterMeasure.mkMetric' m = ⨆ r, ⨆ (_ : r > 0), MeasureTheory.OuterMeasure.mkMetric'.pre m r
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.prod_swap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
  [inst : TopologicalSpace γ] {f : β × α → γ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun z => f z.swap
-- Mathlib.Analysis.Normed.Group.Uniform
NormedGroup.to_isIsometricSMul : ∀ {E : Type u_2} [inst : SeminormedGroup E], IsIsometricSMul E E
-- Mathlib.Analysis.Calculus.FDeriv.Norm
ContDiffAt.contDiffAt_norm_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ},
  t ≠ 0 → ContDiffAt ℝ n (fun x => ‖x‖) x → ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
-- Init.Data.List.Lemmas
List.eraseDups.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (as : List α), as.eraseDups = List.eraseDupsBy (fun x1 x2 => x1 == x2) as
-- Mathlib.Algebra.Tropical.Basic
/-- Reinterpret `x : R` as an element of `Tropical R`.
See `Tropical.tropEquiv` for the equivalence.
 -/
Tropical.trop : {R : Type u} → R → Tropical R
-- Mathlib.Data.Sym.Basic
/-- This is the quotient map that takes a list of n elements as an n-tuple and produces an nth
symmetric power.
 -/
Sym.instCoeVector : {α : Type u_1} → {n : ℕ} → Coe (List.Vector α n) (Sym α n)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Right component of the associator as a natural isomorphism.  -/
CategoryTheory.Bicategory.associatorNatIsoRight : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (d : B) →
            (CategoryTheory.Bicategory.precomposing a c d).obj (CategoryTheory.CategoryStruct.comp f g) ≅
              ((CategoryTheory.Bicategory.precomposing b c d).obj g).comp
                ((CategoryTheory.Bicategory.precomposing a b d).obj f)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.map f).hom = f.hom
-- Mathlib.Algebra.Group.Subgroup.Map
/-- the `AddMonoidHom` from the preimage of an
additive subgroup to itself.  -/
AddMonoidHom.addSubgroupComap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup G'] → (f : G →+ G') → (H' : AddSubgroup G') → ↥(AddSubgroup.comap f H') →+ ↥H'
-- Mathlib.Data.Set.Basic
Set.union_eq_self_of_subset_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s ∪ t = s
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_4 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1) (j : ℕ)
  (hj : j + 1 < n + 1 + 1) (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_4 i hi j hj hij
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightStrictMono_of_mulLeftStrictMono : ∀ (N : Type u_2) [inst : CommSemigroup N] [inst_1 : LT N] [MulLeftStrictMono N], MulRightStrictMono N
-- Mathlib.Algebra.Star.Conjneg
/-- `conjneg` bundled as a ring homomorphism.  -/
conjnegRingHom : {G : Type u_2} → {R : Type u_3} → [AddGroup G] → [inst : CommSemiring R] → [StarRing R] → (G → R) →+* G → R
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMap_map_app_app : ∀ {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₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J)
  [inst_4 :
    ∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
      (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁} (φ : X₁ ⟶ Y₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃) (i : J),
  (((CategoryTheory.GradedObject.mapTrifunctorMap F p).map φ).app X₂).app X₃ i =
    CategoryTheory.GradedObject.mapTrifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id X₂)
      (CategoryTheory.CategoryStruct.id X₃) i
-- Mathlib.Data.Finset.Card
Finset.card_le_one_iff : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
-- Mathlib.Order.Max
isTop_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop (OrderDual.toDual a) ↔ IsBot a
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_snd_prod : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {Y : α → Ω} {mβ : MeasurableSpace β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} (X : α → β),
  AEMeasurable Y μ →
    ∀ (ν : MeasureTheory.Measure γ) [inst_4 : MeasureTheory.IsProbabilityMeasure ν],
      ⇑(ProbabilityTheory.condDistrib (fun ω => Y ω.2) (fun ω => X ω.2) (ν.prod μ)) =ᵐ[MeasureTheory.Measure.map X μ]
        ⇑(ProbabilityTheory.condDistrib Y X μ)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ),
  p.take n =
    match v, p, n with
    | .(u), SimpleGraph.Walk.nil, x => SimpleGraph.Walk.nil
    | v, p, 0 => SimpleGraph.Walk.nil.copy ⋯ ⋯
    | v, SimpleGraph.Walk.cons h q, n.succ => SimpleGraph.Walk.cons h (q.take n)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.aleph0_le_cof : ∀ {α : Type u} [inst : LinearOrder α] [Nonempty α] [NoMaxOrder α], Cardinal.aleph0 ≤ Order.cof α
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- A random maximal ideal that contains `spanEval k`  -/
AlgebraicClosure.maxIdeal : (k : Type u) → [inst : Field k] → Ideal (MvPolynomial (AlgebraicClosure.Vars k) k)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, a ∈ t ↔ (t.get? a).isSome = true
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.snd` is continuous at `x : X × Y`  -/
ContinuousAt.snd'' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : Y → Z} {x : X × Y}, ContinuousAt f x.2 → ContinuousAt (fun x => f x.2) x
-- Mathlib.Data.List.Permutation
List.injective_permutations'Aux : ∀ {α : Type u_1} (x : α), Function.Injective (List.permutations'Aux x)
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.edist_zero_of_eq_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → edist (f a) (f b) = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.toList_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.Functor.mapProjectiveResolution_complex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v_1, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject D] [inst_5 : CategoryTheory.Preadditive D]
  [inst_6 : CategoryTheory.CategoryWithHomology D] (F : CategoryTheory.Functor C D) [inst_7 : F.Additive]
  [inst_8 : F.PreservesProjectiveObjects] [inst_9 : F.PreservesHomology] {Z : C}
  (P : CategoryTheory.ProjectiveResolution Z),
  (F.mapProjectiveResolution P).complex = (F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex
-- Init.Grind.Ordered.Linarith
/-- Similar to `Poly.denote`, but produces a denotation better for normalization.
 -/
Lean.Grind.Linarith.Poly.denote' : {α : Type u_1} → [Lean.Grind.IntModule α] → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Poly → α
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging adjacent `intro`-like tactics whose effect is equivalent to a single `intro`.  -/
linter.tacticAnalysis.introMerge : Lean.Option Bool
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_union_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s t : Finset α),
  mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_1 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.notANumber with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_1 ()
-- Init.Data.SInt.Lemmas
Int32.toInt64_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The positive cone is the pointed cone formed by the set of nonnegative elements in an ordered
module.  -/
PointedCone.positive : (R : Type u_1) →
  (E : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : PartialOrder E] →
              [IsOrderedAddMonoid E] → [inst_6 : Module R E] → [PosSMulMono R E] → PointedCone R E
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c : C) {d d' : D}
  (f : d ⟶ d') {Z : D'} (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)) h)
-- Mathlib.Algebra.Group.Defs
/-- A `LeftCancelSemigroup` is a semigroup such that `a * b = a * c` implies `b = c`.  -/
LeftCancelSemigroup : Type u → Type u
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabReduce : Lean.Elab.Command.CommandElab
-- Mathlib.Order.Lattice
inf_right_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ b ⊓ b = a ⊓ b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {fallback : β},
      Std.DHashMap.Raw.Const.getD (m.erase k) a fallback =
        if (k == a) = true then fallback else Std.DHashMap.Raw.Const.getD m a fallback
-- Mathlib.Combinatorics.Colex
Finset.orderIsoColex_symm_apply : ∀ (s : Colex (Finset ℕ)), (RelIso.symm Finset.orderIsoColex) s = Finset.equivBitIndices.symm (ofColex s)
-- Mathlib.GroupTheory.IsSubnormal
/-- A proper subnormal additive subgroup is contained in a proper normal additive
subgroup.  -/
AddSubgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.IsSubnormal → H ≠ ⊤ → ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
-- Lean.Elab.Tactic.Grind.Basic
/-- Return the first goal.  -/
Lean.Elab.Tactic.Grind.getMainGoal : Lean.Elab.Tactic.Grind.GrindTacticM Lean.Meta.Grind.Goal
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.ofPow : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] {i : ι} (a : A i) (n : ℕ),
  (DirectSum.of A i) a ^ n = (DirectSum.of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_self : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), i.cycleRange i = 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSolverExtension.default : {σ : Type} → Lean.Meta.Grind.SolverExtension σ
-- Mathlib.Data.Finset.Option
/-- Given `s : Finset (Option α)`, `eraseNone s : Finset α` is the set of `x : α` such that
`some x ∈ s`.  -/
Finset.eraseNone : {α : Type u_1} → Finset (Option α) →o Finset α
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The inf of two subfields is their intersection.  -/
Subfield.instMin : {K : Type u} → [inst : DivisionRing K] → Min (Subfield K)
-- Mathlib.Data.Stream.Init
Stream'.iterate_id : ∀ {α : Type u} (a : α), Stream'.iterate id a = Stream'.const a
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- In a real normed space, the image of the unit closed ball under multiplication by a nonnegative
number `r` is the closed ball of radius `r` with center at the origin.  -/
smul_unitClosedBall_of_nonneg : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 ≤ r → r • Metric.closedBall 0 1 = Metric.closedBall 0 r
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.Functor.mapShortComplex.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_4 : F.PreservesZeroMorphisms], F.mapShortComplex = F_1.mapShortComplex
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.ne_zero : ∀ {p q r : ℝ}, p.HolderTriple q r → p ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.braided_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {F : CategoryTheory.Functor C D} [self : F.LaxBraided] (X Y : C) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (CategoryTheory.CategoryStruct.comp (F.map (β_ X Y).hom) h) =
    CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y X) h)