mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
norm_iteratedFDeriv_eq_norm_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜}, ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.locallyOfFinitePresentation_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.LocallyOfFinitePresentation f]
  [hg : AlgebraicGeometry.LocallyOfFinitePresentation g],
  AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.continuous_iteratedFDeriv' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {m : ℕ}, ContDiff 𝕜 (↑m) f → Continuous fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib.Analysis.Convex.Side
Wbtw.wSameSide₂₁ : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Wbtw R x y z → z ∈ s → s.WSameSide y x
-- Mathlib.Topology.Category.UniformSpace
/-- Turn a morphism in `UniformSpaceCat` back into a function which is `UniformContinuous`.  -/
UniformSpaceCat.Hom.hom : {X Y : UniformSpaceCat} → X.Hom Y → { f // UniformContinuous f }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t)[k]? = Option.map (f k) t[k]?
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  IsStrictlyPositive a ↔ IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a
-- Mathlib.Data.Set.Finite.Lattice
/-- A union of sets with `Fintype` structure over a set with `Fintype` structure has a `Fintype`
structure.  -/
Set.fintypeBiUnion : {α : Type u} →
  [DecidableEq α] →
    {ι : Type u_1} →
      (s : Set ι) → [Fintype ↑s] → (t : ι → Set α) → ((i : ι) → i ∈ s → Fintype ↑(t i)) → Fintype ↑(⋃ x ∈ s, t x)
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {B : C}
  (x : T.obj₁ ⟶ (CategoryTheory.shiftFunctor C n₀).obj B),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.preadditiveYoneda.obj B).homologySequenceδ
          ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T)) n₀ n₁ h))
      x =
    CategoryTheory.CategoryStruct.comp T.mor₃
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map x)
        ((CategoryTheory.shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B))
-- Mathlib.Algebra.Algebra.Tower
AlgHom.coe_restrictScalars' : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A →ₐ[S] B), ⇑(AlgHom.restrictScalars R f) = ⇑f
-- Mathlib.RingTheory.Localization.Ideal
/-- If `S` is the localization of `R` at a submonoid, the ordering of ideals of `S` is
embedded in the ordering of ideals of `R`.  -/
IsLocalization.orderEmbedding : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Ideal S ↪o Ideal R
-- Mathlib.NumberTheory.NumberField.House
/-- The house is the largest of the modulus of the conjugates of an algebraic number.  -/
NumberField.house_eq_sup' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K),
  NumberField.house α = ↑(Finset.univ.sup' ⋯ fun φ => ‖φ α‖₊)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
  Nonempty (CategoryTheory.RegularEpi f) → CategoryTheory.IsRegularEpi f
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_of_not_mem_image_support : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {x : α →₀ M} {b : β},
  b ∉ f '' ↑x.support → (Finsupp.mapDomain f x) b = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.endsWith_char_iff_exists_append : ∀ {c : Char} {s : String}, s.endsWith c = true ↔ ∃ t, s = t ++ String.singleton c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α}, ∅.maxD fallback = fallback
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.symm_symm : ∀ {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁), F.symm.symm = F
-- Mathlib.Order.Monotone.Monovary
StrictAnti.trans_antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : PartialOrder ι], StrictAnti f → Antivary g f → Monotone g
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.distinctConstantsTheory_eq_iUnion : ∀ {L : FirstOrder.Language} {α : Type u'} (s : Set α),
  L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.other.sizeOf_spec : sizeOf Lean.Meta.LazyDiscrTree.Key.other = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `X : T` is terminal, then the over category of `X` is equivalent to `T`.  -/
CategoryTheory.Over.equivalenceOfIsTerminal : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Limits.IsTerminal X → (CategoryTheory.Over X ≌ T)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_nonneg : ∀ {α : Sort u_4} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {f : α → M},
  (∀ (i : α), 0 ≤ f i) → 0 ≤ ∑ᶠ (i : α), f i
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.toContinuousAddEquiv.eq_1 : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s),
  e.toContinuousAddEquiv he =
    { toFun := ⇑e, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousOn.zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  {X : Type u_4} [inst_4 : TopologicalSpace X] {s : Set X} {f : X → G₀},
  ContinuousOn f s → ∀ (m : ℤ), (∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) → ContinuousOn (fun x => f x ^ m) s
-- Qq.Typ
/-- For a safer constructor, see `Qq.assertLevelDefEqQ`.  -/
Qq.QuotedLevelDefEq.unsafeIntro : ∀ {u v : Lean.Level}, u =QL v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} (hc : Std.DTreeMap.Internal.Impl.contains k t = true), (compare k (t.maxKey ⋯)).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Raw.Const.getD (m₁ \ m₂) k fallback =
          if m₂.contains k = true then fallback else Std.DTreeMap.Raw.Const.getD m₁ k fallback
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [self : F.IsContinuous J K]
  (G : CategoryTheory.Sheaf K (Type (max u₁ v₁ u₂ v₂))), CategoryTheory.Presieve.IsSheaf J (F.op.comp G.obj)
