mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.mk.inj : ∀ {message? since? message?_1 since?_1 : Option String},
  { message? := message?, since? := since? } = { message? := message?_1, since? := since?_1 } →
    message? = message?_1 ∧ since? = since?_1
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousWithinAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {x : α} {s : Set α}
  {z : Set β}, UpperHemicontinuousWithinAt (fun _x => z) s x
-- Init.Data.List.Lemmas
List.set_replicate_self : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ}, (List.replicate n a).set i a = List.replicate n a
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMaxOrderElemIci : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMaxOrder α], NoMaxOrder ↑(Set.Ici a)
-- Init.Tactics
/-- `assumption` tries to solve the main goal using a hypothesis of compatible type, or else fails.
Note also the `‹t›` term notation, which is a shorthand for `show t by assumption`.
 -/
Lean.Parser.Tactic.assumption : Lean.ParserDescr
-- Lean.Server.FileWorker.Utils
/-- Tracks diagnostics and incremental diagnostic reporting state for a single document version.

The sticky diagnostics are shared across all document versions via an `IO.Ref`, while per-version
diagnostics are stored directly. The whole state is wrapped in a `Std.Mutex` on
`EditableDocumentCore` to ensure atomic updates.
 -/
Lean.Server.FileWorker.DiagnosticsState : Type
-- Mathlib.Order.Filter.Defs
Filter.mk : {α : Type u_1} →
  (sets : Set (Set α)) →
    Set.univ ∈ sets →
      (∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets) → (∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets) → Filter α
-- Init.Data.Vector.Lemmas
Vector.getElem_replicate : ∀ {α : Type u_1} {i n : ℕ} {a : α} (h : i < n), (Vector.replicate n a)[i] = a
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.fourierSMulRight.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V),
  VectorFourier.fourierSMulRight L f v = -(2 * ↑Real.pi * Complex.I) • (L v).smulRight (f v)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an additive semigroup homomorphism
`Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ`. Inverse to `AddHom.op`.  -/
AddHom.unop : {M : Type u_3} → {N : Type u_4} → [inst : Add M] → [inst_1 : Add N] → (Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ) ≃ (M →ₙ+ N)
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.aeval_apply_of_hasEigenvector : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M} {p : Polynomial R}, f.HasEigenvector μ x → ((Polynomial.aeval f) p) x = Polynomial.eval μ p • x
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_mul_iff : ∀ {p x : ℝ} {m : ℤ}, m ≠ 0 → (LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x)
-- Mathlib.Algebra.Category.CommBialgCat
/-- Build a `BialgEquiv` from an isomorphism in the category `CommBialgCat R`.  -/
CommBialgCat.bialgEquivOfIso : {R : Type u} → [inst : CommRing R] → {A B : CommBialgCat R} → (A ≅ B) → ↑A ≃ₐc[R] ↑B
-- Init.Data.Option.Lemmas
Option.none_le : ∀ {α : Type u_1} [inst : LE α] {a : Option α}, none ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- Suppose `f` and `g` are two morphisms with a common codomain and `s` is a limit cone over the
diagram formed by `f` and `g`. Suppose `f` and `g` both factor through a monomorphism `h` via
`x` and `y`, respectively.  Then `s` is also a limit cone over the diagram formed by `x` and `y`.  -/
CategoryTheory.Limits.PullbackCone.isLimitOfFactors : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ Z) →
            [inst_1 : CategoryTheory.Mono h] →
              (x : X ⟶ W) →
                (y : Y ⟶ W) →
                  (hxh : CategoryTheory.CategoryStruct.comp x h = f) →
                    (hyh : CategoryTheory.CategoryStruct.comp y h = g) →
                      (s : CategoryTheory.Limits.PullbackCone f g) →
                        CategoryTheory.Limits.IsLimit s →
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk s.fst s.snd ⋯)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f)[k]? = f m[k]?
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.NatTrans.CommShift₂.commShift_flipApp : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} {G₁ G₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} {τ : G₁ ⟶ G₂}
  {h : CategoryTheory.CommShift₂Setup D M} {inst_7 : G₁.CommShift₂ h} {inst_8 : G₂.CommShift₂ h}
  [self : CategoryTheory.NatTrans.CommShift₂ τ h] (X₂ : C₂),
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.flipApp τ X₂) M
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_mono_real : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} {g : α → ℝ},
  MeasureTheory.MemLp g p μ → (∀ (x : α), ‖f x‖ ≤ g x) → MeasureTheory.lpNorm f p μ ≤ MeasureTheory.lpNorm g p μ
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Icc_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioc a b ⊆ Finset.Icc a b
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaType_obj_obj_coe : ∀ (X : Type uᵒᵖ) (G : AddCommGrpCat), ↑((AddCommGrpCat.coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
-- Mathlib.Topology.Sheaves.Functors
/-- The adjunction between pullback and pushforward for sheaves on topological spaces.  -/
TopCat.Sheaf.pullbackPushforwardAdjunction : {X Y : TopCat} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{w, u_1} A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type w} →
          [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory A FA] →
              [inst_3 : CategoryTheory.Limits.HasColimits A] →
                [inst_4 : CategoryTheory.Limits.HasLimits A] →
                  [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                    [inst_6 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] →
                      [inst_7 : (CategoryTheory.forget A).ReflectsIsomorphisms] →
                        (f : X ⟶ Y) → TopCat.Sheaf.pullback A f ⊣ TopCat.Sheaf.pushforward A f
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.bot : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M], IsHausdorff ⊥ M
-- Mathlib.Analysis.Calculus.Implicit
/-- The implicit function is strictly differentiable.  -/
ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt))
    (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) (φ.rightFun φ.pt)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R), W'.addXYZ P Q 0 = W'.addX P Q
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.equivalence_counitIso : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.equivalence.counitIso = ContinuousGeneratedByCat.equivalenceCounitIso
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup (AddUnits G)) (x : G), x ∈ H.ofAddUnits ↔ toAddUnits x ∈ H
-- Init.Data.List.Lex
List.le_iff_exists : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {l₁ l₂ : List α},
  l₁ ≤ l₂ ↔
    l₁ = List.take l₁.length l₂ ∨
      ∃ i, ∃ (h₁ : i < l₁.length) (h₂ : i < l₂.length), (∀ (j : ℕ) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {V W : CoalgCat R}
  {toCoalgHom' toCoalgHom'_1 : ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat},
  { toCoalgHom' := toCoalgHom' } = { toCoalgHom' := toCoalgHom'_1 } → toCoalgHom' = toCoalgHom'_1
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing a multilinear map twice with a linear map in each argument is
the same as composing with their composition.  -/
MultilinearMap.compLinearMap_assoc : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₁'' : ι → Type v₁''} {M₂ : Type v₂}
  [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : ι) → Module R (M₁ i)] [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)]
  [inst_6 : (i : ι) → Module R (M₁' i)] [inst_7 : (i : ι) → AddCommMonoid (M₁'' i)]
  [inst_8 : (i : ι) → Module R (M₁'' i)] (g : MultilinearMap R M₁'' M₂) (f₁ : (i : ι) → M₁' i →ₗ[R] M₁'' i)
  (f₂ : (i : ι) → M₁ i →ₗ[R] M₁' i), (g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun i => f₁ i ∘ₗ f₂ i
-- Mathlib.Data.Sum.Order
Equiv.optionEquivSumPUnit.eq_1 : ∀ (α : Type w),
  Equiv.optionEquivSumPUnit α =
    { toFun := fun o => o.elim (Sum.inr PUnit.unit) Sum.inl, invFun := fun s => Sum.elim some (fun x => none) s,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_right : ∀ {α : Type u_1} (s t : Set α), s.ite t s = t ∩ s
-- Mathlib.Algebra.Group.Subgroup.Finsupp
Subgroup.mem_closure_range_iff_of_fintype : ∀ {M : Type u_1} [inst : CommGroup M] {ι : Type u_2} {f : ι → M} {x : M} [inst_1 : Fintype ι],
  x ∈ Subgroup.closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i
-- Mathlib.Topology.Compactness.Compact
isCompact_iff_ultrafilter_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
        Std.Internal.List.getKeyD k l₁ fallback
-- Mathlib.Order.Antichain
IsAntichain.insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsAntichain r s →
    (∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r b a) → (∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b) → IsAntichain r (insert a s)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_map_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₃ = f.f k
-- Mathlib.Data.Multiset.DershowitzManna
/-- Over a well-founded order, `OneStep` is well-founded.  -/
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.isDershowitzMannaLT_singleton_wf : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedLT α], WellFounded Multiset.OneStep✝
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux : ∀ (X : AlgebraicGeometry.Scheme) (S : ↑X.affineOpens) (U₁ U₂ : X.Opens) {n₁ n₂ : ℕ}
  {y₁ : ↑(X.presheaf.obj (Opposite.op U₁))} {y₂ : ↑(X.presheaf.obj (Opposite.op U₂))}
  {f : ↑(X.presheaf.obj (Opposite.op (U₁ ⊔ U₂)))} {x : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))} (h₁ : ↑S ≤ U₁)
  (h₂ : ↑S ≤ U₂),
  TopCat.Presheaf.restrictOpen y₁ (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ =
      TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)
            (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ ^
          n₁ *
        TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ →
    TopCat.Presheaf.restrictOpen y₂ (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ =
        TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)
              (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ ^
            n₂ *
          TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ →
      ∃ n,
        ∀ (m : ℕ),
          n ≤ m →
            TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ (m + n₂) * y₁) (↑S) h₁ =
              TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ (m + n₁) * y₂) (↑S) h₂
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_self_apply_zpow : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (n : ℤ) (x : α),
  f.cycleOf ((f ^ n) x) = f.cycleOf x
-- Init.Data.Rat.Lemmas
Rat.floor_add_intCast : ∀ {x : ℚ} {y : ℤ}, (x + ↑y).floor = x.floor + y
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_inv_nat : ∀ (x : ℂ) (n : ℕ), ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasFDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {t : Set 𝕜'} (x : E),
  HasDerivWithinAt h₂ h₂' t y →
    HasFDerivAt f f' x → (∀ᶠ (x' : E) in nhds x, f x' ∈ t) → y = f x → HasFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).mor₃ = DerivedCategory.triangleOfSESδ hS
-- Mathlib.Order.Cover
WCovBy.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β}, x ⩿ y → x.1 ⩿ y.1
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- Counts entries remaining in a subarray, including nested children.  -/
Lean.PersistentHashMap.subarrayMeasure : {α : Type u_1} → {β : Type u_2} → Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → ℕ
-- Lean.Elab.Tactic.Omega.Frontend
/-- An integer linear arithmetic problem.  -/
Lean.Elab.Tactic.Omega.MetaProblem.problem : Lean.Elab.Tactic.Omega.MetaProblem → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Algebra.Category.Ring.FilteredColimits
RingCat.FilteredColimits.colimitRing : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J RingCat) → Ring ↑(RingCat.FilteredColimits.R F)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory CommGrpCat fun x1 x2 => ↑x1 →* ↑x2
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfUnion_subset : ∀ {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  j ∈ J → ↑(hC.disjointOfUnion hJ j) ⊆ C
-- Mathlib.Order.Interval.Finset.Basic
Finset.inf_Ici : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : OrderTop α] (a : α),
  (Finset.Ici a).inf id = a
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.evalFinsetIccNat.eq_def : ∀ (m n : ℕ) (em en : Q(ℕ)),
  Mathlib.Tactic.Simp.evalFinsetIccNat m n em en =
    if m = n then
      have this := ⋯;
      pure ⟨q({«$em»}), q(⋯)⟩
    else
      if m < n then
        have hmn := q(⋯);
        have em' := Qq.mkNatLitQ (m + 1);
        have this := ⋯;
        do
        let __x ← Mathlib.Tactic.Simp.evalFinsetIccNat (m + 1) n em' en
        match __x with
          | ⟨s, hs⟩ => pure ⟨q(insert «$em» «$s»), q(⋯)⟩
      else
        have hnm := q(⋯);
        pure ⟨q(∅), q(⋯)⟩
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `min j j'` is an arbitrary choice of object to the left of both `j` and `j'`,
whose existence is ensured by `IsCofiltered`.
 -/
