mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((sz : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r)) →
            motive t
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ s ≠ ⊤ → μ sᶜ = μ Set.univ - μ s
-- Mathlib.Algebra.BigOperators.Finprod
one_le_finprod' : ∀ {α : Sort u_4} {M : Type u_7} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {f : α → M},
  (∀ (i : α), 1 ≤ f i) → 1 ≤ ∏ᶠ (i : α), f i
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The property of preserving coequalizers expressed in terms of coforks.  -/
CategoryTheory.Limits.isColimitCoforkMapOfIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Y ⟶ Z} →
                (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) →
                  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ h w) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.toImplicit.match_1.splitter : (motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((binderName : Lean.Name) →
        (t : Lean.Expr) →
          (binderName_1 : Lean.Name) →
            (binderType body : Lean.Expr) →
              (binderInfo binderInfo_1 : Lean.BinderInfo) →
                motive
                  (Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo)
                    binderInfo_1)) →
      ((e : Lean.Expr) →
          (∀ (binderName : Lean.Name) (t : Lean.Expr) (binderName_1 : Lean.Name) (binderType body : Lean.Expr)
              (binderInfo binderInfo_1 : Lean.BinderInfo),
              e =
                  Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo)
                    binderInfo_1 →
                False) →
            motive e) →
        motive e
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.nextParamIdx : Lean.MetavarContext.UnivMVarParamResult → ℕ
-- Mathlib.GroupTheory.ArchimedeanDensely
instUniqueOrderAddMonoidIsoIntOrderDual : Unique (ℤ ≃+o ℤᵒᵈ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_perm_of_perm_second : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l1 l2 l : List ((a : α) × β a)},
  l1.Perm l2 →
    Std.Internal.List.DistinctKeys l →
      Std.Internal.List.DistinctKeys l1 → (Std.Internal.List.insertList l l1).Perm (Std.Internal.List.insertList l l2)
-- Mathlib.MeasureTheory.Group.GeometryOfNumbers
/-- **Blichfeldt's Theorem**. If the volume of the set `s` is larger than the covolume of the
countable subgroup `L` of `E`, then there exist two distinct points `x, y ∈ L` such that `(x + s)`
and `(y + s)` are not disjoint.  -/
MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd : ∀ {E : Type u_1} {L : Type u_2} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E}
  [inst_1 : AddGroup L] [Countable L] [inst_3 : AddAction L E] [inst_4 : MeasurableSpace L] [MeasurableVAdd L E]
  [MeasureTheory.VAddInvariantMeasure L E μ],
  MeasureTheory.IsAddFundamentalDomain L F μ →
    MeasureTheory.NullMeasurableSet s μ → μ F < μ s → ∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)
-- Mathlib.Order.Heyting.Basic
le_sdiff_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ b \ a ⊔ a
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_tsum : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) [MeasurableSingletonClass α] (s : Set α),
  p.toMeasure s = ∑' (x : α), s.indicator (⇑p) x
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryGE : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₂ : ι₂} (h : e₂.BoundaryGE i₂),
  ac.Boundary (ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE ac h) i₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.const_cpow : ∀ {α : Type u_1} {l : Filter α} {f : α → ℂ} {a b : ℂ},
  Filter.Tendsto f l (nhds b) → a ≠ 0 ∨ b ≠ 0 → Filter.Tendsto (fun x => a ^ f x) l (nhds (a ^ b))
-- Mathlib.Data.Set.Functor
Set.bind_def : ∀ {α β : Type u} {s : Set α} {f : α → Set β}, s >>= f = ⋃ i ∈ s, f i
-- Std.Internal.UV.UDP
/-- Cancels a receive operation in the form of `recv` or `waitReadable` if there is currently one
pending. This resolves their returned `IO.Promise` to `none`. This function is considered dangerous,
as improper use can cause data loss, and is therefore not exposed to the top-level API.
Note that this function is idempotent and as such can be called multiple times on the same socket
without causing errors, in particular also without a receive running in the first place.
 -/
Std.Internal.UV.UDP.Socket.cancelRecv : Std.Internal.UV.UDP.Socket → IO Unit
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsSplitEpi f],
  CategoryTheory.IsSplitMono f.op
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Algebra.Group.ForwardDiff
/-- The `n`-th forward difference of `x ↦ x^n` is the constant function `n!`.
 -/
