mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → β'}
  {p : β' → m (ULift.{w, 0} Bool)}, Std.IterM.anyM p (Std.IterM.map f it) = Std.IterM.anyM (fun x => p (f x)) it
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instCoeSortType : {k : Type u} →
  {G : Type v} → [inst : TopologicalSpace k] → [inst_1 : Ring k] → [inst_2 : Monoid G] → CoeSort (TopRep k G) (Type w)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.basisSingleton.eq_1 : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
  [inst_3 : Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0),
  FiniteDimensional.basisSingleton ι h v hv =
    {
      repr :=
        {
          toFun := fun w =>
            fun₀ | default => ((Module.basisUnique ι h).repr w) default / ((Module.basisUnique ι h).repr v) default,
          map_add' := ⋯, map_smul' := ⋯, invFun := fun f => f default • v, left_inv := ⋯, right_inv := ⋯ } }
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instDecidableEqHom : {ι : Type u_1} → {a a_1 : CategoryTheory.Pairwise ι} → [DecidableEq ι] → DecidableEq (a.Hom a_1)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.mem_comap : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {x : M} {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R₂ M₂}, x ∈ Submodule.comap f p ↔ f x ∈ p
-- Aesop.Search.SearchM
Aesop.SearchM.instMonadLiftTreeM : {Q : Type} → [inst : Aesop.Queue Q] → MonadLift Aesop.TreeM (Aesop.SearchM Q)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- If `f` has a continuous left inverse, its range admits a closed complement.  -/
ContinuousLinearMap.HasLeftInverse.closedComplemented_range : ∀ {R : Type u_7} {E : Type u_8} {F : Type u_10} [inst : Ring R] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : Module R F] {f : E →L[R] F},
  f.HasLeftInverse → (↑f).range.ClosedComplemented
-- Mathlib.Topology.EMetricSpace.Defs
WeakEMetricSpace.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {m m' : WeakEMetricSpace α}, m = m' ↔ m.toEDist = m'.toEDist
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Abelian.FreydMitchell.functor C)
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.ordConnected : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → s.OrdConnected
-- Mathlib.LinearAlgebra.Ray
/-- An arbitrary `RayVector` giving a ray.  -/
Module.Ray.someRayVector : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.Ray R M → RayVector R M
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt8HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Init.Data.UInt.Bitwise
instIdempotentOpUSizeHAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.Order.Fin.Basic
Fin.val_top : ∀ (n : ℕ) [inst : NeZero n], ↑⊤ = n - 1
-- Mathlib.Algebra.Quandle
Rack.self_invAct_eq_iff_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Rack.invAct x x = Rack.invAct y y ↔ x = y
-- Mathlib.Order.Atoms
IsStronglyCoatomic.mk : ∀ {α : Type u_5} [inst : Preorder α], (∀ (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b) → IsStronglyCoatomic α
-- Mathlib.Order.Closure
ClosureOperator.conjBy_apply : ∀ {α : Type u_4} {β : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] (c : ClosureOperator α) (e : α ≃o β) (a : β),
  (c.conjBy e) a = (e.conj ↑c) a
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.rfl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x : M}, x ≡ x [SMOD U]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.of_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Init.System.IOError
IO.Error.mkUnsupportedOperation : UInt32 → String → IO.Error
-- Mathlib.Order.Max
noMaxOrder_iff' : ∀ (α : Type u_3) [inst : LT α], NoMaxOrder α ↔ ∀ (a : α), ∃ b, a < b
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast.match_1.eq_3 : ∀ {α : Type u_1} (motive : (x : List α) → x ≠ [] → Sort u_2) (head b : α) (as : List α) (x : head :: b :: as ≠ [])
  (h_1 : (h : [] ≠ []) → motive [] h) (h_2 : (a : α) → (x : [a] ≠ []) → motive [a] x)
  (h_3 : (head b : α) → (as : List α) → (x : head :: b :: as ≠ []) → motive (head :: b :: as) x),
  (match head :: b :: as, x with
    | [], h => h_1 h
    | [a], x => h_2 a x
    | head :: b :: as, x => h_3 head b as x) =
    h_3 head b as x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_mul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)
      CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.sort.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.Key.sort = 1
