mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'''} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α Id n]
  [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_14 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ}
  {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← liftM (f b).run
          g d c)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.mapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is continuous if each individual
function is.  -/
continuous_tsum : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
  [inst_2 : TopologicalSpace β] {f : α → β → F},
  (∀ (i : α), Continuous (f i)) →
    Summable u → (∀ (n : α) (x : β), ‖f n x‖ ≤ u n) → Continuous fun x => ∑' (n : α), f n x
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_neg : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Neg α] (A : Matrix m n α),
  (-A).submatrix = -A.submatrix
-- Mathlib.Algebra.GCDMonoid.Nat
Int.gcd_nonneg : ∀ (i j : ℤ), 0 ≤ gcd i j
-- Mathlib.Data.ENNReal.Inv
ENNReal.half_pos : ∀ {a : ENNReal}, a ≠ 0 → 0 < a / 2
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_singleton_trans : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y z : M},
  x ∈ R ∙ y → y ∈ R ∙ z → x ∈ R ∙ z
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- A presheaf is called an ind-object if it can be written as a filtered colimit of representable
presheaves.  -/
CategoryTheory.Limits.IsIndObject : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor Cᵒᵖ (Type v) → Prop
-- Lean.LocalContext
/-- Returns `true` if this is an `ldecl` with `nondep := true`.  -/
Lean.LocalDecl.isNondep : Lean.LocalDecl → Bool
-- Init.Data.List.Attach
/-- “Attaches” individual proofs to a list of values that satisfy a predicate `P`, returning a list of
elements in the corresponding subtype `{ x // P x }`.

`O(1)`.
 -/
List.attachWith : {α : Type u_1} → (l : List α) → (P : α → Prop) → (∀ x ∈ l, P x) → List { x // P x }
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop : ∀ (D : AlgebraicGeometry.Scheme.GlueData),
  CategoryTheory.Limits.PreservesColimit D.diagram.multispan AlgebraicGeometry.Scheme.forgetToTop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, (Std.DHashMap.filter (fun a x => f a) m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.limitMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] →
        Monoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- A property of morphisms `P` in `C` is local at the source with respect to the precoverage `K` if
it respects isomorphisms, and:
`P` holds for `f : X ⟶ Y` if and only if it holds for the restrictions of `f` to `Uᵢ` for a
`0`-hypercover `{Uᵢ}` of `X` in the precoverage `K`.
 -/
CategoryTheory.MorphismProperty.IsLocalAtSource : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.Precoverage C → Prop
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.supportedRecursors : Array Lean.Name
-- Mathlib.Order.CompleteLattice.Basic
iInf_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (i : ι), iInf f ≤ f i
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.mk : Array Lean.HeadIndex → Std.HashSet Lean.HeadIndex → Std.HashSet ℕ → Lean.Meta.Grind.NormalizePattern.State
-- Mathlib.Data.Num.ZNum
ZNum.zneg_zneg : ∀ (n : ZNum), - -n = n
-- Mathlib.Topology.Order
continuous_nhdsAdjoint_dom : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] {f : α → β} {a : α} {l : Filter α},
  Continuous f ↔ Filter.Tendsto f l (nhds (f a))
-- Mathlib.Algebra.Group.Defs
inv_eq_of_mul_eq_one_right : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal of `D` below `P`,
then `P` is the only prime of `L` above `𝓟D`.
 -/
IsDecompositionField.primesOver_eq_singleton : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) [inst_4 : Algebra B L] [IsFractionRing B L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6)
  [inst_8 : Field D] [inst_9 : Algebra D L] [IsDecompositionField K L P D] [inst_11 : CommRing 𝓞D]
  [inst_12 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_14 : Algebra 𝓞D B] [inst_15 : Algebra 𝓞D L]
  [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [hP : P.IsPrime]
  [Finite ↥(MulAction.stabilizer Gal(L/K) P)] [IsIntegrallyClosed 𝓞D] [Algebra.IsIntegral 𝓞D B], 𝓟D.primesOver B = {P}
-- Mathlib.Tactic.Translate.Core
/-- Translate the source declaration and then run `addDecl`. If the kernel throws an error,
try to emit a better error message.

For efficiency in `to_dual`, we first run `updateDecl` without any `UnfoldBoundaries`,
and only if that fails do we try to include them.
The reason is that in the most common case, `to_dual` succeeds without needing to insert
unfold boundaries, and figuring out whether to insert them can be quite expensive.  -/
Mathlib.Tactic.Translate.updateAndAddDecl : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name →
    Lean.ConstantInfo →
      Mathlib.Tactic.Translate.ArgReorder →
        List ℕ → Lean.NameMap Lean.Name → Lean.MetaM (Lean.ConstantInfo × Option Mathlib.Tactic.Translate.RelevantArg)
-- Lean.Meta.LazyDiscrTree
/-- Initial entry in lazy discrimination tree  -/
Lean.Meta.LazyDiscrTree.InitEntry : Type → Type
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivationEquiv_symm_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] [inst_4 : IsScalarTower R (Polynomial R) A] (D : Derivation R (Polynomial R) A),
  (Polynomial.mkDerivationEquiv R).symm D = D Polynomial.X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMergeWith! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.Equiv t₂ →
    t₃.Equiv t₄ →
      t₁.WF →
        t₂.WF →
          t₃.WF →
            t₄.WF →
              ∀ {f : α → β → β → β},
                (Std.DTreeMap.Internal.Impl.Const.mergeWith! f t₁ t₃).Equiv
                  (Std.DTreeMap.Internal.Impl.Const.mergeWith! f t₂ t₄)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_eq_ker_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Surjective ⇑f → ∀ {H : AddSubgroup N}, AddSubgroup.comap f H = f.ker ↔ H = ⊥
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.tdiv.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_2 m n
-- Mathlib.Analysis.Complex.Order
Complex.zero_le_real : ∀ {x : ℝ}, 0 ≤ ↑x ↔ 0 ≤ x
-- Mathlib.Data.Bool.Basic
Bool.of_decide_false : ∀ {p : Prop} [inst : Decidable p], decide p = false → ¬p
-- Mathlib.Analysis.Normed.Affine.MazurUlam
/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
over `ℝ`, then `x ↦ f x - f 0` is a linear isometry equivalence.  -/
IsometryEquiv.toRealLinearIsometryEquiv : {E : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → E ≃ᵢ F → E ≃ₗᵢ[ℝ] F
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Icc_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.Icc (Fin.natAdd m i) (Fin.natAdd m j) = Set.Icc i j
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.mk.inj : ∀ {toSemiring : Lean.Meta.Sym.Arith.Semiring} {ringId : ℕ} {commSemiringInst : Lean.Expr}
  {addRightCancelInst? : Option (Option Lean.Expr)} {toQFn? : Option Lean.Expr}
  {toSemiring_1 : Lean.Meta.Sym.Arith.Semiring} {ringId_1 : ℕ} {commSemiringInst_1 : Lean.Expr}
  {addRightCancelInst?_1 : Option (Option Lean.Expr)} {toQFn?_1 : Option Lean.Expr},
  { toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
      { toSemiring := toSemiring_1, ringId := ringId_1, commSemiringInst := commSemiringInst_1,
        addRightCancelInst? := addRightCancelInst?_1, toQFn? := toQFn?_1 } →
    toSemiring = toSemiring_1 ∧
      ringId = ringId_1 ∧
        commSemiringInst = commSemiringInst_1 ∧ addRightCancelInst? = addRightCancelInst?_1 ∧ toQFn? = toQFn?_1
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAt_iff_isLittleO_nhds_zero : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
  HasGradientAt f f' x ↔ (fun h => f (x + h) - f x - inner 𝕜 f' h) =o[nhds 0] fun h => h
-- Mathlib.Data.Subtype
/-- Restriction of a function to a function on subtypes.  -/
Subtype.map : {α : Sort u_1} →
  {β : Sort u_2} → {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.baseChange_tmul : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Algebra R A] [inst_4 : Module R M₂] (B₂ : LinearMap.BilinForm R M₂) (a : A)
  (m₂ : M₂) (a' : A) (m₂' : M₂),
  ((LinearMap.BilinForm.baseChange A B₂) (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (a * a')
-- Mathlib.Topology.Separation.Regular
/-- A space is `T5Space` iff it is hereditarily `T4Space`.
 -/
t5Space_iff_forall_t4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], T5Space X ↔ ∀ (s : Set X), T4Space ↑s
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.coe_ringOfIntegersComplexConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : NumberField.RingOfIntegers K),
  ↑((NumberField.IsCMField.ringOfIntegersComplexConj K) x) = (NumberField.IsCMField.complexConj K) ↑x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- If two continuous `R`-multilinear maps from `R` are equal on 1, then they are equal.

This is the multilinear version of `ContinuousLinearMap.ext_ring`.  -/
ContinuousMultilinearMap.ext_ring : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : TopologicalSpace M₂] [Finite ι] [inst_5 : TopologicalSpace R]
  ⦃f g : ContinuousMultilinearMap R (fun x => R) M₂⦄, ((f fun x => 1) = g fun x => 1) → f = g
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.iter : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RxoIterator α β → Std.DTreeMap.Internal.Zipper α β
-- Init.Data.Vector.Range
Vector.zipIdx_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {k : ℕ},
  (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + n)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cone F.rightOp),
  (CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- If the `eLpNorm` of a collection of `AEStronglyMeasurable` functions that converges in measure
is bounded by some constant `C`, then the `eLpNorm` of its limit is also bounded by `C`.  -/
MeasureTheory.eLpNorm_le_of_tendstoInMeasure : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5}
  [inst : SeminormedAddGroup E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E}
  {C p : ENNReal},
  (∀ᶠ (i : ι) in u, MeasureTheory.eLpNorm (f i) p μ ≤ C) →
    MeasureTheory.TendstoInMeasure μ f u g →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.eLpNorm g p μ ≤ C
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.decodeList.match_1.eq_1 : ∀ (v : ℕ) (motive : (x : ℕ × ℕ) → x.2 ≤ v → Sort u_1) (v₁ v₂ : ℕ) (h : (v₁, v₂).2 ≤ v)
  (h_1 : (v₁ v₂ : ℕ) → (h : (v₁, v₂).2 ≤ v) → motive (v₁, v₂) h),
  (match (v₁, v₂), h with
    | (v₁, v₂), h => h_1 v₁ v₂ h) =
    h_1 v₁ v₂ h
-- Init.Data.Int.Linear
Int.Internal.Linear.var_eq_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.var_eq_cert x k p =
    Int.Internal.Linear.Poly.rec (fun x => false)
      (fun k₁ x' p' x_1 =>
        Int.Internal.Linear.Poly.rec (fun k₂ => k₁ != 0 && x == x' && k == -k₂ / k₁) (fun x x_2 x_3 x_4 => false) p')
      p
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : UpperSet α),
  ↑((UpperSet.map f) s) = ⇑f '' ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.unop_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.unop.fst = c.inl.unop
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.getComputedFieldValue : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.coe_smul : ∀ {R : Type u_1} {A : Type u_4} [inst : Monoid R] [inst_1 : AddCommMonoid A] [inst_2 : DistribMulAction R A] (r : R)
  (f : AddMonoid.End A), ⇑(r • f) = r • ⇑f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Any_reverse : ∀ {α : Type u_1} {p : α → Prop} {t : RBTree.RBNode α}, RBTree.RBNode.Any p t.reverse ↔ RBTree.RBNode.Any p t
-- Mathlib.Order.Filter.Basic
Filter.generate_union : ∀ {α : Type u} {s t : Set (Set α)}, Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_eval₂_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : CommSemiring R] {p : Polynomial S} (f : S →+* R) (r : R)
  (s : S), Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f r p
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The equivalence `C ≅ Karoubi C` when `C` is idempotent complete.  -/
CategoryTheory.Idempotents.toKaroubiEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.IsIdempotentComplete C] → C ≌ CategoryTheory.Idempotents.Karoubi C
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.smul_eq_C_mul : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (a : R), a • f = PowerSeries.C a * f
-- Std.Time.Format.Modifier
/-- Localized offset text in full form (e.g., "GMT+08:00")
 -/
Std.Time.OffsetZ.full : Std.Time.OffsetZ
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_right_cancel_iff' : ∀ {m a b c : ℤ}, c ≠ 0 → (a * c ≡ b * c [ZMOD m * c] ↔ a ≡ b [ZMOD m])
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- See `Summable.congr_cofinite` for a version allowing the functions to
disagree on a finite set.  -/
Summable.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β}, Summable f L → (∀ (b : β), f b = g b) → Summable g L
-- Init.Data.Stream
Std.instToStreamArraySubarray : {α : Type u_1} → Std.ToStream (Array α) (Subarray α)
-- Mathlib.CategoryTheory.Action.Monoidal
CategoryTheory.Functor.mapAction_η_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {W : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} W] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.OplaxMonoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η (F.mapAction G)).hom = CategoryTheory.Functor.OplaxMonoidal.η F
-- Std.Sync.Notify
Std.Notify.State.mk : Std.Queue (Std.Notify.Consumer Unit) → Std.Notify.State
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.Icc_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), Finset.Icc f g = (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.openPartialHomeomorphCoe_apply : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [inst_5 : OrderTopology 𝕜]
  [inst_6 : DiscreteTopology ↥(AddSubgroup.zmultiples p)] (a_1 : 𝕜),
  ↑(AddCircle.openPartialHomeomorphCoe p a) a_1 = ↑a_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.del.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19) (fvarId_1 : Lean.FVarId)
  (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19),
  (Lean.Compiler.LCNF.Code.del fvarId k h = Lean.Compiler.LCNF.Code.del fvarId_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ k = k_1)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)], DFinsupp.support 0 = ∅
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.mk : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsIdempotentElem P → (∀ (x : X), ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖) → IsLprojection X P
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
integral_comp_polarCoord_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ × ℝ → E),
  ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerRight_comp_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {W X Y Z : CategoryTheory.Mon C} {M M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y) (P : Bimod Y Z),
  Bimod.whiskerRight f (N.tensorBimod P) =
    CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).inv
      (CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight (Bimod.whiskerRight f N) P) (M'.associatorBimod N P).hom)
-- Mathlib.Order.Irreducible
SupIrred.not_isMin : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupIrred a → ¬IsMin a
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- The axis aligned parallelepiped over `ι → ℝ` is a cuboid.  -/
parallelepiped_single : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (a : ι → ℝ),
  (parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.natDegree_divX_eq_natDegree_tsub_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.divX.natDegree = p.natDegree - 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_isOpenImmersion : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.LocallyRingedSpace)
  (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion
    (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_iUnion : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (a : α) (s : ι → Set β), a • ⋃ i, s i = ⋃ i, a • s i
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.refl : ∀ {α : Type u} (R : α → α → Prop) [Std.Refl R], Std.Refl (Computation.LiftRel R)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_zero : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R}, SemimoduleCat.Hom.hom 0 = 0
-- Init.Data.List.Attach
List.unattach_filter : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
  {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x}, (List.filter f l).unattach = List.filter g l.unattach
-- Mathlib.CategoryTheory.Limits.Connected
/-- The functor `(X × -)` preserves any connected limit.
Note that this functor does not preserve the two most obvious disconnected limits - that is,
`(X × -)` does not preserve products or terminal object, e.g. `(X ⨯ A) ⨯ (X ⨯ B)` is not isomorphic
to `X ⨯ (A ⨯ B)` and `X ⨯ 1` is not isomorphic to `1`.
 -/
CategoryTheory.prod_preservesConnectedLimits : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type v₂} [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.IsConnected J] (X : C),
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Limits.prod.functor.obj X)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.addLeft_add : ∀ {X : Type u_6} [inst : AddSemigroup X] [inst_1 : TopologicalSpace X] [inst_2 : SeparatelyContinuousAdd X] (x y : X),
  ContinuousMap.addLeft (x + y) = (ContinuousMap.addLeft x).comp (ContinuousMap.addLeft y)
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
ofCompactSupport.eq_1 : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] (g : α → γ)
  (hg₁ : Continuous g) (hg₂ : HasCompactSupport g),
  ofCompactSupport g hg₁ hg₂ = { toFun := g, continuous_toFun := hg₁, map_bounded' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.labelledCopyCount_pos : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W],
  0 < G.labelledCopyCount H ↔ H.IsContained G