mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form, finite case: a finite semisimple algebra is
isomorphic to a product of matrix algebras over finite division algebras.  -/
IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSemisimpleRing R]
  [Module.Finite R₀ R],
  ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
-- Init.Data.String.Substring
/-- If `pre` is a prefix of `s`, returns the remainder. Returns `none` otherwise.

The substring `pre` is a prefix of `s` if there exists a `t : Substring` such that
`s.toString = pre.toString ++ t.toString`. If so, the result is the substring of `s` without the
prefix.
 -/
Substring.Raw.dropPrefix? : Substring.Raw → Substring.Raw → Option Substring.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.isKernelCompMono_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c) {Z : C} (g : Y ⟶ Z)
  [hg : CategoryTheory.Mono g] {h : X ⟶ Z} (hh : h = CategoryTheory.CategoryStruct.comp f g)
  (s : CategoryTheory.Limits.KernelFork h),
  (CategoryTheory.Limits.isKernelCompMono i g hh).lift s =
    i.lift (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fork.ι s) ⋯)
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, Std.HashMap.unitOfList [] = ∅
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.bot_lt_log_iff : ∀ {x : ENNReal}, ⊥ < x.log ↔ 0 < x
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_add : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] [inst_1 : DecidableEq I] (f₁ f₂ : (i : I) → f i) (i : I)
  (x₁ x₂ : f i), Function.update (f₁ + f₂) i (x₁ + x₂) = Function.update f₁ i x₁ + Function.update f₂ i x₂
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁.eq_1 : ∀ (p t x : ℝ), p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - (t + x)⁻¹)
-- Mathlib.Order.CompleteLattice.Basic
iInf_plift_down : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : ι → α), ⨅ i, f i.down = ⨅ i, f i
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The augmented Čech nerve associated to a split epimorphism has an extra degeneracy.  -/
CategoryTheory.Arrow.AugmentedCechNerve.extraDegeneracy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (f : CategoryTheory.Arrow C) →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        CategoryTheory.SplitEpi f.hom → f.augmentedCechNerve.ExtraDegeneracy
-- Mathlib.Algebra.GroupWithZero.Invertible
/-- A variant of `Ring.inverse_unit`.  -/
Ring.inverse_invertible : ∀ {α : Type u} [inst : MonoidWithZero α] (x : α) [inst_1 : Invertible x], Ring.inverse x = ⅟x
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.ofObj_le_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C)
  (P : CategoryTheory.ObjectProperty C), CategoryTheory.ObjectProperty.ofObj X ≤ P ↔ ∀ (i : ι), P (X i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Paste two pushout squares "vertically" to obtain another pushout square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPushout.paste_vert : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁ →
      CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
        (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mem_top : ∀ {M : Type u_1} [inst : AddZeroClass M] {x : M}, x ∈ ⊤
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.skipWhile.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (nextCurr : s.Pos) → motive (some nextCurr))
  (h_2 : Unit → motive none),
  (match none with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.homologicalComplexToDGO_map_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y)
  (i : β), ((HomologicalComplex.homologicalComplexToDGO b V).map f).f i = f.f i
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for checking grind pattern constraints of the form `size e < threshold`
Implicit arguments and type information in lambdas and let-expressions are ignored.
 -/
Lean.Meta.Grind.EMatch.checkSize : Lean.Expr → ℕ → Lean.MetaM Bool
-- Lean.Server.Completion.CompletionCollectors
/-- Monad used for completion computation that allows modifying a completion `State` and reading
`CompletionParams`.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.M : Type → Type
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_re : ∀ {R : Type u_1} {a b : R} (r : R) [inst : CommSemiring R], ((algebraMap R (QuadraticAlgebra R a b)) r).re = r
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical inclusion `R → TrivSqZeroExt R M`.  -/
TrivSqZeroExt.inl : {R : Type u} → {M : Type v} → [Zero M] → R → TrivSqZeroExt R M
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
/-- The endomorphism `PInfty : K[X] ⟶ K[X]` obtained from the `P q` by passing to the limit.  -/
AlgebraicTopology.DoldKan.PInfty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X
-- Mathlib.Data.List.Perm.Lattice
List.Perm.bagInter : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ t₁ t₂ : List α},
  l₁.Perm l₂ → t₁.Perm t₂ → (l₁.bagInter t₁).Perm (l₂.bagInter t₂)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffAt_section_of_subsingleton : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {x : B}
  [Subsingleton F], ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x
-- Init.Data.SInt.Lemmas
Int8.toInt_minValue : Int8.minValue.toInt = -2 ^ 7
-- Init.Data.SInt.Lemmas
ISize.toInt8_neg : ∀ (x : ISize), (-x).toInt8 = -x.toInt8
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_eq_iff_eq_sq : ∀ {x y : NNReal}, NNReal.sqrt x = y ↔ x = y ^ 2
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_inv : ∀ {r : NNReal}, r ≠ 0 → ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.RingTheory.RingHomProperties
RingHom.CodescendsAlong.and : ∀ {P Q P' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => P) fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => P') fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f => P f ∧ P' f)
        fun {R S} [CommRing R] [CommRing S] => Q
