mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If `x` is not congruent to `a` modulo `p`, then `toIcoDiv` is locally constant near `x`.  -/
eventuallyEq_toIcoDiv_nhds : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → toIcoDiv hp a =ᶠ[nhds x] fun x_1 => toIcoDiv hp a x
-- Mathlib.Algebra.Notation.Support
Pi.support_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i : ι} {a : M} [inst_2 : DecidableEq M],
  Function.support (Pi.single i a) = if a = 0 then ∅ else {i}
-- Init.Grind.Norm
Lean.Grind.beq_eq_decide_eq : ∀ {α : Type u_1} {x : BEq α} [LawfulBEq α] [inst : DecidableEq α] (a b : α), (a == b) = decide (a = b)
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.OreLocalization.smul' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → R → ↥S → X → ↥S → OreLocalization S X
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link2.eq_3 : ∀ {α : Type u} {β : α → Type v} (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) (szr_1 : ℕ) (k''_1 : α) (v''_1 : β k''_1)
  (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β)
  (hr_4 : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced),
  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').link2
      (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr_2 hr_4 =
    if h₁ : Std.DTreeMap.Internal.delta * szr < szr_1 then
      match (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').link2 l''_1 ⋯ ⋯ with
      | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceLErase k''_1 v''_1 ℓ r''_1 ⋯ ⋯ ⋯, balanced_impl := ⋯,
          size_impl := ⋯ }
    else
      if h₂ : Std.DTreeMap.Internal.delta * szr_1 < szr then
        match r''.link2 (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) ⋯ ⋯ with
        | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceRErase k'' v'' l'' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
      else
        {
          impl :=
            (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').glue
              (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) ⋯ ⋯ ⋯,
          balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsNoetherianRing R] [inst_4 : Module.Finite R M] (x : TensorProduct R (AdicCompletion I R) M),
  (AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M) x = (AdicCompletion.ofTensorProduct I M) x
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The object on position `pq` on the `r`th page of the spectral sequence.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            CategoryTheory.Abelian.SpectralObject C ι →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ →
                    (r : ℤ) →
                      κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX._auto_1 → C
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
/-- The singular chain complex functor with coefficients in `C`.  -/
AlgebraicTopology.singularChainComplexFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        CategoryTheory.Functor C (CategoryTheory.Functor TopCat (ChainComplex C ℕ))
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.constCompEvaluationObj_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C) (X_1 : D),
  (CategoryTheory.Functor.constCompEvaluationObj D X).inv.app X_1 = CategoryTheory.CategoryStruct.id X_1
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.lTensor.directLimit_apply : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { P // P.FG }] (Q : { Q // Q.FG })
  (u : TensorProduct R M ↥↑Q),
  (Submodule.FG.lTensor.directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q => TensorProduct R M ↥↑Q)
          (fun x x_1 hPQ => LinearMap.lTensor M (Submodule.inclusion hPQ)) Q)
        u) =
    (LinearMap.lTensor M (↑Q).subtype) u
-- Lean.Parser.Basic
/-- The `linebreak` parser requires that there is at least one line break at this location.
(The line break may be inside a comment.)

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkLinebreakBefore : optParam String "line break" → Lean.Parser.Parser
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- The ramification index of `P` over `p` is the largest exponent `n` such that
`p` is contained in `P^n`.

In particular, if `p` is not contained in `P^n`, then the ramification index is 0.

If there is no largest such `n` (e.g. because `p = ⊥`), then `ramificationIdx'` is
defined to be 0.

Note: This definition of ramification index will eventually be replaced by `Ideal.ramificationIdx`.
 -/
Ideal.ramificationIdx' : {R : Type u} → [inst : CommRing R] → {S : Type v} → [inst_1 : CommRing S] → [Algebra R S] → Ideal R → Ideal S → ℕ
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_two : ∀ {R : Type u_6} [inst : AddCommMonoid R] (A : Matrix (Fin 2) (Fin 2) R), A.trace = A 0 0 + A 1 1
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
finrank_zero_iff_forall_zero : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V], Module.finrank K V = 0 ↔ ∀ (x : V), x = 0
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.consFixedLengthDigits.eq_1 : ∀ {b : ℕ} (hb : 1 < b) (l d : ℕ),
  List.consFixedLengthDigits hb l d = Finset.image (fun L => d :: L) (List.fixedLengthDigits hb l)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is an injection between them,
