mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- Let `J` be a well-ordered type. Assume that for each `j : J`, we
have a family `basicCell j` of morphisms. A relative cell complex
is a morphism `f : X ⟶ Y` which is a transfinite composition of morphisms
in such a way that at the step `j : J`, we attach cells in the family `basicCell j`.  -/
HomotopicalAlgebra.RelativeCellComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [OrderBot J] →
          [SuccOrder J] →
            [WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  ((j : J) → (i : α j) → A j i ⟶ B j i) →
                    {X Y : C} → (X ⟶ Y) → Type (max (max (max (max t u) v) (w + 1)) w')
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α]
  [T0Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α},
  Multipliable f → ∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.reduce.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommRing R] {b : MvPolynomial σ R}
  (hb : IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R),
  m.reduce hb f = f - (MvPolynomial.monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
/-- If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to
`{b} × γ` has product `g b`, then the function `g` has product `a`.  -/
HasProd.prod_fiberwise : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α]
  [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α},
  HasProd f a → (∀ (b : β), HasProd (fun c => f (b, c)) (g b)) → HasProd g a
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.descend.injEq : ∀ {α : Type u_1} (butFirst butFirst_1 : Option α),
  (Lean.MessageData.VisitStep.descend✝ butFirst = Lean.MessageData.VisitStep.descend✝ butFirst_1) =
    (butFirst = butFirst_1)
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_iff_finiteIndex : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex
-- Lean.Elab.Do.Switch
Lean.Elab.Term.elabDo : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (x y : M), Associated x y = ∃ u, x * ↑u = y
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrOn.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsExtrOn f s a → HasLineDerivAt ℝ f f' a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Mathlib.MeasureTheory.Measure.Content
/-- This is "unbundled", because that is required for the API of `inducedOuterMeasure`.  -/
MeasureTheory.Content.innerContent_mono : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V),
  U ⊆ V → μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }
-- Lean.MetavarContext
Lean.isLevelMVarAssigned : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LMVarId → m Bool
-- Init.Data.Option.Lemmas
Option.isSome_dite : ∀ {β : Type u_1} {p : Prop} {x : Decidable p} {b : p → β}, (if h : p then some (b h) else none).isSome = true ↔ p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.min? = none
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric.0.termσ : Lean.ParserDescr
-- Init.Grind.AC
Lean.Grind.AC.eq_erase0_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase0_cert lhs rhs lhs' rhs' = (lhs.erase0.beq' lhs').and' (rhs.erase0.beq' rhs')
-- Lean.DocString.Syntax
/-- Block-level elements, such as paragraphs, headers, and lists.

Conventions:
* When there's concrete syntax that can be written as Lean atoms, do so (code blocks are ` ``` `,
  directives `:::`)
* When Verso's syntax requires a newline, use `|` because `"\n"` is not a valid Lean token
* Directive bodies are in `{` and `}` to avoid quotation parsing issues with `:::` ... `:::`
* If there's no concrete syntax per se, such as for paragraphs or lists, use a name with brackets
  and braces
* Use parentheses around required literals, such as the starting number of an ordered list
* Use square brackets around sequences of literals
* Use curly braces around blocks or lists items (because names and arguments a la roles are always
  newline-separated for directives and code)
 -/
Lean.Parser.Category.block : Lean.Parser.Category
-- Mathlib.Order.OrderDual
Equiv.sdiff_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : SDiff β] (a b : α), a \ b = e.symm (e a \ e b)
-- Mathlib.Probability.Moments.Variance
/-- The variance of the sum of two independent random variables is the sum of the variances.  -/
ProbabilityTheory.IndepFun.variance_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.IndepFun X Y μ →
        ProbabilityTheory.variance (X + Y) μ = ProbabilityTheory.variance X μ + ProbabilityTheory.variance Y μ
-- Lean.Elab.SyntheticMVars
/-- Try to synthesize `mvarId` by starting using a default instance with the given priority.
This method succeeds only if the metavariable of fully synthesized.

Remark: In the past, we would return a list of pending TC problems, but this was problematic since
a default instance may create subproblems that cannot be solved.