-- Init.Grind.AC
Lean.Grind.AC.diseq_erase_dup : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.IdempotentOp ctx.op}
  (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase_dup_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs ≠ Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_continuousLinearMap_comp : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedAddCommGroup H] {μ : MeasureTheory.VectorMeasure X F} [inst_4 : NormedSpace ℝ E]
  [inst_5 : NormedSpace ℝ F] [inst_6 : NormedSpace ℝ G] [inst_7 : NormedSpace ℝ H] {B : E →L[ℝ] F →L[ℝ] G} {f : X → H}
  {C : H →L[ℝ] E}, MeasureTheory.Integrable f μ.variation → ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddZeroClass β]
  [inst_3 : ContinuousAdd β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.FreeMonoidal.μIso_inv_freeMk : ∀ (R : Type u) [inst : CommRing R] {X Y : Type u} (z : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.FreeMonoidal.μIso R X Y).inv) (ModuleCat.freeMk z) =
    ModuleCat.freeMk z.1 ⊗ₜ[R] ModuleCat.freeMk z.2
-- Mathlib.Data.List.GetD
List.getD_default_eq_getI : ∀ {α : Type u} (l : List α) [inst : Inhabited α] {n : ℕ}, l.getD n default = l.getI n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The "second projection" of a CatCommSqOver as a functor.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
                      (CategoryTheory.Functor X C)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- Given a family of opens `U : ι → Opens X` and any open `Y : Opens X`, we obtain a presieve
on `Y` by declaring that a morphism `f : V ⟶ Y` is a member of the presieve if and only if
there exists an index `i : ι` such that `V = U i`.
 -/
TopCat.Presheaf.presieveOfCoveringAux : {X : TopCat} →
  {ι : Type v} → (ι → TopologicalSpace.Opens ↑X) → (Y : TopologicalSpace.Opens ↑X) → CategoryTheory.Presieve Y
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- `FractionalIdeal.mul` is the product of two fractional ideals,
used to define the `Mul` instance.

This is only an auxiliary definition: the preferred way of writing `I.mul J` is `I * J`.

Elaborated terms involving `FractionalIdeal` tend to grow quite large,
so by making definitions irreducible, we hope to avoid deep unfolds.
 -/
FractionalIdeal.mul : {R : Type u_3} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_4} →
        [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P → FractionalIdeal S P → FractionalIdeal S P
-- Lean.Meta.ArgsPacker
/-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
return the function index that is called and the arguments individually.

We expect precisely the expressions produced by `pack`, with manifest
`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
rather than using projections.
 -/
Lean.Meta.ArgsPacker.unpack : Lean.Meta.ArgsPacker → Lean.Expr → Option (ℕ × Array Lean.Expr)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_congr : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
  A = B → schnirelmannDensity A = schnirelmannDensity B
-- Mathlib.Topology.CompactOpen
/-- `C(·, Z)` is a functor.  -/
ContinuousMap.continuous_precomp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : C(X, Y)), Continuous fun g => g.comp f
-- Init.Core
imp.swap : ∀ {a b c : Prop}, a → b → c ↔ b → a → c
-- Std.Do.PostCond
Std.Do.PostShape.except.injEq : ∀ (ε : Type u) (a : Std.Do.PostShape) (ε_1 : Type u) (a_1 : Std.Do.PostShape),
  (Std.Do.PostShape.except ε a = Std.Do.PostShape.except ε_1 a_1) = (ε = ε_1 ∧ a = a_1)
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- the top morphism in the square  -/
CategoryTheory.SmallObject.FunctorObjIndex.t : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        {f : (i : I) → A i ⟶ B i} →
          {S X : C} → {πX : X ⟶ S} → (self : CategoryTheory.SmallObject.FunctorObjIndex f πX) → A self.i ⟶ X
-- Mathlib.Algebra.Opposites
AddOpposite.instVAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β],
  AddOpposite.instVAdd = { vadd := fun c x => AddOpposite.op (c +ᵥ AddOpposite.unop x) }
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIsoClass.toOrderMonoidIso.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : EquivLike F α β] [inst_5 : OrderIsoClass F α β] [inst_6 : MulEquivClass F α β]
  (f : F), ↑f = { toMulEquiv := ↑f, map_le_map_iff' := ⋯ }
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.trans_ssubset`.

---

Set notation form of `LE.le.trans_lt` -/
HasSubset.Subset.trans_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊆ b → b ⊂ c → a ⊂ c
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_iInf_mul_iInf : ∀ {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} {g : κ → ENNReal},
  (∃ i, f i ≠ ⊤) → (∃ j, g j ≠ ⊤) → (∀ (i : ι) (j : κ), a ≤ f i * g j) → a ≤ (⨅ i, f i) * ⨅ j, g j
-- Mathlib.SetTheory.Cardinal.Subfield
_private.Mathlib.SetTheory.Cardinal.Subfield.0.Subfield.surjective_ofWType : ∀ {α : Type u} (s : Set α) [inst : DivisionRing α],
  Function.Surjective (WType.elim (↥(Subfield.closure s)) (Subfield.operate✝ s))
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq_some_getElem : ∀ {w : ℕ} (l : BitVec w) (i : ℕ) (h : i < w), l[i]? = some l[i] ↔ True
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.oproj.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7),
  sizeOf (Lean.Compiler.LCNF.LetValue.oproj i var h) = 1 + sizeOf i + sizeOf var + sizeOf h
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁_map_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₁ A))
  (g : G), (A.ρ g) (f g⁻¹) = -f g
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s : Set M}, PointedCone.dual p (-s) = -PointedCone.dual p s
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  step = none →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.IsLimit.assoc_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y}
  {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY)
  (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z}
  (R : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)),
  (P.assoc Q R).lift t = R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t)
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_id : ∀ (α : Type u_2) [inst : TopologicalSpace α] [inst_1 : Preorder α], ⇑(EsakiaHom.id α) = id
-- Mathlib.Data.Nat.Totient
Nat.totient_gcd_mul_totient_mul : ∀ (a b : ℕ), (a.gcd b).totient * (a * b).totient = a.totient * b.totient * a.gcd b
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i j : Fin (n + 1)),
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (self.h j) (Y.σ i.castSucc) =
      CategoryTheory.CategoryStruct.comp (X.σ i) (self.h j.succ)