-- Lean.Meta.InferType
Lean.Meta.throwFunctionExpected : {α : Type} → Lean.Expr → Lean.MetaM α
-- Lean.Data.Options
Lean.MonadWithOptions.mk : {m : Type → Type} → ({α : Type} → (Lean.Options → Lean.Options) → m α → m α) → Lean.MonadWithOptions m
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu.0.CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite.match_1.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (G : C) (motive : (CategoryTheory.End G)ᵐᵒᵖ → Sort u_3)
  (f : CategoryTheory.End G) (h_1 : (f : CategoryTheory.End G) → motive { unop' := f }),
  (match { unop' := f } with
    | { unop' := f } => h_1 f) =
    h_1 f
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.vadd_symm : ∀ {𝕜 : 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} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : AddGroup G]
  [inst_12 : AddAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffVAdd I I' n G M] (g : G),
  (Diffeomorph.vadd I I' n g).symm = Diffeomorph.vadd I I' n (-g)
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_group_smul_left : ∀ {R : Type u_1} {G : Type u_2} [inst : CommSemiring R] [inst_1 : Group G] [inst_2 : MulAction G R]
  [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R), IsCoprime (x • y) z ↔ IsCoprime y z
-- Std.Http.Data.Request
/-- Sets the HTTP version for the request being built.
 -/
Std.Http.Request.Builder.version : Std.Http.Request.Builder → Std.Http.Version → Std.Http.Request.Builder
-- Mathlib.MeasureTheory.Measure.Map
/-- Mapping a measure twice is the same as mapping the measure with the composition. This version is
for measurable functions. See `map_map_of_aemeasurable` when they are just ae measurable.  -/
MeasureTheory.Measure.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β},
  Measurable g →
    Measurable f → MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
-- Mathlib.Data.Complex.Basic
Complex.ofReal_eq_one : ∀ {z : ℝ}, ↑z = 1 ↔ z = 1
-- Mathlib.MeasureTheory.Measure.Trim
ae_eq_trim_of_measurable : ∀ {α : Type u_3} {β : Type u_4} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
  [MeasurableEq β] (hm : m ≤ m0) {f g : α → β}, Measurable f → Measurable g → f =ᵐ[μ] g → f =ᵐ[μ.trim hm] g
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i j : σ) [Nontrivial R],
  MvPolynomial.degreeOf i (MvPolynomial.X j) = if i = j then 1 else 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.comp_symm_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α),
  g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.Tactic.Linarith.Datatypes
/-- `Comp` has a lex order. First the `ineq`s are compared, then the `coeff`s.  -/
Mathlib.Tactic.Linarith.Comp.cmp : Mathlib.Tactic.Linarith.Comp → Mathlib.Tactic.Linarith.Comp → Ordering
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_add : ∀ (θ₁ θ₂ : Real.Angle), (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
-- Mathlib.Algebra.Group.Prod
MonoidHom.coe_fst : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N], ⇑(MonoidHom.fst M N) = Prod.fst
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_reverse`. -/
List.SortedLE.reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE → l.reverse.SortedGE
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadLift_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ρ : Type u}
  {epost : EPred} (x : m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp x (fun a => post a r) epost ⦄ MonadLift.monadLift x ⦃ post; epost ⦄
-- Init.Data.Vector.Lex
_private.Init.Data.Vector.Lex.0.Vector.lex.eq_1 : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] (xs ys : Vector α n) (lt : α → α → Bool),
  xs.lex ys lt =
    (do
        let __s ←
          forIn' (0...n) (none, ()) fun i h __s =>
              have __r := __s;
              if lt xs[i] ys[i] = true then pure (ForInStep.done (some true, ()))
              else
                if (xs[i] != ys[i]) = true then pure (ForInStep.done (some false, ()))
                else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure false).run
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (X : C) [inst_5 : CategoryTheory.Injective X],
  CategoryTheory.IsIso ((CategoryTheory.InjectiveResolution.self X).toRightDerivedZero' F)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Subsemiring A)
  (h : ∀ (r : R), (algebraMap R A) r ∈ s.carrier) (x : A), x ∈ { toSubsemiring := s, algebraMap_mem' := h } ↔ x ∈ s
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_mul_self_add : ∀ {a b c : ℤ}, a ∣ b * a + c ↔ a ∣ c
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNat.inj : ∀ {ι : Type u_2} {X : Type u_5} {Y : ι → Type u_6} {f : (i : ι) → X → Y i} {ofPiNat ofPiNat_1 : X},
  { ofPiNat := ofPiNat } = { ofPiNat := ofPiNat_1 } → ofPiNat = ofPiNat_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instSubtypeMemSubalgebraOfFieldPrimeComplAsIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain ↥(Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)
-- Mathlib.Algebra.WithConv
WithConv.symm_congr_apply : ∀ {A : Type u_2} {B : Type u_3} (f : A ≃ B) (x : WithConv B),
  (WithConv.congr f).symm x = WithConv.toConv (f.symm x.ofConv)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles in a vector space are translation invariant.  -/
EuclideanGeometry.angle_sub_const : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V),
  EuclideanGeometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = EuclideanGeometry.angle v₁ v₂ v₃
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.pow_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : HPow α ℕ α]
  [Lean.Grind.ToInt.Pow α i] {a : α} (k : ℕ) (a' : ℤ), ↑a = a' → ↑(a ^ k) = i.wrap (a' ^ k)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.sub_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x y : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (x - y).2 = x.2 - y.2
-- Mathlib.Topology.AlexandrovDiscrete
Quotient.instAlexandrovDiscrete : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Setoid α}, AlexandrovDiscrete (Quotient s)
-- Mathlib.RingTheory.Valuation.Basic
/-- The isomorphism between the `ValueGroup₀`'s of two equivalent valuations.  -/
Valuation.IsEquiv.orderMonoidIso : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : LinearOrderedCommGroupWithZero Γ₀] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] →
          [inst_2 : Ring R] →
            {v : Valuation R Γ₀} →
              {w : Valuation R Γ'₀} →
                v.IsEquiv w → (MonoidWithZeroHom.ofClass v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass w).ValueGroup₀
-- Mathlib.Order.Defs.Unbundled
/-- A version of `comm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there.  -/
comm_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Symm r] {a b : α}, r a b ↔ r b a
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.volume_real_fundamentalDomain : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (b : Module.Basis ι ℝ (ι → ℝ)),
  MeasureTheory.volume.real (ZSpan.fundamentalDomain b) = |(Matrix.of ⇑b).det|
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct_whiskerLeft : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (X x x_1 : (i : I) → C i) (f : x ⟶ x_1) (i : I),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f i =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X i) (f i)
-- Mathlib.Data.Vector.Basic
/-- The last element of a `Vector`, given that the vector is at least one element.  -/
List.Vector.last : {α : Type u_1} → {n : ℕ} → List.Vector α (n + 1) → α
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion.eq_1 : ∀ {α : Type u} {ι : Sort v} (s : ι → Set α), Set.iUnion s = iSup s
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Fintype ι] {ι₂ : Type u_5} [inst_5 : Fintype ι₂] {p : ι → P},
  AffineIndependent k p →
    ∀ {w₁ : ι → k} {w₂ : ι₂ → k},
      ∑ i, w₁ i = 1 →
        ∑ i, w₂ i = 1 →
          ∀ (e : ι₂ ↪ ι),
            (Finset.affineCombination k Finset.univ (p ∘ ⇑e)) w₂ = (Finset.affineCombination k Finset.univ p) w₁ →
              (Set.range ⇑e).indicator (Function.extend (⇑e) w₂ 0) = w₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastUmod : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig input).vec.get idx hidx }⟧ =
          (lhs % rhs).getLsbD idx
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSemigroupWithZero : {M₀ : Type u_1} →
  [inst : TopologicalSpace M₀] →
    [inst_1 : SemigroupWithZero M₀] → [ContinuousMul M₀] → SemigroupWithZero (SeparationQuotient M₀)