-- Mathlib.Util.Delaborators
/-- Dependent function type (a "pi type"). The notation `Π x : α, β x` can
also be written as `(x : α) → β x`.  -/
PiNotation.piNotation : Lean.Parser.Parser
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.sdiff_infinite_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → ((B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite)
-- Mathlib.Algebra.BigOperators.Pi
prod_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : CommMonoid β]
  [inst_2 : CommMonoid F] [IsOneApply F α β] [IsMulApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd.injEq : ∀ (a b : ℤ) (c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (a_1 b_1 : ℤ)
  (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd a b c₁ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd a_1 b_1 c₁_1 c₂_1) =
    (a = a_1 ∧ b = b_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.Data.UInt.Basic
instComplementUInt16 : Complement UInt16
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instCommMonoid : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → CommMonoid (PerfectClosure K p)
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it' : Std.IterM m α)
  (out : α) (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_natCast : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : NatCast α] (n : ℕ), (↑n).toProd.2 = ↑n
-- Mathlib.SetTheory.ZFC.Class
Class.not_empty_hom : ∀ (x : ZFSet.{u}), ¬∅ x
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.deriv_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f x → deriv f x < slope f x y
-- Mathlib.RingTheory.Ideal.Operations
Submodule.smul_le_span : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R) (I : Ideal R), s • I ≤ Ideal.span s
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrtho_zero_right : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : CommSemiring R₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₂ M₂] [inst_7 : AddCommMonoid M] [inst_8 : Module R M] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₁), B.IsOrtho x 0
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_neg : ∀ {w : ℕ} {n : ℤ}, BitVec.ofInt w (-n) = -BitVec.ofInt w n
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projIdx.inj : ∀ {structName : Lean.Name} {idx : ℕ} {structName_1 : Lean.Name} {idx_1 : ℕ},
  Lean.Elab.Term.LValResolution.projIdx structName idx = Lean.Elab.Term.LValResolution.projIdx structName_1 idx_1 →
    structName = structName_1 ∧ idx = idx_1
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnratCast_im : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ≥0), RCLike.im ↑q = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.maxKey he) fallback = t.maxKey he
-- Mathlib.Topology.Algebra.Group.Basic
Units.instIsTopologicalGroupOfContinuousMul : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α], IsTopologicalGroup αˣ
-- Lean.Data.OpenDecl
Lean.OpenDecl.explicit.inj : ∀ {id declName id_1 declName_1 : Lean.Name},
  Lean.OpenDecl.explicit id declName = Lean.OpenDecl.explicit id_1 declName_1 → id = id_1 ∧ declName = declName_1
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The `normalizer` of `S` is the subgroup of `G` whose elements satisfy `g + S - g = S`.
When `S` is a subgroup, this is the largest subgroup of `G` inside which `S` is normal.  -/
AddSubgroup.normalizer : {G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup G
-- Mathlib.Order.Filter.Map
Filter.Eventually.comap : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {p : β → Prop},
  (∀ᶠ (b : β) in g, p b) → ∀ (f : α → β), ∀ᶠ (a : α) in Filter.comap f g, p (f a)
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.localRec.inj : ∀ {baseName : Lean.Name} {fvar : Lean.Expr} {baseName_1 : Lean.Name} {fvar_1 : Lean.Expr},
  Lean.Elab.Term.LValResolution.localRec baseName fvar = Lean.Elab.Term.LValResolution.localRec baseName_1 fvar_1 →
    baseName = baseName_1 ∧ fvar = fvar_1
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsCancelMul α], IsCancelMul (Lex α)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.range_IciExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β),
  Set.range (Set.IciExtend f) = Set.range f
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.induct_unfolding : ∀ (motive : ℕ → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (s₁ s₂ : Lean.Grind.AC.Seq), motive 0 s₁ s₂ (s₁.concat s₂)) →
    (∀ (fuel : ℕ) (x₁ x₂ : Lean.Grind.AC.Var),
        Nat.blt x₁ x₂ = true →
          motive fuel.succ (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂)
            (Lean.Grind.AC.Seq.cons x₁ (Lean.Grind.AC.Seq.var x₂))) →
      (∀ (fuel : ℕ) (x₁ x₂ : Lean.Grind.AC.Var),
          ¬Nat.blt x₁ x₂ = true →
            motive fuel.succ (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂)
              (Lean.Grind.AC.Seq.cons x₂ (Lean.Grind.AC.Seq.var x₁))) →
        (∀ (fuel : ℕ) (x₁ x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
            motive fuel.succ (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s)
              (Lean.Grind.AC.Seq.insert x₁ (Lean.Grind.AC.Seq.cons x s))) →
          (∀ (fuel : ℕ) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq) (x₂ : Lean.Grind.AC.Var),
              motive fuel.succ (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂)
                (Lean.Grind.AC.Seq.insert x₂ (Lean.Grind.AC.Seq.cons x s))) →
            (∀ (fuel : ℕ) (x₁ : Lean.Grind.AC.Var) (s₁ : Lean.Grind.AC.Seq) (x₂ : Lean.Grind.AC.Var)
                (s₂ : Lean.Grind.AC.Seq),
                Nat.blt x₁ x₂ = true →
                  motive fuel s₁ (Lean.Grind.AC.Seq.cons x₂ s₂)
                      (Lean.Grind.AC.Seq.unionFuel fuel s₁ (Lean.Grind.AC.Seq.cons x₂ s₂)) →
                    motive fuel.succ (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)
                      (Lean.Grind.AC.Seq.cons x₁
                        (Lean.Grind.AC.Seq.unionFuel fuel s₁ (Lean.Grind.AC.Seq.cons x₂ s₂)))) →
              (∀ (fuel : ℕ) (x₁ : Lean.Grind.AC.Var) (s₁ : Lean.Grind.AC.Seq) (x₂ : Lean.Grind.AC.Var)
                  (s₂ : Lean.Grind.AC.Seq),
                  ¬Nat.blt x₁ x₂ = true →
                    motive fuel (Lean.Grind.AC.Seq.cons x₁ s₁) s₂
                        (Lean.Grind.AC.Seq.unionFuel fuel (Lean.Grind.AC.Seq.cons x₁ s₁) s₂) →
                      motive fuel.succ (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)
                        (Lean.Grind.AC.Seq.cons x₂
                          (Lean.Grind.AC.Seq.unionFuel fuel (Lean.Grind.AC.Seq.cons x₁ s₁) s₂))) →
                ∀ (fuel : ℕ) (s₁ s₂ : Lean.Grind.AC.Seq), motive fuel s₁ s₂ (Lean.Grind.AC.Seq.unionFuel fuel s₁ s₂)