then the induced map on their free groups is also injective.  -/
FreeGroup.map_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → Function.Injective ⇑(FreeGroup.map f)
-- Std.Data.TreeSet.Raw.Iterator
_private.Std.Data.TreeSet.Raw.Iterator.0.Std.TreeSet.Raw.iter.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} (m : Std.TreeSet.Raw α cmp), m.iter = Std.Iter.map (fun e => e.1) m.inner.iter
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.Commute.minimalPeriod_of_comp_dvd_lcm : ∀ {α : Type u_1} {f : α → α} {x : α} {g : α → α},
  Function.Commute f g →
    Function.minimalPeriod (f ∘ g) x ∣ (Function.minimalPeriod f x).lcm (Function.minimalPeriod g x)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β], ↑0 =ᵐ[μ] 0
-- Mathlib.Logic.Equiv.Set
/-- If `f : α → β` is an injective function, then domain `α` is equivalent to the range of `f`.  -/
Equiv.ofInjective : {α : Sort u_3} → {β : Type u_4} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableLocallyUniformly_iff_hasProdLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], MultipliableLocallyUniformly f ↔ HasProdLocallyUniformly f fun x => ∏' (i : ι), f i x
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isHenstock_single : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsHenstock
-- Mathlib.Data.NNReal.Defs
NNReal.inv_le : ∀ {r p : NNReal}, r ≠ 0 → (r⁻¹ ≤ p ↔ 1 ≤ r * p)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.ext : ∀ {α : Type u} {a b : Multiplicative α}, Multiplicative.toAdd a = Multiplicative.toAdd b → a = b
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.inductionOn₃ : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {α₃ : Type u_4} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop}
  {rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop} {rels₃ : FreeMonoid α₃ → FreeMonoid α₃ → Prop}
  {δ : PresentedMonoid rels₁ → PresentedMonoid rels₂ → PresentedMonoid rels₃ → Prop} (q₁ : PresentedMonoid rels₁)
  (q₂ : PresentedMonoid rels₂) (q₃ : PresentedMonoid rels₃),
  (∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂) (c : FreeMonoid α₃),
      δ ((PresentedMonoid.mk rels₁) a) ((PresentedMonoid.mk rels₂) b) ((PresentedMonoid.mk rels₃) c)) →
    δ q₁ q₂ q₃
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_add : ∀ (x y : ℂ), Complex.exp (x + y) = Complex.exp x * Complex.exp y
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower upper : α), (sizeOf lower<...upper) = 1 + sizeOf lower + sizeOf upper
-- Mathlib.CategoryTheory.GradedObject
/-- A type synonym for `β → C`, used for `β`-graded objects in a category `C`.  -/
CategoryTheory.GradedObject : Type w → Type u → Type (max w u)
-- Mathlib.Condensed.Discrete.LocallyConstant
LightCondSet.LocallyConstant.instFaithfulFunctor : LightCondSet.LocallyConstant.functor.Faithful
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.maxKey! = t.maxKeyD default
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The adic topology associated to an ideal `I`. This topology admits powers of `I` as a basis of
neighborhoods of zero. It is compatible with the ring structure and is non-archimedean.  -/
Ideal.adicTopology : {R : Type u_1} → [inst : CommRing R] → Ideal R → TopologicalSpace R
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.sup_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F F' : I.Filtration M), (F ⊔ F').N = F.N ⊔ F'.N
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_zero : Hyperreal.Infinitesimal 0
-- Mathlib.Algebra.Ring.Ext
Semiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : Semiring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Order.Heyting.Hom
CoheytingHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : CoheytingAlgebra α] → [inst_1 : CoheytingAlgebra β] → PartialOrder (CoheytingHom α β)
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNat_lt_true : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = false → a < b
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.notMem_bot : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {x : α → M}, x ∉ ⊥
-- Std.Data.HashSet.Basic
/-- Two hash sets are equivalent in the sense of `Equiv` iff all their values are equal.
 -/
