mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : NonAssocSemiring α] [inst_1 : Preorder α]
  [inst_2 : NonAssocSemiring β] [inst_3 : Preorder β] [inst_4 : NonAssocSemiring γ] [inst_5 : Preorder γ]
  [inst_6 : NonAssocSemiring δ] [inst_7 : Preorder δ] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.MetricSpace.Cauchy
/-- If the distance between `s n` and `s m`, `n, m ≥ N` is bounded above by `b N`
and `b` converges to zero, then `s` is a Cauchy sequence.  -/
cauchySeq_of_le_tendsto_0 : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {s : β → α}
  (b : β → ℝ),
  (∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) → Filter.Tendsto b Filter.atTop (nhds 0) → CauchySeq s
-- Init.Data.List.ControlImpl
List.flatMapMTR.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α),
  List.flatMapMTR f as = List.flatMapMTR.loop f as []
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- For any nonzero `x : R`, `ordFrac R (algebraMap R K x) ≥ 1`. Note here that this last
expression is in `ℤᵐ⁰`, so the syntax may be slightly different than expected. Namely,
the `1` here is `WithZero.exp 0`, and so would usually be written as `0` in the additive
context. Further, the order here is different to similar lemmas involving `Ring.ord`, since
here the order is on `ℤᵐ⁰` has the `∞` element less than everything else, whereas in `Ring.ord`
we work with the order on `ℕ∞` where the `∞` element is interpreted as a `⊤` element.
 -/
Ring.ordFrac_ge_one_of_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsNoetherianRing R] [inst_3 : Ring.KrullDimLE 1 R]
  {K : Type u_2} [inst_4 : Field K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K] {x : R},
  x ≠ 0 → 1 ≤ (Ring.ordFrac R) ((algebraMap R K) x)
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  {x y : CategoryTheory.SimplicialObject.Homotopy f g},
  x = y ↔
    @CategoryTheory.SimplicialObject.Homotopy.h C inst X Y f g x =
      @CategoryTheory.SimplicialObject.Homotopy.h C inst X Y f g y
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.comp_coe : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (f : M₁ ≃SL[σ₁₂] M₂) (f' : M₂ ≃SL[σ₂₃] M₃),
  ↑f' ∘SL ↑f = ↑(f.trans f')
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a ring homomorphism `f : α →+* β` as a monoid homomorphism `α →* β`.
The `simp`-normal form is `(f : α →* β)`.  -/
RingHom.toMonoidHom : {α : Type u_5} → {β : Type u_6} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* β
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Neg β] (f : α → β) (c : α),
  Function.Antiperiodic f c = ∀ (x : α), f (x + c) = -f x
-- Init.Prelude
/-- The predecessor of a natural number is one less than it. The predecessor of `0` is defined to be
`0`.

This definition is overridden in the compiler with an efficient implementation. This definition is
the logical model.
 -/
Nat.pred : ℕ → ℕ
-- Lean.Data.Lsp.Internal
/-- Whether the module is being imported via `private import`.  -/
Lean.Lsp.ImportInfo.isPrivate : Lean.Lsp.ImportInfo → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When `S₁.f`, `S₁.g`, `S₂.f` and `S₂.g` are all zero, the action on homology of a
morphism `φ : S₁ ⟶ S₂` is given by the action `φ.τ₂` on the middle objects.  -/
CategoryTheory.ShortComplex.HomologyMapData.ofZeros : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (hg₁ : S₁.g = 0) →
              (hf₂ : S₂.f = 0) →
                (hg₂ : S₂.g = 0) →
                  CategoryTheory.ShortComplex.HomologyMapData φ
                    (CategoryTheory.ShortComplex.HomologyData.ofZeros S₁ hf₁ hg₁)
                    (CategoryTheory.ShortComplex.HomologyData.ofZeros S₂ hf₂ hg₂)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.assoc_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Order.Filter.Cofinite
/-- A function tendsto 0 along the cofinite filter iff it has finite support.  -/
tendsto_cofinite_pure_iff : ∀ {α : Type u_2} {β : Type u_3} {f : α → β} [inst : Zero β],
  Filter.Tendsto f Filter.cofinite (pure 0) ↔ Function.HasFiniteSupport f
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_eq_blsub' : ∀ {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o)
  (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u u_3}), Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = o.blsub f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rcc_eq_none : ∀ {m n i : ℕ}, n + 1 ≤ i + m → (m...=n).toArray[i]? = none
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_and_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α},
  b ≤ Order.succ a ∧ a ≤ b ↔ b = a ∨ b = Order.succ a
