mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Tactics
/-- `decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
and then reducing that instance to evaluate the truth value of `p`.
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.

The target is not allowed to contain local variables or metavariables.
If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target,
or you can use the `+revert` option, described below.

Options:
- `decide +revert` begins by reverting local variables that the target depends on,
  after cleaning up the local context of irrelevant variables.
  A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
  or if it is a proposition that refers to a relevant variable.
- `decide +kernel` uses kernel for reduction instead of the elaborator.
  It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
  and (2) it reduces the `Decidable` instance only once instead of twice.
- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
  admitting the result via an axiom.
  This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
  of the trusted code base.
  Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
  Like with `+kernel`, the `Decidable` instance is evaluated only once.

Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term,
`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms.
These can appear in instances defined using tactics (such as `rw` and `simp`).
To avoid this, create such instances using definitions such as `decidable_of_iff` instead.

## Examples

Proving inequalities:
```lean
example : 2 + 2 ≠ 5 := by decide
```

Trying to prove a false proposition:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
  1 ≠ 1
is false
-/
```

Trying to prove a proposition whose `Decidable` instance fails to reduce
```lean
opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
  unknownProp
since its 'Decidable' instance reduced to
  Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```

## Properties and relations

For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
```lean
example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl
```
 -/
Lean.Parser.Tactic.decide : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a constant and a `C^n` function at a point is `C^n` at this
point.  -/
ContDiffAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {R : Type u_3} [inst_5 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : E → F} {x : E} (c : R),
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun y => c • f y) x
-- Mathlib.Order.Interval.Set.SuccPred
Set.Iio_succ_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (b : α),
  Set.Iio (Order.succ b) = Set.Iic b
-- Lean.Elab.Do.Basic
/-- The `u` in `m : Type u → Type v`.  -/
Lean.Elab.Do.MonadInfo.u : Lean.Elab.Do.MonadInfo → Lean.Level
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B), ⇑↑f = ⇑f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k}, (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.restrict.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ φ_1 : S →ₐ[R] S}
  (e_φ : φ = φ_1) {Q : Ideal S} (H : φ.IsArithFrobAt Q), H.restrict = ⋯.restrict
-- Init.Data.Option.Lemmas
Option.instLawfulIdentityMaxNone : ∀ {α : Type u_1} [inst : Max α], Std.LawfulIdentity max none
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_some_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.min? = some t.min!
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasGaussianLaw (fun ω => X ω + Y ω) P
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_idx_trichotomy : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} {assign : α → Bool} {invert res : Bool}
  {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size},
  (aig.decls[start] = Std.Sat.AIG.Decl.false →
      ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) →
    (∀ (a : α),
        aig.decls[start] = Std.Sat.AIG.Decl.atom a →
          ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) →
      (∀ (lhs rhs : Std.Sat.AIG.Fanin),
          aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs →
            ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res) →
        ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = res
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars.orderIso_symm_apply : ∀ {L : Type u_2} [inst : Field L] (F : Subfield L) (E : IntermediateField (↥F) L),
  (RelIso.symm (Subfield.extendScalars.orderIso F)) E = ⟨E.toSubfield, ⋯⟩
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_cancel : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r : R} {s t : ↥S},
  ↑s /ₒ t * (r /ₒ s) = r /ₒ t
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.fst_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsMarkovKernel η], (κ.prod η).fst = κ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_3 : ∀ {σ₁ σ₂ σ₃ : Type u_1} {P Q : Std.Do.SPred [σ₁, σ₂, σ₃]},
  P ⊢ₛ Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), (P s₁ s₂ s₃).down → (Q s₁ s₂ s₃).down
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.declareRuleSets : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_eq_one : ∀ {R : Type u} [inst : Semiring R] {a : AddMonoidAlgebra R ℕ}, { toFinsupp := a } = 1 ↔ a = 1
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.IdxSet : Type
-- Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
ZMod.trace_pow_card : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {p : ℕ} [inst_2 : Fact (Nat.Prime p)]
  (M : Matrix n n (ZMod p)), (M ^ p).trace = M.trace ^ p
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vInv_vInv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄)
  (B : CategoryTheory.Functor C₃ C₄) (h : CategoryTheory.CatCommSq T L.functor R.functor B),
  CategoryTheory.CatCommSq.vInv B L.symm R.symm T (CategoryTheory.CatCommSq.vInv T L R B h) = h
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a continuous function `c` realizes its maximum at a unique point `x₀` in a compact set `s`,
then the sequence of functions `(c x) ^ n / ∫ (c x) ^ n` is a sequence of peak functions
concentrating around `x₀`. Therefore, `∫ (c x) ^ n * g / ∫ (c x) ^ n` converges to `g x₀` if `g` is
integrable on `s` and continuous at `x₀`.

Version assuming that `μ` gives positive mass to all open sets.
For a less precise but more usable version, see
`tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn`.
 -/
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn : ∀ {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α}
  [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure],
  IsCompact s →
    ∀ {c : α → ℝ},
      ContinuousOn c s →
        (∀ y ∈ s, y ≠ x₀ → c y < c x₀) →
          (∀ x ∈ s, 0 ≤ c x) →
            0 < c x₀ →
              x₀ ∈ closure (interior s) →
                MeasureTheory.IntegrableOn g s μ →
                  ContinuousWithinAt g s x₀ →
                    Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ)
                      Filter.atTop (nhds (g x₀))
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoDiv hp a (b - OfNat.ofNat m * p) = toIcoDiv hp a b - OfNat.ofNat m
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.coe_δ : ∀ {n : ℕ} (i : Fin (n + 2)), ⇑(CategoryTheory.ConcreteCategory.hom (SimplexCategory.δ i)) = i.succAbove
-- Mathlib.Geometry.Manifold.Complex
/-- If a function `f : M → F` from a complex manifold to a complex normed space is holomorphic on a
(pre)connected compact open set, then it is a constant on this set.  -/
MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M}
  {a b : M}, MDiff[U] f → IsPreconnected U → IsCompact U → IsOpen U → a ∈ U → b ∈ U → f a = f b
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.InftyValuation.map_add_le_max' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (x y : RatFunc F),
  RatFunc.inftyValuationDef F (x + y) ≤ max (RatFunc.inftyValuationDef F x) (RatFunc.inftyValuationDef F y)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_1 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property none)
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨none, h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_1 h'
-- Mathlib.Tactic.Polynomial.Core
/-- An extension for `polynomial`.  -/
Mathlib.Tactic.Polynomial.PolynomialExt : Type
-- Mathlib.Algebra.Field.Basic
same_sub_div : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, b ≠ 0 → (b - a) / b = 1 - a / b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.RankLeOneStruct.strictMono : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (self : ValuativeRel.RankLeOneStruct R),
  StrictMono ⇑self.emb
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `b` is a binary bicone such that `b.inl` is a kernel of `b.snd`, then `b` is a bilimit
bicone.  -/
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsLimit b.sndKernelFork → b.IsBilimit
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalPresentable X κ],
  (CategoryTheory.uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDidSaveTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidSaveTextDocumentParams
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Ico_eq_of_Icc_pred_eq : ∀ {m n : ℤ} {s : Finset ℤ}, Finset.Icc m (n - 1) = s → Finset.Ico m n = s
-- Mathlib.Data.List.InsertIdx
List.insertIdx_subset_cons : ∀ {α : Type u} (n : ℕ) (a : α) (l : List α), l.insertIdx n a ⊆ a :: l
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → NonUnitalSemiring ↥S
-- Mathlib.MeasureTheory.Function.Piecewise
IndexedPartition.measurable_piecewise : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {s : ι → Set α} {f : ι → α → β}
  [inst_1 : MeasurableSpace β] [Countable ι] (hs : IndexedPartition s),
  (∀ (i : ι), MeasurableSet (s i)) → (∀ (i : ι), Measurable (f i)) → Measurable (hs.piecewise f)
-- Init.Data.List.Nat.TakeDrop
List.length_take : ∀ {α : Type u_1} {i : ℕ} {l : List α}, (List.take i l).length = min i l.length
-- Init.Data.Array.Lemmas
Array.isEmpty_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Array.replicate n a).isEmpty = decide (n = 0)
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.Nonempty.mul_zero : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {s : Finset α}, s.Nonempty → s * 0 = 0
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (i : ℕ),
  (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).hom.f i =
    CategoryTheory.CategoryStruct.id ((AlgebraicTopology.DoldKan.Γ₀.splitting K).N i)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.cancelCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : CancelCommMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.cancelCommMonoid f hf one mul npow =
    { toCommMonoid := Function.Injective.commMonoid f hf one mul npow, toIsLeftCancelMul := ⋯ }
-- Mathlib.Order.WithBot
WithTop.instOrderBot.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α], WithTop.instOrderBot = { toBot := WithTop.instBot, bot_le := ⋯ }
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `AdjoinRoot f` is indeed given by adjoining a root of `f`. If `f` is monic this is more
powerful than `AdjoinRoot.isAdjoinRoot`.  -/
AdjoinRoot.isAdjoinRootMonic : {R : Type u} → [inst : CommRing R] → (f : Polynomial R) → f.Monic → IsAdjoinRootMonic (AdjoinRoot f) f
-- Lean.Exception
/-- Lift from `Except KernelException` to `m` when `m` can throw kernel exceptions.  -/
Lean.ofExceptKernelException : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadOptions m] → Except Lean.Kernel.Exception α → m α
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- If this constant application could delaborate using generalized field notation with little confusion,
returns the field name and the index for the argument to be used as the object of the field notation.
Otherwise it fails.
 -/
_private.Lean.PrettyPrinter.Delaborator.FieldNotation.0.Lean.PrettyPrinter.Delaborator.generalizedFieldInfo : Lean.Name → Array Lean.Expr → Lean.MetaM (Lean.Name × ℕ)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.pentagon : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {W X Y Z : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramNatTrans_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C),
  J.diagramNatTrans (CategoryTheory.CategoryStruct.comp η γ) X =
    CategoryTheory.CategoryStruct.comp (J.diagramNatTrans η X) (J.diagramNatTrans γ X)
-- Std.Http.Data.Status
/-- 507 Insufficient Storage
 -/
Std.Http.Status.insufficientStorage : Std.Http.Status
-- Mathlib.Order.Hom.Lattice
/-- We can regard an injective map preserving binary infima as an order embedding.  -/
orderEmbeddingOfInjective : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : SemilatticeInf α] →
          [inst_2 : SemilatticeInf β] → (f : F) → [InfHomClass F α β] → Function.Injective ⇑f → α ↪o β
-- Mathlib.Algebra.Algebra.Hom
RingHom.equivIntAlgHom_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] (self : R →ₐ[ℤ] S),
  (RingHom.equivIntAlgHom R S).symm self = self.toRingHom
-- Mathlib.Topology.Homotopy.Path
/-- A path `Path x₀ x₁` generates a homotopy between constant functions `fun _ ↦ x₀` and
`fun _ ↦ x₁`.  -/
Path.toHomotopyConst : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {x₀ x₁ : X} → Path x₀ x₁ → (ContinuousMap.const Y x₀).Homotopy (ContinuousMap.const Y x₁)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forM_eq_forM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → m PUnit.{w + 1}},
  (forM t fun a => f a.1) = t.keys.forM f
-- Std.Async.Process
Std.IO.Process.ResourceUsageStats.mk.injEq : ∀ (cpuUserTime cpuSystemTime : Std.Time.Millisecond.Offset)
  (peakResidentSetSizeKb sharedMemorySizeKb unsharedDataSizeKb unsharedStackSizeKb minorPageFaults majorPageFaults
    swapOperations blockInputOps blockOutputOps messagesSent messagesReceived signalsReceived voluntaryContextSwitches
    involuntaryContextSwitches : UInt64)
  (cpuUserTime_1 cpuSystemTime_1 : Std.Time.Millisecond.Offset)
  (peakResidentSetSizeKb_1 sharedMemorySizeKb_1 unsharedDataSizeKb_1 unsharedStackSizeKb_1 minorPageFaults_1
    majorPageFaults_1 swapOperations_1 blockInputOps_1 blockOutputOps_1 messagesSent_1 messagesReceived_1
    signalsReceived_1 voluntaryContextSwitches_1 involuntaryContextSwitches_1 : UInt64),
  ({ cpuUserTime := cpuUserTime, cpuSystemTime := cpuSystemTime, peakResidentSetSizeKb := peakResidentSetSizeKb,
        sharedMemorySizeKb := sharedMemorySizeKb, unsharedDataSizeKb := unsharedDataSizeKb,
        unsharedStackSizeKb := unsharedStackSizeKb, minorPageFaults := minorPageFaults,
        majorPageFaults := majorPageFaults, swapOperations := swapOperations, blockInputOps := blockInputOps,
        blockOutputOps := blockOutputOps, messagesSent := messagesSent, messagesReceived := messagesReceived,
        signalsReceived := signalsReceived, voluntaryContextSwitches := voluntaryContextSwitches,
        involuntaryContextSwitches := involuntaryContextSwitches } =
      { cpuUserTime := cpuUserTime_1, cpuSystemTime := cpuSystemTime_1,
        peakResidentSetSizeKb := peakResidentSetSizeKb_1, sharedMemorySizeKb := sharedMemorySizeKb_1,
        unsharedDataSizeKb := unsharedDataSizeKb_1, unsharedStackSizeKb := unsharedStackSizeKb_1,
        minorPageFaults := minorPageFaults_1, majorPageFaults := majorPageFaults_1, swapOperations := swapOperations_1,
        blockInputOps := blockInputOps_1, blockOutputOps := blockOutputOps_1, messagesSent := messagesSent_1,
        messagesReceived := messagesReceived_1, signalsReceived := signalsReceived_1,
        voluntaryContextSwitches := voluntaryContextSwitches_1,
        involuntaryContextSwitches := involuntaryContextSwitches_1 }) =
    (cpuUserTime = cpuUserTime_1 ∧
      cpuSystemTime = cpuSystemTime_1 ∧
        peakResidentSetSizeKb = peakResidentSetSizeKb_1 ∧
          sharedMemorySizeKb = sharedMemorySizeKb_1 ∧
            unsharedDataSizeKb = unsharedDataSizeKb_1 ∧
              unsharedStackSizeKb = unsharedStackSizeKb_1 ∧
                minorPageFaults = minorPageFaults_1 ∧
                  majorPageFaults = majorPageFaults_1 ∧
                    swapOperations = swapOperations_1 ∧
                      blockInputOps = blockInputOps_1 ∧
                        blockOutputOps = blockOutputOps_1 ∧
                          messagesSent = messagesSent_1 ∧
                            messagesReceived = messagesReceived_1 ∧
                              signalsReceived = signalsReceived_1 ∧
                                voluntaryContextSwitches = voluntaryContextSwitches_1 ∧
                                  involuntaryContextSwitches = involuntaryContextSwitches_1)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.ExtHashSet.ofList l).size = l.length
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If an indexed family of points is affinely independent, so is the
corresponding set of points.  -/
AffineIndependent.range : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P}, AffineIndependent k p → AffineIndependent k fun x => ↑x
-- Mathlib.Algebra.Group.Action.Pi
Pi.smul'.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → SMul (α i) (β i)],
  Pi.smul' = { smul := fun s x i => s i • x i }
-- Mathlib.Data.Finset.Union
Finset.pairwiseDisjoint_filter : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → Finset β},
  (↑s).PairwiseDisjoint f →
    ∀ (p : β → Prop) [inst : DecidablePred p], (↑s).PairwiseDisjoint fun a => Finset.filter p (f a)