Std.HashSet.Equiv : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Std.HashSet α → Prop
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `AddLECancellable.tsub_eq_of_eq_add_rev'` for a version assuming that `a = b + c` itself is
cancellable rather than `b`.  -/
AddLECancellable.tsub_eq_of_eq_add_rev : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable b → a = b + c → a - b = c
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun x = 0 ↔ x = 0
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
mapsTo_extChartAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x : M},
  s ⊆ (chartAt H x).source → Set.MapsTo (↑(extChartAt I x)) s (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
-- Init.Control.Lawful.Basic
/-- `pure` after `seq` is equivalent to `Functor.map`.

This means that `pure` really is pure when occurring just after `seq`.
 -/
LawfulApplicative.seq_pure : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : f (α → β)) (x : α),
  g <*> pure x = (fun h => h x) <$> g
-- Init.Data.SInt.Basic
instShiftRightInt64 : ShiftRight Int64
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum.  -/
linearIndepOn_iff' : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  LinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
-- Mathlib.GroupTheory.QuotientGroup.Basic
MonoidHom.domRestrictHomKerEquiv.eq_1 : ∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal],
  MonoidHom.domRestrictHomKerEquiv A H =
    {
      toFun := fun x =>
        match x with
        | ⟨f, hf⟩ => QuotientGroup.lift H f ⋯,
      invFun := fun f => ⟨f.comp (QuotientGroup.mk' H), ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Fin.Tuple.BubbleSortInduction
/-- *Bubble sort induction*: Prove that the sorted version of `f` has some property `P`
if `f` satisfies `P` and `P` is preserved when swapping two antitone values.  -/
Tuple.bubble_sort_induction : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop},
  P f → (∀ (g : Fin n → α) (i j : Fin n), i < j → g j < g i → P g → P (g ∘ ⇑(Equiv.swap i j))) → P (f ∘ ⇑(Tuple.sort f))
-- Mathlib.Data.Fintype.Card
/-- **Alias** of the forward direction of `Finite.injective_iff_bijective`. -/
Function.Injective.bijective_of_finite : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Injective f → Function.Bijective f
-- Mathlib.Algebra.Ring.Rat
Rat.mul_den_eq_num : ∀ (q : ℚ), q * ↑q.den = ↑q.num
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCoseparating_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  P.unop.IsCoseparating ↔ P.IsSeparating
-- Mathlib.Data.Part
/-- We give `Part α` the order where everything is greater than `none`.  -/
Part.instPartialOrder : {α : Type u_1} → PartialOrder (Part α)
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_ric : ∀ {α : Type u_1} {xs : List α} {hi : ℕ},
  Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (List.take (hi + 1) xs).toArray
-- Mathlib.Algebra.BigOperators.Finprod
/-- See `finsum_comp`, `Fintype.sum_bijective` and `Finset.sum_bij`.  -/
finsum_eq_of_bijective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → M} (e : α → β),
  Function.Bijective e → (∀ (x : α), f x = g (e x)) → ∑ᶠ (i : α), f i = ∑ᶠ (j : β), g j