-- Std.Internal.Do.Order.Lemmas
/-- Cancel a redundant `⊓ ⊤` on the left of an entailment.  -/
Std.Internal.Do.CompleteLattice.meet_top_le_of_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel (Lean.Order.meet P Lean.Order.top) Q
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g)
      f'
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft.default : Mathlib.Tactic.BicategoryLike.WhiskerLeft
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit of `F.leftOp : Jᵒᵖ ⥤ C` into a colimit of `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isColimitCoconeOfConeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F.leftOp} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c)
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.instContinuousFunctionalCalculusIsClosedEmbedding : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  ClosedEmbeddingContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint
-- Lean.Meta.Match.SimpH
/-- Auxiliary tactic that tries to replace as many variables as possible and then apply `contradiction`.
We use it to discard redundant hypotheses.
 -/
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.trySubstVarsAndContradiction : Lean.MVarId → optParam Lean.FVarIdSet ∅ → Lean.MetaM Bool
-- Lean.CoreM
Lean.DeclNameGenerator.next : Lean.DeclNameGenerator → Lean.DeclNameGenerator
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.Model.ForwardSliceSearcher.instLawfulForwardPatternModel : ∀ {pat : String.Slice}, String.Slice.Pattern.Model.LawfulForwardPatternModel pat
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.torsionMulEquiv_symm_apply_coe`. -/
Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : CommMonoid G] (tG : IsMulTorsion G) (a : G), ↑(tG.torsionMulEquiv.symm a) = a
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List (α × β)},
  (Std.DHashMap.Raw.Const.ofList l).WF