-- Mathlib.Algebra.Order.Floor.Defs
Int.lt_floor_iff : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, z < ⌊a⌋ ↔ ↑z + 1 ≤ a
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_infs_of_notMem : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α} [inst_2 : DecidableLE α]
  [inst_3 : BoundedOrder α], a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t → (s ⊼ t).truncatedSup a = ⊤
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.whiskerLeft_id_star : ∀ {x : AugmentedSimplexCategory},
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft x
      (CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x CategoryTheory.WithInitial.star)
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAtFilter.congr_simp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f f_1 : 𝕜 → F),
  f = f_1 →
    ∀ (f' f'_1 : F),
      f' = f'_1 → ∀ (L L_1 : Filter (𝕜 × 𝕜)), L = L_1 → HasDerivAtFilter f f' L = HasDerivAtFilter f_1 f'_1 L_1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.injective_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, Function.Injective BoxIntegral.Prepartition.boxes
-- Mathlib.Dynamics.Transitive
/-- An action of a monoid `M` on a topological space `α` is called *topologically transitive* if for
any pair of nonempty open sets `U` and `V` in `α` there exists an `m : M` such that `(m • U) ∩ V` is
nonempty.  -/
MulAction.IsTopologicallyTransitive : (M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [TopologicalSpace α] → [MulAction M α] → Prop
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ext_mem_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashSet α},
  m₁ = m₂ ↔ ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂
-- Mathlib.Analysis.Asymptotics.TVS
/-- If `f` converges along `l` to a finite limit `x`, then `f =O[𝕜, l] 1`.  -/
Asymptotics.Filter.Tendsto.isBigOTVS_one : ∀ {α : Type u_1} (𝕜 : Type u_3) {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} {f : α → E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  {x : E}, Filter.Tendsto f l (nhds x) → f =O[𝕜; l] fun x => 1
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.down_Rel : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α] (i j : α),
  (ComplexShape.down α).Rel i j = (j + 1 = i)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (carrier : Type v) [instRing : Ring carrier]
  [instBialgebra : Bialgebra R carrier],
  sizeOf { carrier := carrier, instRing := instRing, instBialgebra := instBialgebra } =
    1 + sizeOf carrier + sizeOf instRing + sizeOf instBialgebra
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] {it : Std.IterM Id α},
  it.internalState.next = some a → it.IsPlausibleOutput a
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i ≤ j`  -/
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            (hj : ¬IsMax j) →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} →
                  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) →
                    (i : J) →
                      (hi : i ≤ j) →
                        (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).obj ⟨i, ⋯⟩ ≅ F.obj ⟨i, hi⟩
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.anti_right : ∀ {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β}, H ≤ G₁ → G₁ ≤ G → H.IsClosedSubgraph G → H.IsClosedSubgraph G₁
-- Mathlib.Topology.Algebra.Monoid
/-- A version of `Pi.continuousAdd` for non-dependent functions. It is needed
because sometimes Lean fails to use `Pi.continuousAdd` for non-dependent functions.  -/
Pi.continuousAdd' : ∀ {ι : Type u_1} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousAdd (ι → M)
-- Mathlib.Logic.Function.Conjugate
/-- If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`,
then `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`.  -/
Function.Semiconj.option_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → Function.Semiconj (Option.map f) (Option.map ga) (Option.map gb)
-- Lean.Parser.Command
Lean.Parser.Command.structParent : Lean.Parser.Parser
-- Mathlib.Tactic.LinearCombination
/-- A proof of `a = b`, `a ≤ b`, or `a < b` (according to the value of `Ineq`).  -/
Mathlib.Tactic.LinearCombination.Expanded.proof : Mathlib.Ineq → Lean.Term → Mathlib.Tactic.LinearCombination.Expanded
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toIsAffineHom : AlgebraicGeometry.IsAffineHom f],
  (∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).IsIntegral) →
    AlgebraicGeometry.IsIntegralHom f
-- Mathlib.Order.Filter.Map
Filter.disjoint_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β},
  Function.Surjective m → (Disjoint (Filter.comap m g₁) (Filter.comap m g₂) ↔ Disjoint g₁ g₂)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.le_ker_coroot' : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] {P : RootPairing ι K M N}
  (q : ↥P.invtRootSubmodule) {k : ι}, P.root k ∉ ↑q → ↑q ≤ LinearMap.ker (P.coroot' k)