-- Mathlib.CategoryTheory.Presentable.Finite
/-- An object `X` is finitely presentable if `Hom(X, -)` preserves all filtered colimits.  -/
CategoryTheory.IsFinitelyPresentable : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Prop
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_toGeneralLinearGroup_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (u : SpecialLinearGroup R V), ↑(SpecialLinearGroup.toGeneralLinearGroup u) = ↑(SpecialLinearGroup.toLinearEquiv u)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
basisOfLinearIndependentOfCardEqFinrank'_repr_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [inst_4 : FiniteDimensional K V] (b : ι → V) (hb : LinearIndependent K b)
  (hι : Fintype.card ι = Module.finrank K V) (x : V),
  (basisOfLinearIndependentOfCardEqFinrank' b hb hι).repr x =
    hb.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) x)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- In the space `ℝ × ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure.  -/
MeasureTheory.hausdorffMeasure_prod_real : MeasureTheory.Measure.hausdorffMeasure 2 = MeasureTheory.volume
-- Init.Data.BitVec.Bitblast
BitVec.extractLsb'_cpopLayer : ∀ {w iterNum i oldLen : ℕ} {oldLayer : BitVec (oldLen * w)} {newLayer : BitVec (iterNum * w)}
  (hold : 2 * (iterNum - 1) < oldLen),
  (∀ i < iterNum,
      BitVec.extractLsb' (i * w) w newLayer =
        BitVec.extractLsb' (2 * i * w) w oldLayer + BitVec.extractLsb' ((2 * i + 1) * w) w oldLayer) →
    BitVec.extractLsb' (i * w) w (oldLayer.cpopLayer newLayer hold) =
      BitVec.extractLsb' (2 * i * w) w oldLayer + BitVec.extractLsb' ((2 * i + 1) * w) w oldLayer
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (X : CategoryTheory.Subobject B) (f : A₁ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g]
  (h₁ : X ≤ CategoryTheory.Subobject.mk f) (h₂ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLEMk f g h₂) = X.ofLEMk g ⋯
-- Std.Time.Format.Modifier
/-- Exactly 00:00:00
 -/
Std.Time.ExtendedDayPeriod.midnight : Std.Time.ExtendedDayPeriod
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_mul_apply_of_not_exists_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (r : R) {g g' : M} (x : MonoidAlgebra R M),
  (¬∃ d, g' = g * d) → (MonoidAlgebra.single g r * x).coeff g' = 0
-- Lean.Parser.Command
Lean.Parser.Command.in.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Lemmas
Array.extract_zero : ∀ {α : Type u_1} {start : ℕ} {xs : Array α}, xs.extract start 0 = #[]
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The Hadamard determinant identity: `star (det A) * det A = (card n)^(card n)`.  -/
Matrix.IsHadamard.star_det_mul_det : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → star A.det * A.det = ↑(Fintype.card n) ^ Fintype.card n
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_snd : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitInTwo l).2 = ⟨List.drop ((n + 1) / 2) ↑l, ⋯⟩
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The shadow of a set family `𝒜` is all sets we can get by removing one element from any set in
`𝒜`, and the (`k` times) iterated shadow (`shadow^[k]`) is all sets we can get by removing `k`
elements from any set in `𝒜`.  -/
Finset.shadow : {α : Type u_1} → [DecidableEq α] → Finset (Finset α) → Finset (Finset α)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h
-- Mathlib.Order.Category.BddDistLat
/-- Typecheck a `BoundedLatticeHom` as a morphism in `BddDistLat`.  -/
BddDistLat.ofHom : {X Y : Type u} →
  [inst : DistribLattice X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : DistribLattice Y] →
        [inst_3 : BoundedOrder Y] → BoundedLatticeHom X Y → (BddDistLat.of X ⟶ BddDistLat.of Y)
-- Init.Data.Int.LemmasAux
Int.zero_le_ofNat : ∀ (n : ℕ), 0 ≤ OfNat.ofNat n
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.rpcWireFormat : Lean.Lsp.ClientCapabilities → Lean.Lsp.RpcWireFormat
-- Lean.Declaration
Lean.ConstantInfo.quotInfo : Lean.QuotVal → Lean.ConstantInfo
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- Singletons are bounded.  -/
Bornology.isVonNBounded_singleton : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E), Bornology.IsVonNBounded 𝕜 {x}
-- Mathlib.RingTheory.Polynomial.Basic
/-- Given an ideal `I` in `R[X]`, make the ideal in `R` of the
leading coefficients in `I`.  -/
Ideal.leadingCoeff : {R : Type u} → [inst : Semiring R] → Ideal (Polynomial R) → Ideal R
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.toArrow_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).right =
    CategoryTheory.SimplicialObject.Augmented.point.obj X
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.below.iUnion : ∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop}
  (f : ℕ → Set α) (a : ∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n)),
  (∀ (n : ℕ), MeasurableSpace.GenerateMeasurable.below ⋯) →
    (∀ (n : ℕ), motive (f n) ⋯) → MeasurableSpace.GenerateMeasurable.below ⋯
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set is continuous in point  -/
Metric.continuous_infDist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Continuous fun x => Metric.infDist x s
-- Mathlib.Control.Monad.Cont
MonadCont.mk : {m : Type u → Type v} → ({α β : Type u} → (MonadCont.Label α m β → m α) → m α) → MonadCont m
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- `(G × H) / (A × B)` is isomorphic to `G / A × H / B`.  -/
QuotientAddGroup.prodAddEquiv : {G : Type u} →
  [inst : AddGroup G] →
    {H : Type v} →
      [inst_1 : AddGroup H] →
        (A : AddSubgroup G) →
          (B : AddSubgroup H) → [inst_2 : A.Normal] → [inst_3 : B.Normal] → (G × H) ⧸ A.prod B ≃+ (G ⧸ A) × H ⧸ B
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.sum_monomial_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : AddCommMonoid A] {u : σ →₀ ℕ} {r : R}
  {b : (σ →₀ ℕ) → R → A}, b u 0 = 0 → ((MvPolynomial.monomial u) r).coeff.sum b = b u r
-- Mathlib.Data.Finsupp.BigOperators
List.support_sum_eq : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] (l : List (ι →₀ M)),
  List.Pairwise (Function.onFun Disjoint Finsupp.support) l →
    l.sum.support = List.foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l
-- Mathlib.Data.Rat.Defs
Rat.addGroup : AddGroup ℚ
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_symm_apply : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (a : Polynomial (MvPolynomial S₁ R)),
  (MvPolynomial.optionEquivLeft R S₁).symm a =
    (Polynomial.aevalTower (MvPolynomial.rename some) (MvPolynomial.X none)) a
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on an additive quantale are similar
to the Heyting operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ᵣ z ↔ y + x ≤ z` or alternatively `x ⇨ₗ y = sSup { z | x + z ≤ y }`."  -/
AddQuantale.rightAddResiduation : {α : Type u_1} → [AddSemigroup α] → [CompleteLattice α] → α → α → α
-- Mathlib.Analysis.Real.Cardinality
Cardinal.Real.Icc_countable_iff : ∀ {x y : ℝ}, (Set.Icc x y).Countable ↔ y ≤ x
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.graph.card : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α), (Tuple.graph f).card = n
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_sInf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (S : Set (BooleanSubalgebra α)), ↑(sInf S) = ⋂ L ∈ S, ↑L
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.bot_imp : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Imp ⊥ φ
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instRing : {R : Type u_1} → [Ring R] → Ring Rᵒᵈ
-- Mathlib.Algebra.Opposites
/-- The element of `αᵃᵒᵖ` that represents `x : α`.  -/
AddOpposite.op : {α : Type u_1} → α → αᵃᵒᵖ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_nil : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α], m.WF → m.insertMany [] = m
-- Mathlib.Analysis.Complex.Norm
Complex.abs_re_lt_norm : ∀ {z : ℂ}, |z.re| < ‖z‖ ↔ z.im ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.minKey? = none ↔ t.isEmpty = true)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).get! k' =
        if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
