mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.IsNatPowT.bit0 : ∀ {a b c : ℕ}, Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.one_le_inv`. -/
Units.le_of_one_le_inv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), 1 ≤ ↑u⁻¹ → ↑u ≤ 1
-- Mathlib.Data.Nat.Bits
Nat.bit_false_zero : Nat.bit false 0 = 0
-- Init.System.IO
/-- Runs a process to completion, blocking until it terminates.
The child process is run with a null standard input or the specified input if provided,
If the child process terminates successfully with exit code 0, its standard output is returned.
An exception is thrown if it terminates with any other exit code.

The specifications of standard input, output, and error handles in `args` are ignored.
 -/
IO.Process.run : IO.Process.SpawnArgs → optParam (Option String) none → IO String
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableOn.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableOn 𝕜 φ s → DifferentiableOn 𝕜 φs s → DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x)) s
-- Mathlib.Data.Sym.Sym2
Sym2.other_invol' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Sym2.Mem.other' ha ∈ z),
  Sym2.Mem.other' hb = a
-- Lean.ExtraModUses
Lean.instHashableExtraModUse : Hashable Lean.ExtraModUse
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diagonal` as a `LinearMap`.  -/
Matrix.diagonalLinearMap : (n : Type u_3) →
  (R : Type u_7) →
    (α : Type u_11) →
      [DecidableEq n] →
        [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → (n → α) →ₗ[R] Matrix n n α
-- Mathlib.SetTheory.Cardinal.Aleph
/-- **Alias** of `Cardinal.preAleph_natCast`. -/
Cardinal.preAleph_nat : ∀ (n : ℕ), Cardinal.preAleph ↑n = ↑n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates.0.Tactic.ComputeAsymptotics.UnitMonomial.sign.match_1.splitter : (motive : Tactic.ComputeAsymptotics.UnitMonomial → Sort u_1) →
  (x : Tactic.ComputeAsymptotics.UnitMonomial) →
    (Unit → motive []) → ((hd : ℝ) → (tl : List ℝ) → motive (hd :: tl)) → motive x
-- Batteries.Data.Fin.Coding
Fin.encodeQuotient.eq_1 : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Quotient s),
  Fin.encodeQuotient s x = Fin.encodeSubtype (fun i => Fin.getRepr s i = i) (x.liftOn (fun i => ⟨Fin.getRepr s i, ⋯⟩) ⋯)
-- Mathlib.Computability.NFA
NFA.eval_append_singleton : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (x : List α) (a : α), M.eval (x ++ [a]) = M.stepSet (M.eval x) a
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a `SubNegMonoid` if `β` is a `SubNegMonoid`.  -/
FunLike.subNegMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : SubNegMonoid β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → SubNegMonoid F
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProbaEquiv.eq_1 : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X],
  MeasureTheory.diracProbaEquiv =
    { toFun := fun x => ⟨MeasureTheory.diracProba x, ⋯⟩, invFun := MeasureTheory.diracProbaInverse, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_smul : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {S : Type u_1} [inst_1 : Monoid S] [inst_2 : DistribMulAction S ↑N]
  [inst_3 : SMulCommClass R S ↑N] (s : S) (f : M ⟶ N), ModuleCat.Hom.hom (s • f) = s • ModuleCat.Hom.hom f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.const_add : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Add β]
  [ContinuousAdd β], MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => c + f x
-- Mathlib.Analysis.Analytic.Basic
/-- The radius of convergence is positive  -/
HasFPowerSeriesWithinOnBall.r_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal}, HasFPowerSeriesWithinOnBall f p s x r → 0 < r
-- Mathlib.Topology.Separation.Basic
/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets.  -/
IsCompact.binary_compact_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K U V : Set X},
  IsCompact K → IsOpen U → IsOpen V → K ⊆ U ∪ V → ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