Remark: The new approach also has limitations because other pending metavariables are not taken into account
while backtracking. That is, we fail to synthesize `mvarId` because we reach subproblems that are stuck,
but we could "unstuck" them if we tried to solve other pending metavariables. Considering all pending metavariables
into a single backtracking search seems to be too expensive, and potentially generate incomprehensible error messages.
This is particularly true if we consider pending metavariables for "postponed" elaboration steps.
Here is an example that demonstrate this issue. The example considers we are using the old `binrel%` elaborator which was
disconnected from `binop%`.
```
example (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry
```
We have two pending coercions for the `↑` and `HSub ?m.220 ?m.221 ?m.222`.
When we did not use a backtracking search here, then the homogeneous default instance for `HSub`.
```
instance [Sub α] : HSub α α α where
```
would be applied first, and would propagate the expected type `Int` to the pending coercions which would now be unblocked.

Instead of performing a backtracking search that considers all pending metavariables, we improved the `binrel%` elaborator.
 -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio : Lean.MVarId → ℕ → Lean.Elab.TermElabM Bool
-- Init.Data.List.Attach
List.getLast_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a)
  (h : List.pmap f xs H ≠ []), (List.pmap f xs H).getLast h = f (xs.getLast ⋯) ⋯
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.prodOfFinsuppNat_injective : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] {f : P × M →ₗ[R] M},
  Function.Injective ⇑f → Function.Injective ⇑f.prodOfFinsuppNat