-- Qq.Commands
/-- `by_elabq` is the Qq analogue to `by_elab` which allows executing arbitrary `TermElabM` code in
place of a term. In contrast to `by_elab`, the local context can be directly accessed as quoted
expressions and the return type is Q-annotated.
Example:
```
def f (x : Prop) [Decidable x] : Int :=
  by_elabq
    Lean.logInfo x
    Lean.logInfo x.ty
    return q(if $x then 2 else 3)
```
See also: `run_tacq`.
 -/
Qq.termBy_elabq_ : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.LogDeriv
/-- At a simple zero of an analytic function, the logarithmic residue
`(w - x) * logDeriv f w` tends to 1.  -/
AnalyticAt.tendsto_mul_logDeriv_simple_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜},
  AnalyticAt 𝕜 f x →
    f x = 0 → deriv f x ≠ 0 → Filter.Tendsto (fun w => (w - x) * logDeriv f w) (nhdsWithin x {x}ᶜ) (nhds 1)
-- Mathlib.Topology.Order.OrderClosed
Ioi_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ioi a ∈ nhds b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.NNReal.upper_bound : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α NNReal) (x : α), f x ≤ nndist f 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.map_bot : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : IsScalarTower R B B] [inst_8 : SMulCommClass R B B] (f : A →ₙₐ[R] B),
  NonUnitalSubalgebra.map f ⊥ = ⊥
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ),
  ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.ext.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)),
  CategoryTheory.Limits.Cone.ext φ w =
    { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty P.FullSubcategory)),
  (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.lift s).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.toUnit s.pt.obj
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.LimitPresentation J X) {i j : J} (f : i ⟶ j) {Z : C} (h : pres.diag.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (pres.π.app i) (CategoryTheory.CategoryStruct.comp (pres.diag.map f) h) =
    CategoryTheory.CategoryStruct.comp (pres.π.app j) h
-- Init.Data.Rat.Lemmas
_private.Init.Data.Rat.Lemmas.0.Rat.divInt.match_3.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (n : ℤ) (d : ℕ) (h_1 : (n : ℤ) → (d : ℕ) → motive n (Int.ofNat d))
  (h_2 : (n : ℤ) → (d : ℕ) → motive n (Int.negSucc d)),
  (match n, Int.negSucc d with
    | n, Int.ofNat d => h_1 n d
    | n, Int.negSucc d => h_2 n d) =
    h_2 n d
-- Std.Data.DHashMap.Raw
/-- Well-formedness predicate for hash maps. Users of `DHashMap` will not need to interact with
this. Users of `DHashMap.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas
like `WF.empty` and `WF.insert` (which are always named exactly like the operations they are about)
to show that map operations preserve well-formedness. The constructors of this type are internal
implementation details and should not be accessed by users.
 -/
Std.DHashMap.Raw.WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → Prop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [SecondCountableTopology α] {f g : β → α},
  Measurable f → Measurable g → Measurable fun b => edist (f b) (g b)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
/-- If `C` is monoidal closed and has suitable limits, the functor
category `J ⥤ C` is monoidal closed.  -/
CategoryTheory.MonoidalClosed.FunctorCategory.monoidalClosed : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        {J : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
            [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                  CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] →
              [∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] →
                CategoryTheory.MonoidalClosed (CategoryTheory.Functor J C)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.size ≤ t.size + 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.eq_2 : ∀ (x : ℕ), Nat.nthRoot 1 x = x
-- Mathlib.Data.List.Permutation
List.length_foldr_permutationsAux2 : ∀ {α : Type u_1} (t : α) (ts : List α) (r L : List (List α)),
  (List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L).length = (List.map List.length L).sum + r.length
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.AdjoinSimple.coe_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  ↑(IntermediateField.AdjoinSimple.gen F α) = α
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_neg : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a : AsBoolRing α), ofBoolRing (-a) = ofBoolRing a
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonAssocCommSemiring` instance along an injective function.  -/
Function.Injective.nonAssocCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : One S] →
            [inst_4 : SMul ℕ S] →
              [inst_5 : NatCast S] →
                [inst_6 : NonAssocCommSemiring R] →
                  (f : S → R) →
                    Function.Injective f →
                      f 0 = 0 →
                        f 1 = 1 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → NonAssocCommSemiring S