mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ZetaValues
integral_bernoulliFun_eq_zero : ∀ {k : ℕ}, k ≠ 0 → ∫ (x : ℝ) in 0..1, bernoulliFun k x = 0
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker.eq_1 : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Mul α],
  Matrix.kronecker = Matrix.kroneckerMap fun x1 x2 => x1 * x2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α},
  m.WF → (k ∈ Std.HashMap.Raw.filterMap f m ↔ ∃ (g : k ∈ m), (f (m.getKey k g) m[k]).isSome = true)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_20 : HSub Std.Time.Minute.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.orderHom.eq_1 : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N),
  ArchimedeanOrder.orderHom f = { toFun := fun a => ArchimedeanOrder.of (f (ArchimedeanOrder.val a)), monotone' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Construct an adjunction between `F` and `G` out of a natural bijection between each
`F.obj X ⟶ Y` and `X ⟶ G.obj Y`.  -/
CategoryTheory.Adjunction.mkOfHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.CoreHomEquiv F G → (F ⊣ G)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The `K`-algebra automorphisms of `L` are isometries with respect to the spectral norm.  -/
spectralNorm_eq_of_equiv : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] (σ : Gal(L/K)) (x : L),
  spectralNorm K L x = spectralNorm K L (σ x)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the forward direction of `Subgroup.normal_op`. -/
Subgroup.Normal.of_op : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G}, H.op.Normal → H.Normal
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.semiring : {R : Type u} → [inst : Semiring R] → Semiring (Polynomial R)
-- Init.GetElem
/-- Helper function for implementation of `GetElem?.getElem?`.  -/
decidableGetElem? : {coll : Type u_1} →
  {idx : Type u_2} →
    {elem : Type u_3} →
      {valid : coll → idx → Prop} →
        [GetElem coll idx elem valid] → (xs : coll) → (i : idx) → [Decidable (valid xs i)] → Option elem
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, t.size ≤ (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).size
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
/-- If `R` is an injective resolution of `Y`, then `Ext X Y n` identifies
to the group of cohomology classes of degree `n` from `(singleFunctor C 0).obj X`
to `R.cochainComplex`.  -/
CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.InjectiveResolution Y) →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃+
                CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Host.mk.injEq : ∀ (host : Std.Http.URI.Host) (port : Std.Http.URI.Port) (host_1 : Std.Http.URI.Host) (port_1 : Std.Http.URI.Port),
  ({ host := host, port := port } = { host := host_1, port := port_1 }) = (host = host_1 ∧ port = port_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.map_id_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  m.WF → (Std.DHashMap.Raw.map (fun x v => v) m).Equiv m
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.lup : List (List (Option ℕ)) → ℕ × Nat.Partrec.Code → ℕ → Option ℕ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cochainsIso₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.cochainsIso₁ A = (LinearEquiv.funCongrLeft k (↑A) (Equiv.funUnique (Fin 1) G)).toModuleIso.symm
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.nonunits_le : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K}, A.nonunits ≤ A.toNonUnitalSubring
-- Init.Data.Vector.Lemmas
Vector.toList_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (h : i < n), (xs.set i x h).toList = xs.toList.set i x
-- Lean.Expr
/-- `.sort u` is now the preferred form.  -/
Lean.mkSort : Lean.Level → Lean.Expr
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_pos : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : LT α],
  0 < a → 0 < b → 0 < if p then a else b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α},
  (Std.ExtDTreeMap.Const.modify t k f).minKeyD fallback = t.minKeyD fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combineC.induct_unfolding : ∀ (c : ℕ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k₁ k₂ : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂)
        (Lean.Grind.CommRing.Poly.num ((k₁ + k₂) % ↑c))) →
    (∀ (k₁ k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
        motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
          ((Lean.Grind.CommRing.Poly.add k₂ m₂ p₂).addConstC k₁ c)) →
      (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ),
          motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂)
            ((Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).addConstC k₂ c)) →
        (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
            (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
            m₁.grevlex m₂ = Ordering.eq →
              have k := (k₁ + k₂) % ↑c;
              (k == 0) = true →
                motive p₁ p₂ (p₁.combineC p₂ c) →
                  motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
                    (p₁.combineC p₂ c)) →
          (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
              (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
              m₁.grevlex m₂ = Ordering.eq →
                have k := (k₁ + k₂) % ↑c;
                (k == 0) = false →
                  motive p₁ p₂ (p₁.combineC p₂ c) →
                    motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
                      (Lean.Grind.CommRing.Poly.add k m₁ (p₁.combineC p₂ c))) →
            (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
                (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
                m₁.grevlex m₂ = Ordering.gt →
                  motive p₁ (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
                      (p₁.combineC (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂) c) →
                    motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
                      (Lean.Grind.CommRing.Poly.add k₁ m₁ (p₁.combineC (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂) c))) →
              (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
                  (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
                  m₁.grevlex m₂ = Ordering.lt →
                    motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) p₂
                        ((Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).combineC p₂ c) →
                      motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)
                        (Lean.Grind.CommRing.Poly.add k₂ m₂ ((Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).combineC p₂ c))) →
                ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly), motive p₁ p₂ (p₁.combineC p₂ c)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.range : Lean.Lsp.LeanFileProgressProcessingInfo → Lean.Lsp.Range
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csInf_union : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] (s t : Set α), min (sInf s) (sInf t) ≤ sInf (s ∪ t)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, (Asymptotics.IsBigOWith c l f fun x => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f g'
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall_top`. -/
EMetric.closedBall_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α), Metric.closedEBall x ⊤ = Set.univ
-- Mathlib.Topology.Order.IntermediateValue
/-- If a closed interval is contained in its own image under a continuous map `f : α → α`,
then this map has a fixed point on this interval.  -/
exists_mem_Icc_isFixedPt_of_surjOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.Icc a b) →
    a ≤ b → Set.SurjOn f (Set.Icc a b) (Set.Icc a b) → ∃ c ∈ Set.Icc a b, Function.IsFixedPt f c
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return : Std.Sat.AIG Std.Tactic.BVDecide.BVBit → ℕ → Type
-- Mathlib.Algebra.DirectSum.Module
DFinsupp.mapRange.linearEquiv.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i),
  DFinsupp.mapRange.linearEquiv e =
    { toFun := DFinsupp.mapRange (fun i x => (e i) x) ⋯, map_add' := ⋯, map_smul' := ⋯,
      invFun := DFinsupp.mapRange (fun i x => (e i).symm x) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- Auxiliary lemma for `Lp.induction_stronglyMeasurable`.  -/
MeasureTheory.Lp.induction_stronglyMeasurable_aux : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F] (hm : m ≤ m0),
  p ≠ ⊤ →
    ∀ (P : ↥(MeasureTheory.Lp F p μ) → Prop),
      (∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
          P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)) →
        (∀ ⦃f g : α → F⦄ (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
            MeasureTheory.AEStronglyMeasurable f μ →
              MeasureTheory.AEStronglyMeasurable g μ →
                Disjoint (Function.support f) (Function.support g) →
                  P (MeasureTheory.MemLp.toLp f hf) →
                    P (MeasureTheory.MemLp.toLp g hg) →
                      P (MeasureTheory.MemLp.toLp f hf + MeasureTheory.MemLp.toLp g hg)) →
          IsClosed {f | P ↑f} → ∀ (f : ↥(MeasureTheory.Lp F p μ)), MeasureTheory.AEStronglyMeasurable (↑↑f) μ → P f
-- Mathlib.Data.List.Destutter
List.destutter.eq_2 : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R], List.destutter R [] = []
-- Mathlib.Tactic.Simps.Basic
Simps.ParsedProjectionData.mk : Lean.Name →
  Lean.Syntax → Lean.Name → Lean.Syntax → Bool → Bool → Option Lean.Expr → Array ℕ → Bool → Simps.ParsedProjectionData
-- Lean.Setup
Lean.ModuleArtifacts.mk.inj : ∀
  {lean? olean? oleanServer? oleanPrivate? ilean? irSig? ir? c? bc? lean?_1 olean?_1 oleanServer?_1 oleanPrivate?_1
    ilean?_1 irSig?_1 ir?_1 c?_1 bc?_1 : Option System.FilePath},
  { lean? := lean?, olean? := olean?, oleanServer? := oleanServer?, oleanPrivate? := oleanPrivate?, ilean? := ilean?,
        irSig? := irSig?, ir? := ir?, c? := c?, bc? := bc? } =
      { lean? := lean?_1, olean? := olean?_1, oleanServer? := oleanServer?_1, oleanPrivate? := oleanPrivate?_1,
        ilean? := ilean?_1, irSig? := irSig?_1, ir? := ir?_1, c? := c?_1, bc? := bc?_1 } →
    lean? = lean?_1 ∧
      olean? = olean?_1 ∧
        oleanServer? = oleanServer?_1 ∧
          oleanPrivate? = oleanPrivate?_1 ∧
            ilean? = ilean?_1 ∧ irSig? = irSig?_1 ∧ ir? = ir?_1 ∧ c? = c?_1 ∧ bc? = bc?_1
-- Mathlib.Geometry.Manifold.Algebra.Structures
ContMDiffRing.toContMDiffAdd : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {R : Type u_4} {inst_4 : Semiring R} {inst_5 : TopologicalSpace R} {inst_6 : ChartedSpace H R}
  [self : ContMDiffRing I n R], ContMDiffAdd I n R
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_3 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (hp : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.done, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_3 hp
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_insert : ∀ {α : Type u_2} [inst : AddCommMonoid α] [IsCancelAdd α] {s : Set α} {a : α},
  ThreeAPFree (insert a s) ↔
    ThreeAPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b + c = a + a → b = a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.lift_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.fun_sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableSub₂ G],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i - g i) μ
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedAddMonoid.toAddLeftMono : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α], AddLeftMono α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_iff_one_lt_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosStrictMono α]
  [MulPosReflectLT α], 0 < a → (a < b * a ↔ 1 < b)
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaCongrRight_refl : ∀ {α : Type u_2} {β : α → Type u_1}, (Equiv.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
-- Mathlib.RingTheory.Ideal.Operations
instNonUnitalSubringClassIdeal : ∀ {R : Type u_1} [inst : Ring R], NonUnitalSubringClass (Ideal R) R
-- Mathlib.Tactic.Use
/-- `use e₁, e₂, ⋯` instantiates all existential quantifiers in the main goal by using `e₁`, `e₂`, ...
as witnesses, creates goals for all the remaining witnesses, and tries to discharge these goals
automatically.

`use` is similar to `exists` or `existsi`, but unlike `exists` it is equivalent to applying the
tactic `refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩` with any number of placeholders (rather than just one) and
then trying to close goals associated to the placeholders with a configurable discharger (rather
than just `try trivial`).

* `use! e₁, e₂, ⋯` applies constructors everywhere rather than just for goals that correspond to the
  last argument of a constructor. This gives the effect that nested constructors are being flattened
  out, with the supplied values being used along the leaves and nodes of the tree of constructors.
* `use (discharger := tac) e₁, e₂, ...` calls `tac` as a discharger, on all remaining `Prop`-valued
  goals. If this option is omitted, `use` calls `try with_reducible use_discharger` as default
  discharger.
  To turn off the discharger and keep all goals, use `(discharger := skip)`.
  To allow "heavy refls", use `(discharger := try use_discharger)`.
  If `tac` fails on the new goal, `use (discharger := tac)` fails (hint: you might want to use
  `(discharger := try tac)` instead).

Examples:

```lean
example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

-- With `use!` one can feed in each `42` one at a time:
example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
/-
The second line makes use of the fact that `use!` tries refining with the argument before
applying a constructor. Also note that `use`/`use!` by default uses a tactic
called `use_discharger` to discharge goals, so `use! 42` will close the goal in this example since
`use_discharger` applies `rfl`, which as a consequence solves for the other `Nat` metavariable.
-/
```
 -/
Mathlib.Tactic.useSyntax : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.descH.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k k_1 : h.K ⟶ A) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp h.f' k = 0), h.descH k hk = h.descH k_1 ⋯
-- Init.Meta.Defs
/-- Creates an identifier with its position copied from the syntax returned by `getRef`.

To refer to a specific constant without a risk of variable capture, use `mkCIdentFromRef` instead.
 -/
Lean.mkIdentFromRef : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → Lean.Name → optParam Bool false → m Lean.Ident
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.equal.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {t₁ t₂ t₁_1 t₂_1 : L.Term (α ⊕ Fin n)},
  FirstOrder.Language.BoundedFormula.equal t₁ t₂ = FirstOrder.Language.BoundedFormula.equal t₁_1 t₂_1 →
    t₁ = t₁_1 ∧ t₂ = t₂_1
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The category of finitely generated `R`-algebras is equivalent to the category of
finite type ring homomorphisms from `R`.  -/
FGAlgCat.equivUnder : (R : CommRingCat) →
  FGAlgCat ↑R ≌ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.FiniteType).Under ⊤ R
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp.inj : ∀ {e : Lean.Expr} {f g h : Mathlib.Tactic.BicategoryLike.Mor₁} {η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e_1 f_1 g_1 h_1 η_1 θ_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1 ∧ θ = θ_1
-- Mathlib.RingTheory.Noetherian.Defs
/-- `IsNoetherian R M` is the proposition that `M` is a Noetherian `R`-module,
implemented as the predicate that all `R`-submodules of `M` are finitely generated.
 -/
IsNoetherian : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.BisimO.match_1.splitter : {α : Type u_1} →
  (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) →
    (x x_1 : α ⊕ Computation α) →
      ((a a' : α) → motive (Sum.inl a) (Sum.inl a')) →
        ((s s' : Computation α) → motive (Sum.inr s) (Sum.inr s')) →
          ((x x_2 : α ⊕ Computation α) →
              (∀ (a a' : α), x = Sum.inl a → x_2 = Sum.inl a' → False) →
                (∀ (s s' : Computation α), x = Sum.inr s → x_2 = Sum.inr s' → False) → motive x x_2) →
            motive x x_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.empty_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β}, ∅ = m ↔ m = ∅
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.exists_mul_mem_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {I p : Ideal R}, p ∈ I.minimalPrimes → ∀ {x : R}, x ∈ p → ∃ y ∉ I, x * y ∈ I
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `sum f g` is the sum of `g a (f.coeff a)` over the support of `f`.  -/
SkewMonoidAlgebra.sum : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid k] → {N : Type u_3} → [AddCommMonoid N] → SkewMonoidAlgebra k G → (G → k → N) → N
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The `BoxIntegral.IntegrationParams` corresponding to the generalized Perron integral. In the
corresponding filter, we require that the tagged partition is subordinate to a (possibly,
discontinuous) positive function `r` and each tag belongs to the corresponding closed box. We also
require an upper estimate on the distortion of all boxes of the partition.  -/
BoxIntegral.IntegrationParams.GP : BoxIntegral.IntegrationParams
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_eq_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {β : ι → Type u_4}
  {f f' : (i : ι) → α i → β i},
  (∀ (i : ι), f i =ᵐ[μ i] f' i) → (fun x i => f i (x i)) =ᵐ[MeasureTheory.Measure.pi μ] fun x i => f' i (x i)
-- Mathlib.Order.RelSeries
RelSeries.last_cons : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r),
  (p.cons newHead rel).last = p.last
-- Lean.Compiler.IR.Basic
Lean.IR.reshapeAux : Array Lean.IR.FnBody → ℕ → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCocones_pt_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) (k : K),
  (CategoryTheory.Limits.combineCocones F c).pt.obj k = (c k).cocone.pt
-- Lean.Elab.DeclNameGen
/-- Keeps track of constants that appear in the generated name.  -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.consts : Lean.Elab.Command.NameGen.MkNameState✝ → Lean.NameSet