-- Mathlib.Topology.DiscreteQuotient
/-- The quotient by `⊤ : DiscreteQuotient X` is a `Subsingleton`.  -/
DiscreteQuotient.instSubsingletonQuotientTop : ∀ {X : Type u_2} [inst : TopologicalSpace X], Subsingleton (Quotient ⊤.toSetoid)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.source_inter_preimage_inv_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set X), e.source ∩ ↑e ⁻¹' ↑e.symm ⁻¹' s = e.source ∩ s
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentData f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι),
  (CategoryTheory.CategoryStruct.comp φ φ').hom i = CategoryTheory.CategoryStruct.comp (φ.hom i) (φ'.hom i)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_of_pos : ∀ {x : ℝ} (hx : 0 < x), Real.log x = Real.expOrderIso.symm ⟨x, hx⟩
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.instTopologicalSpaceFiniteAdeleRing : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] → TopologicalSpace (IsDedekindDomain.FiniteAdeleRing R K)
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, sep, ...as]` is split on `p`, the first element is `xs`,
assuming no element in `xs` satisfies `p` but `sep` does satisfy `p`  -/
List.splitOnP_append_cons_of_forall_mem : ∀ {α : Type u_1} {p : α → Bool} {xs : List α},
  (∀ x ∈ xs, p x = false) →
    ∀ (sep : α), p sep = true → ∀ (as : List α), List.splitOnP p (xs ++ sep :: as) = xs :: List.splitOnP p as
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- By `infer_instance` for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.comap_algEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (p : Ideal S) [inst_5 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p]
  (f : T ≃ₐ[R] S), Algebra.WeaklyQuasiFiniteAt R (Ideal.comap f.toRingEquiv.toRingHom p)
-- Std.Async.Basic
/-- Lifts a `BaseIO` action into a `BaseAsync` computation.
 -/
Std.Async.BaseAsync.lift : {α : Type} → BaseIO α → Std.Async.BaseAsync α
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousOn_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  LowerSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_const : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (b : β),
  ⇑(MeasureTheory.SimpleFunc.const α b) = Function.const α b
-- Mathlib.Data.Real.Pointwise
Real.iInf_mul_of_nonpos : ∀ {ι : Sort u_1} {r : ℝ}, r ≤ 0 → ∀ (f : ι → ℝ), (⨅ i, f i) * r = ⨆ i, f i * r
-- Mathlib.Dynamics.Minimal
eq_empty_or_univ_of_vadd_invariant_closed : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] {s : Set α}, IsClosed s → (∀ (c : M), c +ᵥ s ⊆ s) → s = ∅ ∨ s = Set.univ
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a normal
subgroup `Γ` of an additive topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `AddQuotientMeasureEqMeasurePreimage`.  -/
IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ [μ.IsAddLeftInvariant] [MeasureTheory.SigmaFinite μ] {V : Set (G ⧸ Γ)},
      (interior V).Nonempty →
        MeasurableSet V →
          μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ 𝓕) → μ V ≠ ⊤ → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec_succ_eq : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.sshiftRightRec y (n + 1) = (x.sshiftRightRec y n).sshiftRight' (y &&& BitVec.twoPow w₂ (n + 1))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α}, (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Geometry.Manifold.Immersion
/-- Being an immersion at `x` w.r.t. `F` is stable under replacing `F` by an isomorphic copy.  -/
Manifold.IsImmersionAtOfComplement.congr_F : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F]
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {G : Type u_9} [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {M : Type u_11} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] {N : Type u_13}
  [inst_13 : TopologicalSpace N] [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (e : F ≃L[𝕜] F'),
  Manifold.IsImmersionAtOfComplement F I J n f x ↔ Manifold.IsImmersionAtOfComplement F' I J n f x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_inclusion_apply : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {S₁ S₂ : AffineSubspace k P₁} [inst_4 : Nonempty ↥S₁] (h : S₁ ≤ S₂) (x : ↥S₁),
  ↑((AffineSubspace.inclusion h) x) = ↑x
-- Mathlib.Geometry.Euclidean.Sphere.Power
EuclideanGeometry.Sphere.power.eq_1 : ∀ {P : Type u_2} [inst : MetricSpace P] (s : EuclideanGeometry.Sphere P) (p : P),
  s.power p = dist p s.center ^ 2 - s.radius ^ 2
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- A category `C` has a subobject classifier if there is at least one subobject classifier.  -/
CategoryTheory.HasSubobjectClassifier : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Init.Data.UInt.Lemmas
UInt16.toNat_sub_of_le : ∀ (a b : UInt16), b ≤ a → (a - b).toNat = a.toNat - b.toNat
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instCommRingUInt64 : Lean.Grind.CommRing UInt64
-- Std.Do.PostCond
Std.Do.ExceptConds.and_elim_right : ∀ {ps : Std.Do.PostShape} (x y : Std.Do.ExceptConds ps), (x ∧ₑ y).entails y
-- Mathlib.Tactic.FastInstance
/-- `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into
constructor applications that leverage existing instances. It uses the expected type to fill in
the constructor applications and lambda binders of data fields.