-- Mathlib.Order.Disjointed
/-- `disjointed f` is the unique map `d : ι → α` such that `d` has the same partial sups as `f`,
and `d i` and `d j` are disjoint whenever `i < j`.  -/
disjointed_unique : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : PartialOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] {f d : ι → α},
  (∀ {i j : ι}, i < j → Disjoint (d i) (d j)) → partialSups d = partialSups f → d = disjointed f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.add : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A} {f' q' : PowerSeries A}
  {r' : Polynomial A},
  f.IsWeierstrassDivisionAt g q r I →
    f'.IsWeierstrassDivisionAt g q' r' I → (f + f').IsWeierstrassDivisionAt g (q + q') (r + r') I
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_mul_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) '' Set.Iio b = Set.Iio (a * b)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃' : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ),
  CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))) →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃'._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃'._auto_3),
      CategoryTheory.IsIso (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_sub_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), deriv (fun x => c - x) x = -1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.concat.eq_2 : ∀ (m₂ : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  (Lean.Grind.CommRing.Mon.mult p m).concat m₂ = Lean.Grind.CommRing.Mon.mult p (m.concat m₂)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_preimage : ∀ {α : Type u_2} [inst : Neg α] {s : Set α}, Neg.neg ⁻¹' s = -s
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.ofNat_ctorIdx : ∀ (x : Lean.Meta.ProjReductionKind), Lean.Meta.ProjReductionKind.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.inter_vadd_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t : Finset β}
  [inst_2 : DecidableEq α], s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instBEqConfig : BEq Mathlib.Tactic.AtomM.Recurse.Config
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBit.mk.sizeOf_spec : ∀ (var : ℕ) {w : ℕ} (idx : Fin w), sizeOf { var := var, w := w, idx := idx } = 1 + sizeOf var + sizeOf w + sizeOf idx
-- ProofWidgets.Component.RefreshComponent
/-- Version of the current HTML tree.
It should increase by `1` with each state update.  -/
ProofWidgets.RefreshComponent.RefreshState.idx : ProofWidgets.RefreshComponent.RefreshState → ℕ
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If F and G are naturally isomorphic functors, establish an equivalence of hom-sets.  -/
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} → (F ≅ F') → {X : C} → {Y : D} → (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y)
-- Mathlib.RingTheory.Ideal.Defs
Ideal.mem_of_dvd : ∀ {α : Type u} {a b : α} [inst : CommSemiring α] (I : Ideal α), a ∣ b → a ∈ I → b ∈ I
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborator for `const` expressions.
This is not registered as a delaborator, as `const` is not an expression kind
(see [delab] description and `Lean.PrettyPrinter.Delaborator.getExprKind`).
Rather, it is called through the `app` delaborator.
 -/
Lean.PrettyPrinter.Delaborator.delabConst : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.RelSeries
RelSeries.smash.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : p.last = q.head),
  p.smash q connect =
    { length := p.length + q.length, toFun := fun i => Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun i, step := ⋯ }
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.recZeroCoe_zero : ∀ {α : Type u} {motive : WithZero α → Sort u_1} (h₁ : motive 0) (h₂ : (a : α) → motive ↑a),
  WithZero.recZeroCoe h₁ h₂ 0 = h₁
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `monovary_iff_exists_monotone`. -/
Monovary.exists_monotone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g → ∃ x, Monotone f ∧ Monotone g
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i₁ i₂ i₃ : ι)
  {Z : ↑(F.obj { as := Opposite.op (X i₁) }).obj}
  (h :
    (F.map (f i₁).op.toLoc).l.toFunctor.obj
        ((F.map (f i₂).op.toLoc).r.toFunctor.obj
          ((F.map (f i₂).op.toLoc).l.toFunctor.obj ((F.map (f i₃).op.toLoc).r.toFunctor.obj (self.obj i₃)))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (self.hom i₁ i₂)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂ i₃))) h) =
    CategoryTheory.CategoryStruct.comp (self.hom i₁ i₃)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (f i₁).op.toLoc).l.toFunctor.map
          ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (self.obj i₃))))
        h)
-- Mathlib.Computability.Primrec.List
/-- If `R a b` is decidable, then given `L : List α` and `b : β`, it is primitive recursive
to filter `L` for elements `a` with `R a b`  -/
PrimrecRel.listFilter : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [inst : Primcodable α] [inst_1 : Primcodable β],
  PrimrecRel R → ∀ [inst_2 : DecidableRel R], Primrec₂ fun L b => List.filter (fun a => decide (R a b)) L
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.instId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} → CategoryTheory.Bicategory.Comonad (CategoryTheory.CategoryStruct.id a)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listDecode.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (n : ℕ) (f : L.Functions n) (l : List (α ⊕ (i : ℕ) × L.Functions i)),
  FirstOrder.Language.Term.listDecode (Sum.inr ⟨n, f⟩ :: l) =
    if h : n ≤ (FirstOrder.Language.Term.listDecode l).length then
      (FirstOrder.Language.func f fun i => (FirstOrder.Language.Term.listDecode l)[i]) ::
        List.drop n (FirstOrder.Language.Term.listDecode l)
    else []
-- Lean.Meta.InferType
/-- Auxiliary function for processing the result for the binders `forallE` and `letE`.  -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowProposition'.processResult : Lean.Meta.ArrowPropResult✝ → Lean.Expr → Lean.Meta.ArrowPropResult✝