-- Std.Http.Data.Body.Length
Std.Http.Body.Length.chunked.sizeOf_spec : sizeOf Std.Http.Body.Length.chunked = 1
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforward_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y)
  {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X_1 ⟶ Y_1)
  (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.pushforward C f).map α).app X_2 =
    α.app (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X_2)))
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K]
  [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj],
  CategoryTheory.Limits.PreservesColimitsOfShape K J.yoneda
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- If `M ≤ N` are submonoids of `R`, then `N⁻¹S` is also the localization of `M⁻¹S` at `N`.  -/
IsLocalization.isLocalization_of_submonoid_le : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (M N : Submonoid R),
  M ≤ N →
    ∀ [IsLocalization M S] [IsLocalization N T] [inst_7 : Algebra S T] [IsScalarTower R S T],
      IsLocalization (Submonoid.map (algebraMap R S) N) T
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
-- Init.Prelude
Lean.instMonadRefOfMonadLiftOfMonadFunctor : (m n : Type → Type) → [MonadLift m n] → [MonadFunctor m n] → [Lean.MonadRef m] → Lean.MonadRef n
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.setLIntegral_tilted' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) (g : α → ENNReal) {s : Set α},
  MeasurableSet s →
    ∫⁻ (x : α) in s, g x ∂μ.tilted f =
      ∫⁻ (x : α) in s, ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * g x ∂μ
-- Mathlib.Logic.Equiv.Sum
Equiv.sumSigmaDistrib_apply : ∀ {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (x : (i : α ⊕ β) × t i),
  (Equiv.sumSigmaDistrib t) x =
    match x with
    | ⟨Sum.inl x, y⟩ => Sum.inl ⟨x, y⟩
    | ⟨Sum.inr x, y⟩ => Sum.inr ⟨x, y⟩
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The canonical isomorphism between `(trianglehOfDegreewiseSplit S σ).rotate.rotate` and
`mappingCone.triangleh (homOfDegreewiseSplit S σ)` when `S` is a degreewise split
short exact sequence of cochain complexes.  -/
CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            (CochainComplex.trianglehOfDegreewiseSplit S σ).rotate.rotate ≅
              CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ)
-- Mathlib.Data.Finset.Image
Finset.map_filter' : ∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) [inst : DecidablePred p] (f : α ↪ β) (s : Finset α)
  [inst_1 : DecidablePred fun x => ∃ a, p a ∧ f a = x],
  Finset.map f (Finset.filter p s) = {b ∈ Finset.map f s | ∃ a, p a ∧ f a = b}
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instFaithfulOppositeTypeRestrictedULiftYonedaOfIsDense : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsDense], (CategoryTheory.Presheaf.restrictedULiftYoneda F).Faithful
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.unfold_smulg : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℕ) (x y : α), Mathlib.Tactic.Abel.smulg (Int.ofNat n) x = y → ↑n • x = y
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of indexed infimum on function lattices.  -/
Lean.Order.iInf_apply : ∀ {ι : Type v} {σ : Type w} {β : Type u} [inst : Lean.Order.CompleteLattice β] (f : ι → σ → β) (s : σ),
  Lean.Order.iInf f s = Lean.Order.iInf fun i => f i s
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.dep_of_ssubset : ∀ {α : Type u_1} {M : Matroid α} {B X : Set α},
  M.IsBase B → B ⊂ X → autoParam (X ⊆ M.E) Matroid.IsBase.dep_of_ssubset._auto_1 → M.Dep X
-- Mathlib.Order.CompleteLattice.Basic
Monotone.le_map_iSup₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] {f : α → β},
  Monotone f → ∀ (s : (i : ι) → κ i → α), ⨆ i, ⨆ j, f (s i j) ≤ f (⨆ i, ⨆ j, s i j)