For instance, when used as
```lean
instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..
```
this will define `instRing` as a nested constructor application that refers to `instSemiring`
rather than applications of `Function.Injective.ring` or other non-canonical constructors.
The advantage is then that `instRing.toSemiring` unifies almost immediately with `instSemiring`,
rather than having to break it down into smaller pieces.
 -/
Mathlib.Elab.FastInstance.fastInstance : Lean.ParserDescr
-- Mathlib.Order.DirectedInverseSystem
/-- If `i` is a limit in a well-ordered type indexing a family of types,
then `piLT X i` is the limit of all `piLT X j` for `j < i`.  -/
InverseSystem.piLTLim : {ι : Type u_6} →
  [inst : LinearOrder ι] →
    {X : ι → Type u_7} →
      {i : ι} → Order.IsSuccPrelimit i → InverseSystem.piLT X i ≃ ↑(InverseSystem.limit InverseSystem.piLTProj i)
-- Lean.Meta.Match.CaseValues
/-- Split goal `... |- C x`, where `fvarId` is `x`s id, into `values.size + 1` subgoals
1)   `..., (h_1 : x = value[0])      |- C value[0]`
...
n)   `..., (h_n : x = value[n - 1])  |- C value[n - 1]`
n+1) `..., (h_1 : x != value[0]) ... (h_n : x != value[n-1]) |- C x`
where `n = values.size`
The type of `x` must have decidable equality.

Remark: the last subgoal is for the "else" catchall case, and its `subst` is `{}`.
Remark: the field `newHs` has size 1 forall but the last subgoal.

If `needsHyps = false` then the else case comes without hypotheses.
 -/
