mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection], U.starProjection = U.subtypeL ∘SL U.orthogonalProjectionOnto
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω),
  MeasurableSet s ↔ MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
-- Mathlib.GroupTheory.Complement
AddSubgroup.instInhabitedLeftTransversal : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → Inhabited H.LeftTransversal
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isNatCastInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The flat sections of a functor into `AddMonCat` form an additive submonoid of all sections.  -/
AddMonCat.sectionsAddSubmonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) → AddSubmonoid ((j : J) → ↑(F.obj j))
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_of_eq : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, toZ i0 i0 = 0
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.depthLt : Lean.Parser.Parser
-- Mathlib.Data.List.Dedup
List.count_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a : α), List.count a l.dedup = if a ∈ l then 1 else 0
-- Mathlib.Topology.UniformSpace.Path
/-- The function `Path.trans` that concatenates two paths `γ₁ : Path x y` and `γ₂ : Path y z`
is uniformly continuous in `(γ₁, γ₂)`.  -/
Path.uniformContinuous_trans : ∀ {X : Type u_1} [inst : UniformSpace X] {x y z : X}, UniformContinuous (Function.uncurry Path.trans)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` contains the monoid's 0.  -/
AddSubmonoid.zero_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), 0 ∈ S
-- Mathlib.Data.Complex.Basic
Complex.im_ofScientific : ∀ (m : ℕ) (s : Bool) (e : ℕ), Complex.im (OfScientific.ofScientific m s e) = 0
-- Std.Do.Triple.Basic
Std.Do.Triple.of_entails_wp : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond α ps}, (P ⊢ₛ (Std.Do.wp x).apply Q) → ⦃P⦄ x ⦃Q⦄
-- Mathlib.Probability.Decision.Risk.Basic
/-- For a bounded loss, the Bayes risk with respect to a prior is finite.  -/
ProbabilityTheory.bayesRisk_lt_top : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Nonempty 𝓨] (P : ProbabilityTheory.Kernel Θ 𝓧)
  [ProbabilityTheory.IsFiniteKernel P] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] {C : NNReal},
  (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.bayesRisk ℓ P π < ⊤
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Ioo i j) = Finset.Ioo (i.addNat m) (j.addNat m)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
      (self.mapComp f g')
-- Mathlib.Analysis.Normed.Order.Lattice
/-- Let `α` be a normed lattice ordered group. Then `α` is a topological lattice in the norm topology.
 -/
HasSolidNorm.toTopologicalLattice : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  TopologicalLattice α
-- Init.Data.Vector.Lemmas
Vector.any_congr : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n},
  xs = ys → ∀ {p q : α → Bool}, (∀ (a : α), p a = q a) → xs.any p = ys.any q
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite coproducts, then `F.unop : C ⥤ D` creates finite
products.  -/
CategoryTheory.Limits.createsFiniteProductsUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteCoproducts F] → CategoryTheory.Limits.CreatesFiniteProducts F.unop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).support = List.take (n + 1) p.support
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- An element `ζ` is a primitive `k`-th root of unity if `ζ ^ k = 1`,
and if `l` satisfies `ζ ^ l = 1` then `k ∣ l`.  -/
IsPrimitiveRoot : {M : Type u_1} → [CommMonoid M] → M → ℕ → Prop
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.trans : ∀ {p : Prop} {a b m c b' c' : ℕ},
  Mathlib.Meta.NormNum.IsNatPowModT p a b m c →
    Mathlib.Meta.NormNum.IsNatPowModT ((a.pow b).mod m = c) a b' m c' → Mathlib.Meta.NormNum.IsNatPowModT p a b' m c'
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_ofCoeff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (f : G →₀ k), { coeff := f }.coeff = f
-- Lean.Parser.Extension
Lean.Parser.builtinTokenTable : IO.Ref Lean.Parser.TokenTable
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive :
          (n : ℕ) →
            ((a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
              Sort u_2) →
        (n : ℕ) →
          (recur :
              (a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
            ((recur :
                  (a' : Std.Iter β) →
                    (b' : ℕ) →
                      InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                          (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
                        Option β) →
                motive 0 recur) →
              ((k : ℕ) →
                  (recur :
                      (a' : Std.Iter β) →
                        (b' : ℕ) →
                          InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                              (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                            Option β) →
                    motive k.succ recur) →
                motive n recur
-- Mathlib.Analysis.Complex.Tietze
RCLike.instTietzeExtension : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], TietzeExtension 𝕜
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k : α} {fallback : β} {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.modify k f t) k fallback =
        (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.compl : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage sᶜ tᶜ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul.eq_1 : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  MeasureTheory.condExpIndSMul hm hs hμs x =
    (ContinuousLinearMap.compLpL 2 μ (ContinuousLinearMap.toSpanSingleton ℝ x))
      ↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_mul : ∀ (a b : BitVec 16), Int16.ofBitVec (a * b) = Int16.ofBitVec a * Int16.ofBitVec b
-- Mathlib.Algebra.Opposites
AddOpposite.op_unop : ∀ {α : Type u_1} (x : αᵃᵒᵖ), AddOpposite.op (AddOpposite.unop x) = x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.mk.inj : ∀ {p : Int.Internal.Linear.Poly} {h : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof} {p_1 : Int.Internal.Linear.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeLinearEquiv_apply : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : AddCommMonoid α] [inst_3 : StarAddMonoid α] [inst_4 : Module R α] [inst_5 : StarModule R α]
  (a : Matrix m n α), (Matrix.conjTransposeLinearEquiv m n R α) a = (Matrix.conjTransposeAddEquiv m n α).toFun a
-- Mathlib.Logic.Function.ULift
PLift.down_injective : ∀ {α : Sort u_1}, Function.Injective PLift.down
-- Mathlib.Algebra.Quaternion
Quaternion.im_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), (↑q).im = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecomposeEquivalenceFunctor =
    CategoryTheory.Limits.Cocone.extInv
      (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocone.precomposeEquivalence α).functor.obj c)).pt)
      ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.OuterMeasure.toMeasure_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, ⊤.toMeasure ⋯ = ⊤
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.inclusion_map : ∀ {C : Type u} {X Y : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C}
  (f : X ⟶ Y), CategoryTheory.FreeMonoidalCategory.inclusion.map f = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Convex.ContinuousLinearEquiv
ContinuousLinearEquiv.strictConvex_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F]
  [inst_7 : TopologicalSpace F] {s : Set F} (e : E ≃L[𝕜] F), StrictConvex 𝕜 (⇑e ⁻¹' s) ↔ StrictConvex 𝕜 s
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.internalError.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.internalError = 1
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_ne_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], ⊥ ≠ 1
-- Init.Data.Array.Attach
/-- This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Array.map_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → β} {g : α → β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.map f xs = Array.map g xs.unattach
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.ite' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} {p : Prop},
  (p → MeasurableSet s) → (¬p → MeasurableSet t) → MeasurableSet (if p then s else t)
-- Mathlib.Topology.ClusterPt
clusterPt_principal_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : X) in nhds x, y ∈ s
-- Mathlib.Topology.VectorBundle.Basic
/-- Analogous construction of `FiberBundleCore` for vector bundles. This
construction gives a way to construct vector bundles from a structure registering how
trivialization changes act on fibers.  -/
VectorBundleCore : (R : Type u_1) →
  (B : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [NormedSpace R F] → [TopologicalSpace B] → Type u_5 → Type (max (max u_2 u_3) u_5)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_15.splitter : (C : Type u_1) →
  (motive : CategoryTheory.WithInitial Cᵒᵖ → Sort u_2) →
    (x : CategoryTheory.WithInitial Cᵒᵖ) →
      ((x : Cᵒᵖ) → motive (CategoryTheory.WithInitial.of x)) →
        (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.priorParts : Lean.VersoModuleDocs.DocFrame✝ → Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor C E),
  e.congrLeft.unitIso.inv.app X = (e.funInvIdAssoc X).hom
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant ring homomorphism as an equivariant additive monoid homomorphism.  -/
MulSemiringActionHom.toDistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} → [inst_4 : Semiring S] → [inst_5 : MulSemiringAction N S] → (R →ₑ+*[φ] S) → R →ₑ+[φ] S
-- Lean.Elab.PreDefinition.Structural.IndPred
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.replaceIndPredRecApp : Lean.Elab.Structural.RecArgInfo →
  Lean.Meta.IndPredBelow.RecursionContext →
    ℕ → Lean.Elab.Structural.Positions → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Logic.Equiv.Defs
Equiv.comp_symm_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubNegMonoid : {α : Type u_1} → [SubNegMonoid α] → SubNegMonoid αᵃᵒᵖ
-- Mathlib.RingTheory.DedekindDomain.SInteger
/-- If `S` is the empty set, then the `S`-integers are the minimal `R`-subalgebra of `K` (which is
just `R` itself, via `Algebra.botEquivOfInjective` and `IsFractionRing.injective`).  -/
IsDedekindDomain.integer_empty : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K], ∅.integer K = ⊥
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_algebra_smul : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k)
  (c : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
  (x : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)),
  SMul.smul c x =
    (MvPolynomial.aeval (Sum.elim (fun x => MvPolynomial.X x ⊗ₜ[R] 1) fun x => 1 ⊗ₜ[R] MvPolynomial.X x)).toRingHom c *
      x
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.incidenceFinset_subset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V]
  [inst_2 : Fintype ↑G.edgeSet], G.incidenceFinset v ⊆ G.edgeFinset
-- Mathlib.Control.Traversable.Lemmas
Traversable.traverse_comp : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α β γ : Type u} (g : α → F β) (h : β → G γ),
  traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) = Functor.Comp.mk ∘ Functor.map (traverse h) ∘ traverse g
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (x : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (h_1 : Unit → motive none)
  (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false)))
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n),
  x = some (l, true) →
    (match x with
      | none => h_1 ()
      | some (l, true) => h_2 l
      | some (l, false) => h_3 l) ≍
      h_2 l
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingCoeff_nonzero_iff_nonzero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingCoeff ≠ 0 ↔ p ≠ 0
-- Mathlib.RingTheory.Ideal.Over
/-- The ideal obtained by pulling back the ideal `P` from `B` to `A`.  -/
Ideal.under : (A : Type u_2) → [inst : CommSemiring A] → {B : Type u_3} → [inst_1 : Semiring B] → [Algebra A B] → Ideal B → Ideal A
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsHomogeneous.mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R} {p q : ℕ},
  f.IsHomogeneous p → g.IsHomogeneous q → (f * g).IsHomogeneous (p + q)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
  {g : (i : ι) → E → F i →L[𝕜] G i} {g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i} {x : E} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι],
  HasStrictFDerivAt f f' x →
    (∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x) →
      HasStrictFDerivAt (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.compContinuousLinearMapL fun x_1 => g x_1 x) ∘SL f' +
          ((f x).fderivCompContinuousLinearMap fun x_1 => g x_1 x) ∘SL ContinuousLinearMap.pi g')
        x
-- Lean.Elab.PreDefinition.Structural.IndPred
/-- Monad for inductive predicate recursion that accumulates matcher creation side-effects.  -/
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.IndPredM : Type → Type
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_modify : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m] (s : σ)
  (f : σ → σ),
  (do
      set s
      modify f) =
    set (f s)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.C_inv : ∀ {k : Type u_2} [inst : Field k] (r : k), (PowerSeries.C r)⁻¹ = PowerSeries.C r⁻¹
-- Mathlib.Logic.Relator
/-- A relation is "left unique" if every element on the right is paired with at
most one element on the left.  -/
Relator.LeftUnique : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y] (e : X ≃* Y),
  e.toMonCatIso =
    { hom := MonCat.ofHom e.toMonoidHom, inv := MonCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J) {Z : C} (h : G.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j)
      (CategoryTheory.CategoryStruct.comp (α.app j) h)
-- Mathlib.Util.Superscript
/-- Loop body of `satisfyTokensFn`  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.satisfyTokensFn.loop : (Char → Bool) →
  (Array (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) → Lean.Parser.ParserState → Lean.Parser.ParserState) →
    Lean.Parser.ParserContext →
      Array (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.δ_comp_σ_self : ∀ {n : ℕ} {i : Fin (n + 1)},
  FreeSimplexQuiver.homRel
    (CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc))
      ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
    (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk n)))
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is an `n`-smooth number if the `Finset` of its prime factors consists of numbers `< n`.  -/
Nat.mem_smoothNumbers_of_primeFactors_subset : ∀ {m n : ℕ}, m ≠ 0 → m.primeFactors ⊆ Finset.range n → m ∈ n.smoothNumbers
-- Mathlib.Dynamics.Flow
Flow.mk.inj : ∀ {τ : Type u_1} {α : Type u_2} {inst : TopologicalSpace τ} {inst_1 : TopologicalSpace α} {inst_2 : AddZero τ}
  {toFun : τ → α → α} {cont' : Continuous (Function.uncurry toFun)}
  {map_add' : ∀ (t₁ t₂ : τ) (x : α), toFun (t₁ + t₂) x = toFun t₁ (toFun t₂ x)} {map_zero' : ∀ (x : α), toFun 0 x = x}
  {toFun_1 : τ → α → α} {cont'_1 : Continuous (Function.uncurry toFun_1)}
  {map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), toFun_1 (t₁ + t₂) x = toFun_1 t₁ (toFun_1 t₂ x)}
  {map_zero'_1 : ∀ (x : α), toFun_1 0 x = x},
  { toFun := toFun, cont' := cont', map_add' := map_add', map_zero' := map_zero' } =
      { toFun := toFun_1, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } →
    toFun = toFun_1
-- Init.Internal.Order.Basic
Lean.Order.iterates.brecOn : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} {motive : (a : α) → Lean.Order.iterates f a → Prop} {a : α}
  (t : Lean.Order.iterates f a),
  (∀ (a : α) (t : Lean.Order.iterates f a), Lean.Order.iterates.below t → motive a t) → motive a t
-- Std.Sat.AIG.Basic
/-- An AIG gate with configurable input nodes and polarity. `l` and `r` are the
input nodes together with their inverter bit.
 -/
Std.Sat.AIG.Decl.gate : {α : Type} → Std.Sat.AIG.Fanin → Std.Sat.AIG.Fanin → Std.Sat.AIG.Decl α
-- Mathlib.Geometry.Manifold.Riemannian.Basic
instRiemannianBundleTangentSpaceRealModelWithCornersSelf : {F : Type u_4} →
  [inst : NormedAddCommGroup F] →
    [inst_1 : InnerProductSpace ℝ F] → Bundle.RiemannianBundle fun x => TangentSpace (modelWithCornersSelf ℝ F) x
-- Lean.Data.Position
Lean.Position.instToExpr : Lean.ToExpr Lean.Position
-- Init.Data.Iterators.Basic
/-- Asserts that a certain output value could plausibly be emitted by the given iterator in its next
step.
 -/
Std.IterM.IsPlausibleOutput : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → β → Prop