-- Mathlib.Tactic.Abel
/-- True if this represents an atomic expression.  -/
Mathlib.Tactic.Abel.NormalExpr.isAtom : Mathlib.Tactic.Abel.NormalExpr → Bool
-- Mathlib.Analysis.Convex.Independent
/-- If a family is convex independent, so is any subfamily indexed by a subtype of the index type.
 -/
ConvexIndependent.subtype : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → ∀ (s : Set ι), ConvexIndependent 𝕜 fun i => p ↑i
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_and : ∀ (a b : BitVec 64), { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An action is preprimitive if it is pretransitive and
the only blocks are the trivial ones  -/
MulAction.IsPreprimitive : (G : Type u_1) → (X : Type u_2) → [SMul G X] → Prop
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_anti : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s} {t : Set α} {x : α} (h : s ⊆ t), ↑((Order.enum t ⋯) x) ≤ ↑((Order.enum s hs) x)
-- Mathlib.Probability.Distributions.Gaussian.Basic
InnerProductSpace.toDual.eq_1 : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E],
  InnerProductSpace.toDual 𝕜 E = LinearIsometryEquiv.ofSurjective (InnerProductSpace.toDualMap 𝕜 E) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_sdiff : ∀ {V : Type u} (s t : Set (Sym2 V)),
  SimpleGraph.fromEdgeSet (s \ t) = SimpleGraph.fromEdgeSet s \ SimpleGraph.fromEdgeSet t
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pell_val : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.pell a1 n = (Pell.xn a1 n, Pell.yn a1 n)
-- Init.Data.SInt.Bitwise
Int16.or_not_self : ∀ {a : Int16}, a ||| ~~~a = -1
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.le_of_lt_succFn : ∀ {ι : Type u_1} [inst : LinearOrder ι] (j i : ι), j < LinearLocallyFiniteOrder.succFn i → j ≤ i
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Descend along an effective epi family.  -/
CategoryTheory.EffectiveEpiFamily.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B W : C} →
      {α : Type u_2} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            [CategoryTheory.EffectiveEpiFamily X π] →
              (e : (a : α) → X a ⟶ W) →
                (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                    CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
                      CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
                  (B ⟶ W)
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algHom_of_minpoly_eq : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  (∀ (x : E), ∃ y, minpoly F x = minpoly F y) → Nonempty (E →ₐ[F] K)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_finset_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {s : Finset β}
  {t : β → Set α}, MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_T_eval_one_dvd : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] (n : ℤ) (k : ℕ),
  ↑(∏ l ∈ Finset.range k, (2 * l + 1)) ∣ ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.q : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w) → self.aig.RefVec w