-- Mathlib.RingTheory.KrullDimension.Basic
ringKrullDim_eq_bot_of_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] [Subsingleton R], ringKrullDim R = ⊥
-- Aesop.Frontend.Tactic
/-- `aesop <clause>*` tries to solve the current goal by applying a set of rules
registered with the `@[aesop]` attribute. See [its
README](https://github.com/JLimperg/aesop#readme) for a tutorial and a
reference.

The variant `aesop?` prints the proof it found as a `Try this` suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available
clauses are:

- `(add <phase> <priority> <builder> <rule>)` adds a rule. `<phase>` is
  `unsafe`, `safe` or `norm`. `<priority>` is a percentage for unsafe rules and
  an integer for safe and norm rules. `<rule>` is the name of a declaration or
  local hypothesis. `<builder>` is the rule builder used to turn `<rule>` into
  an Aesop rule. Example: `(add unsafe 50% apply Or.inl)`.
- `(erase <rule>)` disables a globally registered Aesop rule. Example: `(erase
  Aesop.BuiltinRules.assumption)`.
- `(rule_sets := [<ruleset>,*])` enables or disables named sets of rules for
  this Aesop call. Example: `(rule_sets := [-builtin, MyRuleSet])`.
- `(config { <opt> := <value> })` adjusts Aesop's search options. See
  `Aesop.Options`.
- `(simp_config { <opt> := <value> })` adjusts options for Aesop's built-in
  `simp` rule. The given options are directly passed to `simp`. For example,
  `(simp_config := { zeta := false })` makes Aesop use
  `simp (config := { zeta := false })`.
 -/
Aesop.Frontend.Parser.aesopTactic? : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
ContinuousLinearEquiv.homothety_inverse : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_6 : RingHomInvPair σ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ] (a : ℝ),
  0 < a → ∀ (f : E ≃ₛₗ[σ] F), (∀ (x : E), ‖f x‖ = a * ‖x‖) → ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {fallback : β} {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k fallback =
        (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.rat_sub_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_inverse_map_get_coe : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : PartialFun.of { x // x ≠ X.point }) (property : f.toFun ↑a ≠ Y.point),
  ↑((partialFunEquivPointed.inverse.map f a).get property) = f.toFun ↑a
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.add.injEq : ∀ (a b a_1 b_1 : Lean.Grind.Linarith.Expr), (a.add b = a_1.add b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein.z.eq_1 : ∀ {n : ℕ} (k : Fin (n + 1)), bernstein.z k = ⟨↑↑k / ↑n, ⋯⟩
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iUnion : ∀ {α : Type u_1} {ι : Sort u_3} [inst : LE α] {f : ι → Set α}, (∀ (i : ι), IsLowerSet (f i)) → IsLowerSet (⋃ i, f i)
-- Qq.Typ
/-- `Quoted α` is the type of Lean expressions having type `α`.

You should usually write this using the notation `Q($α)`.
 -/
Qq.Quoted : Lean.Expr → Type
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.CG.sup : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N₁ N₂ : L.Substructure M},
  N₁.CG → N₂.CG → (N₁ ⊔ N₂).CG
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.one_le_mul_inv`. -/
Units.one_le_mul_inv_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), ↑u ≤ a → 1 ≤ a * ↑u⁻¹
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.instIsAdicCompleteMaximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : IsLocalRing R],
  IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R))
    (AdicCompletion (IsLocalRing.maximalIdeal R) R)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.span_gramSchmidt_Iio : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (c : ι), Submodule.span 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f '' Set.Iio c) = Submodule.span 𝕜 (f '' Set.Iio c)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_MonadExcept : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {x : m α} {h : ε → m α}
  {Q : Std.Do.PostCond α ps} [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps],
  (Std.Do.wp (tryCatch x h)).apply Q = (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q
-- Mathlib.Order.JordanHolder
CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → s₁.length = 0 → s₂.length = 0
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Surjective.surj : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.Surjective f], Function.Surjective ⇑f
-- Mathlib.Topology.AlexandrovDiscrete
AlexandrovDiscrete.toFirstCountable : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α], FirstCountableTopology α
-- Init.Data.List.Basic
/-- If two lists are identical except for having their first two elements swapped, then they are
permutations of each other: `x::y::l ~ y::x::l`.
 -/
List.Perm.swap : ∀ {α : Type u} (x y : α) (l : List α), (y :: x :: l).Perm (x :: y :: l)
-- Mathlib.Data.Set.Monotone
strictAntiOn_insert_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, b < a → f a < f b) ∧ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_graphOn_univ : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : CommGroup β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (x : α × β) (f : F),
  x • Set.graphOn (⇑f) Set.univ = Set.graphOn (fun a => x.2 / f x.1 * f a) Set.univ
-- Mathlib.Analysis.Convex.Extrema
/-- Helper lemma for the more general case: `IsMinOn.of_isLocalMinOn_of_convexOn`.
 -/
IsMinOn.of_isLocalMinOn_of_convexOn_Icc : ∀ {β : Type u_2} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] [inst_3 : Module ℝ β]
  [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {f : ℝ → β} {a b : ℝ},
  a < b → IsLocalMinOn f (Set.Icc a b) a → ConvexOn ℝ (Set.Icc a b) f → IsMinOn f (Set.Icc a b) a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_image_mulLeft_inv_inter_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s t : Set α} {a : α},
  ((fun x => a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun x => x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `eVariation_mul_le` -/
eVariationOn_fun_mul_le : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {C D : ENNReal} {s : Set α},
  (∀ x ∈ s, ‖f x‖ₑ ≤ C) →
    (∀ x ∈ s, ‖g x‖ₑ ≤ D) → eVariationOn (fun i => f i * g i) s ≤ C * eVariationOn g s + D * eVariationOn f s
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
-- Batteries.Data.List.Lemmas
List.sum_zero_cons : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] {l : List α},
  (0 :: l).sum = l.sum
-- Mathlib.Data.Finite.Prod
Set.Finite.prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Finite → t.Finite → (s ×ˢ t).Finite
-- Init.Data.BitVec.Lemmas
BitVec.instCommutativeHMul : ∀ {w : ℕ}, Std.Commutative fun x y => x * y
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map.eq_1 : ∀ {n : ℕ} (d : ℕ), Behrend.map d = { toFun := fun a => ∑ i, a i * d ^ ↑i, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.Spectrum.Maximal.Topology
MaximalSpectrum.instT1Space : ∀ {R : Type u} [inst : CommRing R], T1Space (MaximalSpectrum R)
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Roc.Sliceable.mkSlice xs lo<...=hi).stop = min (hi + 1) xs.size
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.of_toFunctor : ∀ {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) [inst_6 : F.LaxBraided], (CategoryTheory.LaxBraidedFunctor.of F).toFunctor = F
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adjunction.ofCat_id : ∀ (C : CategoryTheory.Cat),
  CategoryTheory.Adjunction.ofCat (CategoryTheory.Bicategory.Adjunction.id C) = CategoryTheory.Adjunction.id
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The projection on the `i`-th coordinate of `PiLp p β`, as a continuous linear map.  -/
PiLp.proj : (p : ENNReal) →
  {𝕜 : Type u_1} →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [inst : Semiring 𝕜] →
          [inst_1 : (i : ι) → NormedAddCommGroup (β i)] →
            [inst_2 : (i : ι) → Module 𝕜 (β i)] → (i : ι) → PiLp p β →L[𝕜] β i
-- Mathlib.Testing.Plausible.Functions
_private.Mathlib.Testing.Plausible.Functions.0.List.dlookup.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (a' : α) → (b : β a') → (l : List (Sigma β)) → motive (⟨a', b⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨a', b⟩ :: l => h_2 a' b l) =
    h_1 ()
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_isOpen_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f ↔ ∀ (y : Y), IsOpen (f ⁻¹' {y})
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.notification.inj : ∀ {method : String} {params? : Option Lean.Json.Structured} {method_1 : String}
  {params?_1 : Option Lean.Json.Structured},
  Lean.JsonRpc.Message.notification method params? = Lean.JsonRpc.Message.notification method_1 params?_1 →
    method = method_1 ∧ params? = params?_1
-- Mathlib.Data.Finset.Card
/-- We can shrink a set to any smaller size.  -/
Finset.exists_subset_card_eq : ∀ {α : Type u_1} {s : Finset α} {n : ℕ}, n ≤ s.card → ∃ t ⊆ s, t.card = n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_ofRepr : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι),
  ⇑{ repr := e } = fun i => e.symm (EuclideanSpace.single i 1)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.isIrreducible_iff_invtRootSubmodule : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [inst_3 : Module K M] [inst_4 : Module K N] [Nontrivial M] (P : RootPairing ι K M N),
  P.IsIrreducible ↔ IsSimpleOrder ↥P.invtRootSubmodule
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_hom_comp_i : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 2) (groupHomology.chainsIso₂ A).hom
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_congr_mono : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t → μ.restrict t = ν.restrict t → μ.restrict s = ν.restrict s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.symm_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ}, IntervalIntegrable f μ a b ↔ IntervalIntegrable f μ b a
-- ProofWidgets.Util
instFromJsonUnit_proofWidgets : Lean.FromJson Unit
-- Init.Data.Int.Order
Int.sign_natCast_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → (↑n).sign = 1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_le_iff_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N},
  Subsemigroup.map f S ≤ T ↔ S ≤ Subsemigroup.comap f T
-- Mathlib.Data.Finset.Insert
Finset.subset_singleton_iff' : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊆ {a} ↔ ∀ b ∈ s, b = a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_eq_one : ∀ {M : Type u_4} [inst : Monoid M] {l : List M}, (∀ x ∈ l, x = 1) → l.prod = 1
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ) (h : n₁ + n₂ = n)
  (m₂ m : ℤ) (hm₂ : m₂ = n₂ + y) (hm : m = n + y) {Z : D}
  (h_1 : ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h)
      (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n) h_1) =
    CategoryTheory.CategoryStruct.comp
      ((n₁ * y).negOnePow •
        CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom)
          (CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯)
            ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv))
      h_1
-- Mathlib.Topology.MetricSpace.Holder
/-- A Hölder continuous function is uniformly continuous  -/
HolderOnWith.uniformContinuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → 0 < r → UniformContinuousOn f s
-- Init.Classical
/-- Transfer decidability of `¬ p` to decidability of `p`.  -/
Classical.decidable_of_decidable_not : (p : Prop) → [h : Decidable ¬p] → Decidable p
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.inc.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15),
  sizeOf (Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h) =
    1 + sizeOf fvarId + sizeOf n + sizeOf check + sizeOf persistent + sizeOf k + sizeOf h
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Triangle diagrams for (right) lifts.
```
            b
          ◹ |
   lift /   |      | counit
      /     | f    ▽
    /       ▽
  c - - - ▷ a
       g
```
 -/
CategoryTheory.Bicategory.RightLift : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (b ⟶ a) → (c ⟶ a) → Type (max v w)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root element in the equivalence class of `e`.  -/
Lean.Meta.Grind.getNext : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr