mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- Let `e` be an open partial homeomorphism of `B × F` whose source is `U ×ˢ univ`, for some set
`U` in `B`, and which, at any point `x` in `U`, admits a neighbourhood `u` of `x` such that `e` is
equal on `u ×ˢ univ` to some bi-`C^n` fiberwise linear open partial homeomorphism.  Then `e` itself
is equal to some bi-`C^n` fiberwise linear open partial homeomorphism.

This is the key mathematical point of the `locality` condition in the construction of the
`StructureGroupoid` of bi-`C^n` fiberwise linear open partial homeomorphisms.  The proof is by
gluing together the various bi-`C^n` fiberwise linear open partial homeomorphism which exist
locally.

The `U` in the conclusion is the same `U` as in the hypothesis. We state it like this, because this
is exactly what we need for `contMDiffFiberwiseLinear`.  -/
ContMDiffFiberwiseLinear.locality_aux₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB]
  [inst_5 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B]
  {IB : ModelWithCorners 𝕜 EB HB} (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)) (U : Set B),
  e.source = U ×ˢ Set.univ →
    (∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
            ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) u) (h2φ :
            ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) u),
            (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)) →
      ∃ Φ U,
        ∃ (hU₀ : IsOpen U) (hΦ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(Φ x)) U) (h2Φ :
          ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(Φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph Φ hU₀ ⋯ ⋯)
-- Init.Data.List.Monadic
List.mapM'_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → m β}, List.mapM' f [] = pure []
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constModify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ (k : α) (f : β → β),
        m₁.Equiv m₂ → (Std.DHashMap.Raw.Const.modify m₁ k f).Equiv (Std.DHashMap.Raw.Const.modify m₂ k f)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M}
  {n : WithTop ℕ∞}, (∀ y ∈ s, f₁ y = f y) → (ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s)
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_single_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a₁ a₂ : α) (b₁ b₂ : M),
  ((fun₀ | a₁ => b₁) = fun₀ | a₂ => b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_6 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2) (x y : RingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.mul y with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_6 x y
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.extendScalars_adjoin : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E}
  {S : Set E} (h : K ≤ IntermediateField.adjoin F S),
  IntermediateField.extendScalars h = IntermediateField.adjoin (↥K) S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).isEmpty = ((t.erase k).isEmpty && (f (t.get? k)).isNone)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.neg` -/
Differentiable.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  Differentiable 𝕜 f → Differentiable 𝕜 fun i => -f i
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.State.mk.inj : ∀ {newGoals : Array Lean.MVarId} {patterns : List (Lean.TSyntax `rintroPat)} {newGoals_1 : Array Lean.MVarId}
  {patterns_1 : List (Lean.TSyntax `rintroPat)},
  { newGoals := newGoals, patterns := patterns } = { newGoals := newGoals_1, patterns := patterns_1 } →
    newGoals = newGoals_1 ∧ patterns = patterns_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.sum.map_one : ∀ {α : Type u} [inst : AddGroup α], FreeGroup.sum 1 = 0
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.strictMono_valueGroupOrderIso₀_symm : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀),
  StrictMono ⇑(WithVal.valueGroupOrderIso₀ v).symm
-- Mathlib.LinearAlgebra.Vandermonde
/-- `vandermonde v` is the square matrix with `i`th row equal to `1, v i, v i ^ 2, v i ^ 3, ...`.  -/
Matrix.vandermonde : {R : Type u_1} → [CommRing R] → {n : ℕ} → (Fin n → R) → Matrix (Fin n) (Fin n) R
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.addCommute_inlₗ_inrₗ : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (m : α) (n : β), AddCommute ((OrderAddMonoidHom.inlₗ α β) m) ((OrderAddMonoidHom.inrₗ α β) n)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_comp_δ_of_not_surjective : ∀ {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ { len := n + 1 }),
  ¬Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom θ) →
    ∃ i θ', θ = CategoryTheory.CategoryStruct.comp θ' (SimplexCategory.δ i)
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerEquiv_symm_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [inst_3 : IsUltrametricDist E] [inst_4 : CompleteSpace E]
  (a : ZeroAtInftyContinuousMap ℕ E), (PadicInt.mahlerEquiv E).symm a = PadicInt.mahlerSeries ⇑a
-- Aesop.Rule.Name
Aesop.instInhabitedDisplayRuleName.default : Aesop.DisplayRuleName
-- Mathlib.Algebra.Ring.Pi
Pi.commRing : {I : Type u} → {f : I → Type v} → [(i : I) → CommRing (f i)] → CommRing ((i : I) → f i)
-- Std.Async.System
/-- The current high-resolution timestamp in nanoseconds. It is relative to an arbitrary time in the past.
 -/
Std.Async.System.getHighResolutionTime : IO Std.Time.Nanosecond.Offset
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α} {h : Std.DTreeMap.Internal.Impl.contains a t = true}, t.getKey a h = t.getKeyD a fallback
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.reverse.match_1.eq_2 : ∀ (motive : (x : ℕ) → BitVec x → Sort u_1) (w : ℕ) (x : BitVec (w + 1)) (h_1 : (x : BitVec 0) → motive 0 x)
  (h_2 : (w : ℕ) → (x : BitVec (w + 1)) → motive w.succ x),
  (match w.succ, x with
    | 0, x => h_1 x
    | w.succ, x => h_2 w x) =
    h_2 w x
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.ofList_dProd : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] {α : Type u_3} (l : List α) (fι : α → ι)
  (fA : (a : α) → A (fι a)),
  (DirectSum.of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a => (DirectSum.of A (fι a)) (fA a)) l).prod
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.toAbsoluteValue_apply : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [inst_3 : IsAbsoluteValue abv] (a : R), (IsAbsoluteValue.toAbsoluteValue abv) a = abv a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.sign.eq_def : ∀ (x : Tactic.ComputeAsymptotics.UnitMonomial),
  x.sign =
    match x with
    | [] => Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero
    | hd :: tl =>
      if 0 < hd then Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos
      else
        if hd < 0 then Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg
        else Tactic.ComputeAsymptotics.UnitMonomial.sign tl
-- Mathlib.Topology.Homotopy.Lifting
/-- The existence of `liftHomotopy` satisfying `liftHomotopy_lifts` and `liftHomotopy_zero` is
the homotopy lifting property for covering maps.
In other words, a covering map is a Hurewicz fibration.
Proposition 1.30 of [hatcher02].  -/
IsCoveringMap.liftHomotopy : {E : Type u_1} →
  {X : Type u_2} →
    {A : Type u_3} →
      [inst : TopologicalSpace E] →
        [inst_1 : TopologicalSpace X] →
          [inst_2 : TopologicalSpace A] →
            {p : E → X} →
              IsCoveringMap p →
                (H : C(↑unitInterval × A, X)) →
                  (f : C(A, E)) → (∀ (a : A), H (0, a) = p (f a)) → C(↑unitInterval × A, E)
-- Mathlib.Computability.TuringMachine.Config
List.headI.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α], [].headI = default
-- Std.Do.PostCond
/-- Entailment of postconditions.

This consists of:
 * Entailment of the assertion about the return value, for all possible return values.
 * Entailment of the exception conditions.

While implication of postconditions (`PostCond.imp`) results in a new postcondition, entailment is
an ordinary proposition.
 -/
Std.Do.«term_⊢ₚ_» : Lean.TrailingParserDescr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ t.insertMany l},
      k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get k' h' = k
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two_mul_add_one : ∀ (n : ℤ), Int.fib (2 * n + 1) = Int.fib (n + 1) ^ 2 + Int.fib n ^ 2
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
groupAddGroupEquivalence_counitIso : groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrpCat.toGrp.comp GrpCat.toAddGrp)
-- Init.Data.Int.DivMod.Lemmas
Int.add_emod_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (y + x % ↑n).bmod n = (y + x).bmod n
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.cast_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : Function.LeftInverse g f)
  (C : (a : α) → γ (f a)) (a : α), cast ⋯ (C (g (f a))) = C a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.isCentralScalar : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] [inst_2 : SMulZeroClass Sᵐᵒᵖ R]
  [IsCentralScalar S R], IsCentralScalar S (Polynomial R)
-- Aesop.Search.SearchM
Aesop.SearchM.Context.ruleSet : Aesop.SearchM.Context → Aesop.LocalRuleSet
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rci.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.toArray = (Std.Rci.Internal.iter r).toArray
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_insert_left : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → insert a (Finset.Ioc a b) = Finset.Icc a b
-- Aesop.RuleSet.Member
Aesop.instInhabitedBaseRuleSetMember : Inhabited Aesop.BaseRuleSetMember
-- Mathlib.Data.EReal.Inv
/-- Extension for the `positivity` tactic: inverse of an `EReal`.  -/
Mathlib.Meta.Positivity.evalERealInv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We have that `J(a | b^e) = J(a | b)^e`.  -/
jacobiSym.pow_right : ∀ (a : ℤ) (b e : ℕ), jacobiSym a (b ^ e) = jacobiSym a b ^ e
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
/-- *Gauss-Lucas Theorem*: if $P$ is a nonconstant polynomial with complex coefficients,
then all zeros of $P'$ belong to the convex hull of the set of zeros of $P$.

This version provides explicit formulas for the coefficients of the convex combination.
See also `rootSet_derivative_subset_convexHull_rootSet` below.
 -/
Polynomial.eq_centerMass_of_eval_derivative_eq_zero : ∀ {P : Polynomial ℂ} {z : ℂ},
  0 < P.degree →
    Polynomial.eval z (Polynomial.derivative P) = 0 → z = P.roots.toFinset.centerMass (P.derivRootWeight z) id
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  (s : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).obj F).obj s = ∏ᶜ fun x => F.obj ↑x
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Notation for m×n matrices, aka `Matrix (Fin m) (Fin n) α`.

For instance:
* `!![a, b, c; d, e, f]` is the matrix with two rows and three columns, of type
  `Matrix (Fin 2) (Fin 3) α`
* `!![a, b, c]` is a row vector of type `Matrix (Fin 1) (Fin 3) α` (see also `Matrix.row`).
* `!![a; b; c]` is a column vector of type `Matrix (Fin 3) (Fin 1) α` (see also `Matrix.col`).

This notation implements some special cases:

* `![,,]`, with `n` `,`s, is a term of type `Matrix (Fin 0) (Fin n) α`
* `![;;]`, with `m` `;`s, is a term of type `Matrix (Fin m) (Fin 0) α`
* `![]` is the 0×0 matrix

Note that vector notation is provided elsewhere (by `Matrix.vecNotation`) as `![a, b, c]`.
Under the hood, `!![a, b, c; d, e, f]` is syntax for `Matrix.of ![![a, b, c], ![d, e, f]]`.
 -/
Matrix.matrixNotation0xC : Lean.ParserDescr
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.runMetaM : {α : Type} → ProofWidgets.ExprWithCtx → (Lean.Expr → Lean.MetaM α) → IO α
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Coindep.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X → X ⊆ M.E
-- Mathlib.MeasureTheory.Measure.ContinuousPreimage
/-- Let `f : Z → C(X, Y)` be a continuous (in the compact open topology) family
of continuous measure-preserving maps.
Let `t : Set Y` be a null measurable set of finite measure.
Then for any `s`, the set of parameters `z`
such that the preimage of `t` under `f_z` is a.e. equal to `s`
is a closed set.

In particular, if `X = Y` and `s = t`,
then we see that the a.e. stabilizer of a set is a closed set.  -/
MeasureTheory.isClosed_setOfPred_preimage_ae_eq : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  [R1Space X] [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
  [inst_8 : TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)},
  Continuous f →
    (∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) →
      ∀ (s : Set X) {t : Set Y}, MeasureTheory.NullMeasurableSet t ν → ν t ≠ ⊤ → IsClosed {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}
-- ProofWidgets.Component.RefreshComponent
/-- The HTML tree to display, stored as a delayed computation.

We only force the thunk when the client requests it.
This means that if several updates arrive in quick succession,
only the ones that the client actually sees will be computed.  -/
ProofWidgets.RefreshComponent.RefreshState.curr : ProofWidgets.RefreshComponent.RefreshState → Thunk ProofWidgets.Html
-- 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_1 : ∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1) (var : Std.Tactic.BVDecide.BVPred)
  (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.literal var 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_1 var
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg.instIsAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant], μ.neg.IsAddLeftInvariant
-- Mathlib.Tactic.GCongr.ForwardAttr
/-- An extension for `gcongr_forward`.  -/
Mathlib.Tactic.GCongr.ForwardExt : Type
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {f : α → Bool},
  t.WF → (Std.TreeSet.Raw.filter f t).toList = List.filter f t.toList
-- Mathlib.Logic.Function.Basic
Function.Injective.trichotomous_onFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [Std.Trichotomous r], Std.Trichotomous (Function.onFun r f)
-- Mathlib.GroupTheory.Nilpotent
_private.Mathlib.GroupTheory.Nilpotent.0.Subgroup.upperCentralSeriesAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Data.Finset.Image
Finset.map_filter : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {p : α → Prop} [inst : DecidablePred p],
  Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p ∘ ⇑f.symm) (Finset.map f.toEmbedding s)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_natCast : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : NatCast R]
  (n : ℕ), (HahnSeries.single 0) ↑n = ↑n
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.inner.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  sizeOf (Std.DTreeMap.Internal.Impl.inner size k v l r) = 1 + sizeOf size + sizeOf k + sizeOf v + sizeOf l + sizeOf r
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of the reverse direction of `Set.subset_compl_iff_disjoint_right`. -/
Disjoint.subset_compl_right : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → s ⊆ tᶜ
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.hom_ext`. -/
CategoryTheory.Mod_.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f₁ f₂ : M ⟶ N), f₁.hom = f₂.hom → f₁ = f₂
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_vadd_eball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), (fun x => c +ᵥ x) ⁻¹' Metric.eball x r = Metric.eball (-c +ᵥ x) r
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The `MulActionHom` underlying a `LinearMap`.  -/
LinearMap.toMulActionHom : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] → [inst_5 : Module S M₂] → (M →ₛₗ[σ] M₂) → M →ₑ[⇑σ] M₂
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_mod : ∀ (a b : UInt16), (a % b).toUInt64 = a.toUInt64 % b.toUInt64
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- Let `G` be a finite commutative group and let `H` be a subgroup. If `M` is a commutative monoid
such that `G →* Mˣ` and `H →* Mˣ` are both finite (this is the case for example if `M` is a
commutative domain) and with enough `n`th roots of unity, where `n` is the exponent
of `G`, then any homomorphism `H →* Mˣ` can be extended to an homomorphism `G →* Mˣ`.
 -/
MonoidHom.domRestrict_surjective : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Function.Surjective ⇑(MonoidHom.domRestrictHom H Mˣ)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion `f : X ⟶ Y` induces an isomorphism `X ≅ Y|_{f(X)}`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Y) → [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → X ≅ Y.restrict ⋯
-- Init.Data.BitVec.Basic
/-- Remainder for signed division rounding to zero.

SMT-LIB name: `bvsrem`.
 -/
BitVec.srem : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- If `P` is a partition of `s₁` and `s₁ ⊆ s₂` then
`∑ p ∈ P.parts, f p ≤ preVariationFun f s₂`.  -/
MeasureTheory.preVariation.sum_le_preVariationFun_of_subset : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X} (hs₁ : MeasurableSet s₁),
  MeasurableSet s₂ → s₁ ⊆ s₂ → ∀ (P : Finpartition ⟨s₁, hs₁⟩), ∑ p ∈ P.parts, f ↑p ≤ MeasureTheory.preVariationFun f s₂
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- If `X` is a limit indexed by `J` of objects satisfying a property `P`,
it is also a limit indexed by `J` of objects satisfying `Q` if `P ≤ Q`.  -/
CategoryTheory.ObjectProperty.LimitOfShape.ofLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.LimitOfShape J X → {Q : CategoryTheory.ObjectProperty C} → P ≤ Q → Q.LimitOfShape J X
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.eq_1 : ∀ {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 = ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r