Lean.Meta.caseValues : Lean.MVarId →
  Lean.FVarId →
    Array Lean.Expr → optParam Lean.Name `h → optParam Bool true → Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommRing.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [inst_1 : (i : ι) → AddCommGroup (A i)] →
        [toGRing : DirectSum.GRing A] → (∀ (a b : GradedMonoid A), a * b = b * a) → DirectSum.GCommRing A
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- This is a fork which is helpful for establishing comonadicity: the morphism from this fork to
the Beck equalizer is the counit for the adjunction on the comparison functor.
 -/
CategoryTheory.Comonad.ComonadicityInternal.counitFork : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {adj : F ⊣ G} →
              (A : adj.toComonad.Coalgebra) →
                [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] →
                  CategoryTheory.Limits.Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A)))
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc)
      (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) h)) =
    CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
-- Mathlib.NumberTheory.Modular
/-- The function `(c,d) → |cz+d|^2` is proper, that is, preimages of bounded-above sets are finite.
 -/
ModularGroup.tendsto_normSq_coprime_pair : ∀ (z : UpperHalfPlane), Filter.Tendsto (fun p => Complex.normSq (↑(p 0) * ↑z + ↑(p 1))) Filter.cofinite Filter.atTop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.not_nil_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w}, ¬(SimpleGraph.Walk.cons h p).Nil
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.foldM_filterMapWithPostcondition.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (match some c with
    | some c => h_1 c
    | x => h_2 x) =
    h_1 c
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₃
-- Mathlib.Data.ENat.Basic
instWellFoundedLTENat : WellFoundedLT ℕ∞
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofList_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {k : α} {v : β},
  Std.DHashMap.Raw.Const.ofList [(k, v)] = ∅.insert k v
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
CategoryTheory.IsFiltered.toSup.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X : C} (m : X ∈ O),
  CategoryTheory.IsFiltered.toSup O H m = CategoryTheory.IsFiltered.toSup O H m
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.setLIntegral_eq_top_of_measure_eq_top_ne_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  AEMeasurable f (μ.restrict s) → μ {x | x ∈ s ∧ f x = ⊤} ≠ 0 → ∫⁻ (x : α) in s, f x ∂μ = ⊤
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
/-- Given a profinite set `S` and a closed embedding `S → (I → Bool)`, the `ℤ`-module
`LocallyConstant C ℤ` is free.
 -/
Profinite.NobelingProof.Nobeling_aux : ∀ {I : Type u} [inst : LinearOrder I] [WellFoundedLT I] {S : Profinite} {ι : ↑S.toTop → I → Bool},
  Topology.IsClosedEmbedding ι → Module.Free ℤ (LocallyConstant ↑S.toTop ℤ)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.congrHash.goEq : Lean.Meta.Grind.ENodeMap → Lean.Expr → Lean.Expr → UInt64
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.η_hom_app_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : ChainComplex C ℕ) (i : ℕ),
  (CategoryTheory.Idempotents.DoldKan.η.hom.app X).f i =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map
            (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)).f
        i)
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X).f i)
-- Mathlib.CategoryTheory.Limits.EssentiallySmall
CategoryTheory.Limits.hasProductsOfShape_of_small : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β]
  [CategoryTheory.Limits.HasProducts C], CategoryTheory.Limits.HasProductsOfShape β C
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.tactic : Lean.Elab.DecreasingBy → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_piCurry : ∀ {ι : Type u_6} {κ : ι → Type u_7} (X : (i : ι) → κ i → Type u_8)
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], ⇑(MeasurableEquiv.piCurry X) = Sigma.curry
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congr_arg : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : LocallyConstant X Y) {x y : X}, x = y → f x = f y
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_toSubsemiring : ∀ {R : Type u} [inst : NonAssocRing R] {s : Subring R} {x : R}, x ∈ s.toSubsemiring ↔ x ∈ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_nat_mul_two_pi_add_pi : ∀ (n : ℕ), Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_left_one' : ∀ {α : Type u_2} [inst : Group α] {a : α}, Finset.preimage 1 (fun x => a⁻¹ * x) ⋯ = {a}
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instCanonicallyOverFiber : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (y : ↥Y) → (AlgebraicGeometry.Scheme.Hom.fiber f y).CanonicallyOver X
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The chain map from the standard resolution of `k` to `k[0]` given by `∑ nᵢgᵢ ↦ ∑ nᵢ` in
degree zero.  -/
Rep.standardComplex.εToSingle₀ : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] → Rep.standardComplex k G ⟶ (ChainComplex.single₀ (Rep.{u, u, u} k G)).obj (Rep.trivial k G k)
-- Lean.Meta.Tactic.UnifyEq
/-- Convert heterogeneous equality into a homogeneous one  -/
_private.Lean.Meta.Tactic.UnifyEq.0.Lean.Meta.heqToEq' : Lean.MVarId → Lean.LocalDecl → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_four : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {p₁ p₂ p₃ p₄ : P},
  List.Sbtw R [p₁, p₂, p₃, p₄] ↔ Sbtw R p₁ p₂ p₃ ∧ Sbtw R p₁ p₂ p₄ ∧ Sbtw R p₁ p₃ p₄ ∧ Sbtw R p₂ p₃ p₄
-- Lean.DocString.Types
Lean.Doc.instBEqMathMode.beq : Lean.Doc.MathMode → Lean.Doc.MathMode → Bool
-- Init.Notation
/-- `attr` is a builtin syntax category for attributes.
Declarations can be annotated with attributes using the `@[...]` notation.  -/
Lean.Parser.Category.attr : Lean.Parser.Category
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁.union t₂},
  Std.ExtDTreeMap.Const.get (t₁.union t₂) k h' = Std.ExtDTreeMap.Const.get t₂ k ⋯
-- Mathlib.Order.CompleteLattice.Basic
iInf_range' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : InfSet α] (g : β → α) (f : ι → β), ⨅ b, g ↑b = ⨅ i, g (f i)
-- Init.Data.ByteArray.Lemmas
ByteArray.toList_data_append : ∀ {l l' : ByteArray}, (l ++ l').data.toList = l.data.toList ++ l'.data.toList
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.induction_on : ∀ {α : Type u_1} [inst : UniformSpace α] {p : UniformSpace.Completion α → Prop} (a : UniformSpace.Completion α),
  IsClosed {a | p a} → (∀ (a : α), p ↑a) → p a
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_mono : ∀ {M : Type u_1} [inst : Add M] {U V : Set M}, U ⊆ V → SimpleGraph.addCayley U ≤ SimpleGraph.addCayley V