CategoryTheory.IsCofiltered.min : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.IsCofilteredOrEmpty C] → C → C → C
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.denote_go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool)
  (lhs rhs : BitVec w) (n d q r : aig.RefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = false) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = false) →
          0#w < rhs →
            ∀ (idx : ℕ) (hidx : idx < w),
              ⟦assign,
                  { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w n d w 0 q r).aig,
                    ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w n d w 0 q r).r.get idx hidx }⟧ =
                (lhs % rhs).getLsbD idx
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (x : ℕ),
  Std.DTreeMap.Internal.Impl.leaf.entryAtIdx! x =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.entryAtIdx!" 467 16
      "Out-of-bounds access"
-- Mathlib.Topology.ContinuousMap.Defs
instCoeTCContinuousMap : {F : Type u_1} →
  {X : Type u_2} →
    {Y : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : FunLike F X Y] → [ContinuousMapClass F X Y] → CoeTC F C(X, Y)
-- Mathlib.NumberTheory.MulChar.Basic
/-- If the domain has a zero (and is nontrivial), then `χ 0 = 0`.  -/
MulChar.map_zero : ∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommMonoidWithZero R] [Nontrivial R]
  (χ : MulChar R R'), χ 0 = 0
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instSub : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Sub (LeftInvariantDerivation I G)
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the right-most term is one in terms of
groups. For a diagram explaining the variables, see the module docstring.  -/
MonoidHom.injective_of_surjective_of_injective_of_right_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : Group M₁]
  [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group N₁] [inst_4 : Group N₂] [inst_5 : Group N₃] (f₁ : M₁ →* M₂)
  (f₂ : M₂ →* M₃) (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.MulExact ⇑f₁ ⇑f₂ →
        Function.MulExact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Injective ⇑i₃
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for nonnegative `p : ℝ`, `|X| ^ p * exp (v * X)` is integrable.  -/
ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
        ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => |X ω| ^ p * Real.exp (v * X ω)) μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_empty : ∀ {α : Type u} {β : α → Type v}, ∅.keys = []
-- Mathlib.GroupTheory.CoprodI
/-- Given a pair `(head, tail)`, we can form a word by prepending `head` to `tail`, except if `head`
is `1 : M i` then we have to just return `Word` since we need the result to be reduced.  -/
Monoid.CoprodI.Word.rcons : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [(i : ι) → DecidableEq (M i)] → {i : ι} → Monoid.CoprodI.Word.Pair M i → Monoid.CoprodI.Word M
-- Mathlib.Order.Cover
/-- **Alias** of `wcovBy_of_le_of_le`. -/
LE.le.wcovBy_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → b ≤ a → a ⩿ b
-- Mathlib.Computability.Partrec
Computable.option_bind : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → Option β} {g : α → β → Option σ}, Computable f → Computable₂ g → Computable fun a => (f a).bind (g a)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The short complex `(G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A`.  -/
groupHomology.shortComplexH1 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_incl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J]
  [W.IsStableUnderTransfiniteComposition] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) (j : J),
  W (h.incl.app j)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.Finite.forgetPreservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.forget R)
-- Std.Data.Iterators.Lemmas.Producers.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : CategoryTheory.CatCenter C) {X Y : C} (f : X ⟶ Y),
  z • f = CategoryTheory.CategoryStruct.comp f (z.app Y)