fwdDiff_iter_eq_factorial : ∀ {R : Type u_3} [inst : CommRing R] {n : ℕ}, ((fwdDiff 1)^[n] fun r => r ^ n) = ↑n.factorial
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- For any two charts `e`, `e'` around a point `x` in a C¹ manifold, if `e` maps `x` to the
interior of the model space, `e'` does too - in other words, the notion of interior points does not
depend on any choice of charts.

Note that in general, this is actually quite nontrivial; that is why are focusing only on C¹
manifolds here. For merely topological finite-dimensional manifolds the proof involves singular
homology, and for infinite-dimensional topological manifolds I don't even know if this lemma holds.
 -/
ModelWithCorners.mem_interior_range_of_mem_interior_range_of_mem_atlas : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  {e e' : OpenPartialHomeomorph M H} {x : M},
  n ≠ 0 →
    e ∈ atlas H M →
      e' ∈ atlas H M →
        x ∈ e.source →
          x ∈ e'.source →
            ↑(e.extend I) x ∈ interior (e.extend I).target → ↑(e'.extend I) x ∈ interior (e'.extend I).target
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- `Lp.simpleFunc` is a subspace of Lp consisting of equivalence classes of an integrable simple
function.  -/
MeasureTheory.Lp.simpleFunc : {α : Type u_1} →
  (E : Type u_4) →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        (p : ENNReal) → (μ : MeasureTheory.Measure α) → AddSubgroup ↥(MeasureTheory.Lp E p μ)
-- Lean.Meta.IndPredBelow
/-- The motives (fvars)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.motives : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Expr
-- Lean.Meta.AppBuilder
/-- Given `h : a = b`, returns a proof for `a ↔ b`.  -/
Lean.Meta.mkIffOfEq : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Instances.Matrix
Matrix.conjTranspose_tsum : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : StarAddMonoid R] [ContinuousStar R] [T2Space R] {f : X → Matrix m n R},
  (∑'[L] (x : X), f x).conjTranspose = ∑'[L] (x : X), (f x).conjTranspose
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_iff : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhds x] g → (P f s x ↔ P g s x)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.refl_source : ∀ (X : Type u_7) [inst : TopologicalSpace X], (OpenPartialHomeomorph.refl X).source = Set.univ
-- Init.Data.SInt.Lemmas
Int16.toISize_toInt32 : ∀ (n : Int16), n.toInt32.toISize = n.toISize
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_ground : ∀ {α : Type u_1} {E I : Set α}, (Matroid.uniqueBaseOn I E).E = E
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.preserves_map' : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β),
  (fun {α} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} => η.app α
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sInf` function
that returns the greatest lower bound of a nonempty set which is bounded below. Usually this
constructor provides poor definitional equalities.  If other fields are known explicitly, they
should be provided; for example, if `inf` is known explicitly, construct the
`ConditionallyCompleteLattice` instance as
```
instance : ConditionallyCompleteLattice my_T :=
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sSup
  __ := conditionallyCompleteLatticeOfsInf my_T ...
```
 -/
conditionallyCompleteLatticeOfsInf : (α : Type u_5) →
  [H1 : PartialOrder α] →
    [H2 : InfSet α] →
      (∀ (a b : α), BddAbove {a, b}) →
        (∀ (a b : α), BddBelow {a, b}) →
          (∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) → ConditionallyCompleteLattice α
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α), (Stream'.WSeq.cons a s).destruct = Computation.pure (some (a, s))
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.instPreregular : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C], CategoryTheory.Preregular C
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_toInt : ∀ (x : Int64), Int64.ofIntClamp x.toInt = x
-- Mathlib.Order.SupClosed
SupClosed.biSup_mem_of_nonempty : ∀ {α : Type u_3} [inst : CompleteLattice α] {s : Set α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  SupClosed s → t.Finite → t.Nonempty → (∀ i ∈ t, f i ∈ s) → ⨆ i ∈ t, f i ∈ s
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousAt_iff_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {x : α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u
-- Init.Data.ByteArray.Lemmas
ByteArray.set.congr_simp : ∀ (a a_1 : ByteArray) (e_a : a = a_1) (i i_1 : ℕ) (e_i : i = i_1) (a_2 a_3 : UInt8),
  a_2 = a_3 → ∀ (h : i < a.size), a.set i a_2 h = a_1.set i_1 a_3 ⋯
-- Mathlib.Topology.ContinuousOn
continuousOn_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)},
  ContinuousOn Prod.snd s
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn_2.go : {motive_1 : Aesop.Script.StepTree → Sort u} →
  {motive_2 : Array Aesop.Script.StepTree → Sort u} →
    {motive_3 : List Aesop.Script.StepTree → Sort u} →
      (t : List Aesop.Script.StepTree) →
        ((t : Aesop.Script.StepTree) → t.below → motive_1 t) →
          ((t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t) →
            ((t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t) →
              motive_3 t ×' Aesop.Script.StepTree.below_2 t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_boole_nsmul : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) (a : ι),
  ∑ x ∈ s, (if a = x then 1 else 0) • f x = if a ∈ s then f a else 0
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If a module has a finite dimension, all bases are indexed by a finite set.  -/
Module.Basis.finite_index_of_rank_lt_aleph0 : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_1} {s : Set ι} (b : Module.Basis (↑s) R M), Module.rank R M < Cardinal.aleph0 → s.Finite
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_counit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.counit) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Init.Control.MonadAttach
LawfulMonadAttach.mk : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadAttach m]
  [toWeaklyLawfulMonadAttach : WeaklyLawfulMonadAttach m],
  (∀ {α : Type u} {P : α → Prop} {x : m (Subtype P)} {a : α}, MonadAttach.CanReturn (Subtype.val <$> x) a → P a) →
    LawfulMonadAttach m
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.uniformSpace : (p : ENNReal) → {ι : Type u_2} → (β : ι → Type u_4) → [(i : ι) → UniformSpace (β i)] → UniformSpace (PiLp p β)
-- Mathlib.Data.Finite.Defs
Infinite.false : ∀ {α : Sort u_1} [Finite α], Infinite α → False
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.fromRel_prop`. -/
Sym2.fromRel_proj_prop : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r} {a b : α}, s(a, b) ∈ Sym2.fromRel sym ↔ r a b
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_continuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {B : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedCommRing B] [inst_4 : NormedAlgebra 𝕜 B] {σ : Type u_5} (f : E →L[𝕜] σ → B)
  (p : MvPolynomial σ B), AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.eval (f x)) p) Set.univ
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.cons.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} (a : Q(«$α»)) (s' : Q(List «$α»)) (pf : Q(«$s» = «$a» :: «$s'»))
  (a_1 : Q(«$α»)) (s'_1 : Q(List «$α»)) (pf_1 : Q(«$s» = «$a_1» :: «$s'_1»)),
  (Mathlib.Meta.List.ProveNilOrConsResult.cons a s' pf = Mathlib.Meta.List.ProveNilOrConsResult.cons a_1 s'_1 pf_1) =
    (a = a_1 ∧ s' = s'_1 ∧ pf = pf_1)
-- Lean.Server.References
/-- Finds the first range in `self` that contains `pos`.  -/
Lean.Lsp.ModuleRefs.findRange? : Lean.Lsp.ModuleRefs → Lean.Lsp.Position → optParam Bool false → Option Lean.Lsp.Range
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.UnifEigenvalues.val_mk : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞} (h : f.HasUnifEigenvalue μ k), ↑f k ⟨μ, h⟩ = μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Mathlib.Data.Nat.Digits.Lemmas
/-- Any non-zero natural number `m` is greater than
(b+2)^((number of digits in the base (b+2) representation of m) - 1)
 -/
Nat.base_pow_length_digits_le' : ∀ (b m : ℕ), m ≠ 0 → (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_carrier : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α),
  (SubAddAction.ofFixingAddSubgroup M s).carrier = sᶜ
-- Init.Data.Int.Order
Int.mul_sign_self : ∀ (i : ℤ), i * i.sign = ↑i.natAbs
-- Mathlib.Order.Fin.Basic
/-- A function `f` on `Fin (n + 1)` is strictly monotone if and only if `f i < f (i + 1)`
for all `i`.  -/
Fin.strictMono_iff_lt_succ : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  StrictMono f ↔ ∀ (i : Fin n), f i.castSucc < f i.succ
-- Mathlib.GroupTheory.NoncommCoprod
/-- Coproduct of two `MulHom`s with the same codomain with `Commute` assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2`.
(For the commutative case, use `MulHom.coprod`)  -/
MulHom.noncommCoprod : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : Mul M] →
        [inst_1 : Mul N] →
          [inst_2 : Semigroup P] →
            (f : M →ₙ* P) → (g : N →ₙ* P) → (∀ (m : M) (n : N), Commute (f m) (g n)) → M × N →ₙ* P
-- Mathlib.Data.Set.Lattice
Set.iUnion_symmDiff_subset : ∀ {α : Type u_1} {ι : Sort u_5} {s : Set α} [Nonempty ι] {f : ι → Set α}, symmDiff (⋃ n, f n) s ⊆ ⋃ n, symmDiff (f n) s
-- Mathlib.Algebra.Group.Fin.Basic
/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too.  -/
Fin.instAddRightCancelSemigroup : (n : ℕ) → AddRightCancelSemigroup (Fin n)
-- Init.Core
/-- A setoid's equivalence relation is symmetric.  -/
Setoid.symm : ∀ {α : Sort u} [inst : Setoid α] {a b : α}, a ≈ b → b ≈ a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.neg with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_8 a
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
/-- **Alias** of the reverse direction of `AddSubgroup.zmultiples_le`. -/
AddSubgroup.zmultiples_le_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {H : AddSubgroup G}, g ∈ H → AddSubgroup.zmultiples g ≤ H
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `S` is the localization of `R` at `r`, this is the canonical submersive presentation
of `S` as `R`-algebra.  -/
Algebra.PreSubmersivePresentation.localizationAway : {R : Type u} →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (r : R) → [IsLocalization.Away r S] → Algebra.PreSubmersivePresentation R S Unit Unit
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for `tensorIso`, the tensor product of isomorphisms  -/
CategoryTheory.MonoidalCategory.«term_⊗ᵢ_» : Lean.TrailingParserDescr
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (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.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHomMonomial_single : ∀ {σ : Type u_1} {R : Type u_3} {n k : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] {i : Fin n} {r : R},
  MvPolynomial.esymmAlgHomMonomial σ (fun₀ | i => k) r = MvPolynomial.C r * MvPolynomial.esymm σ R (↑i + 1) ^ k
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_symm_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : M), (AddEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coneOfIsSplitMono_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitMono f],
  (CategoryTheory.Limits.coneOfIsSplitMono f).ι = f
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- If `g : ι → G × G` converges to the uniformity, then any `f : ι → G × G` converges to the
uniformity iff `f * g` does. This is often useful when `g` is valued in the diagonal,
in which case its convergence is automatic.  -/
Filter.Tendsto.uniformity_mul_iff_left : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto g l (uniformity α) → (Filter.Tendsto (f * g) l (uniformity α) ↔ Filter.Tendsto f l (uniformity α))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.ext_iff : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  {c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x}, c1 = c2 ↔ c1.deg = c2.deg ∧ ↑c1.num = ↑c2.num ∧ ↑c1.den = ↑c2.den
-- Mathlib.Algebra.Regular.Basic
/-- An element `a` is right-regular if and only if a positive power of `a` is right-regular.  -/
IsRightRegular.pow_iff : ∀ {R : Type u_1} [inst : Monoid R] {a : R} {n : ℕ}, 0 < n → (IsRightRegular (a ^ n) ↔ IsRightRegular a)
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Ioo : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot],
      l₁ ≤ Filter.principal s →
        l₂ ≤ Filter.principal s →
          ∀ {f : X → α},
            ContinuousOn f s →
              ∀ {v₁ v₂ : α}, Filter.Tendsto f l₁ (nhds v₁) → Filter.Tendsto f l₂ (nhds v₂) → Set.Ioo v₁ v₂ ⊆ f '' s
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : AddSubmonoid M), s.AddSaturated = ∀ ⦃x y : M⦄, x + y ∈ s → x ∈ s ∧ y ∈ s