mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
/-- Build a map out of the exterior algebra given a collection of alternating maps acting on each
exterior power  -/
ExteriorAlgebra.liftAlternating : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.comp_map : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ)
  (x : F α), MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)
-- Mathlib.Data.Fin.Tuple.Reflection
Matrix.vecEmpty.eq_1 : ∀ {α : Type u}, ![] = Fin.elim0
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
          h_1))
-- Mathlib.Data.Nat.Init
Or.by_cases.congr_simp : ∀ {p q : Prop} {inst : Decidable p} [inst_1 : Decidable p] {α : Sort u} (h : p ∨ q) (h₁ h₁_1 : p → α),
  h₁ = h₁_1 → ∀ (h₂ h₂_1 : q → α), h₂ = h₂_1 → h.by_cases h₁ h₂ = h.by_cases h₁_1 h₂_1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.mk : {C : Type u} → (I : Type w) → (I → C) → CategoryTheory.Limits.FormalCoproduct C
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.PolarizationEquiv.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P P_1 : RootPairing ι R M N)
  (e_P : P = P_1) [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem], P.PolarizationEquiv = P_1.PolarizationEquiv
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_mem_prod : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} {s : Finset ι} {I : ι → Ideal R} {x : ι → R},
  (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparison_map_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Comonad.comparison h).map f).f = L.map f
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mk.congr_simp : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (toIntermediateField toIntermediateField_1 : IntermediateField k K)
  (e_toIntermediateField : toIntermediateField = toIntermediateField_1)
  [finiteDimensional : FiniteDimensional k ↥toIntermediateField] [isGalois : IsGalois k ↥toIntermediateField],
  { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois } =
    { toIntermediateField := toIntermediateField_1, finiteDimensional := ⋯, isGalois := ⋯ }
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrable : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.StronglyMeasurable f →
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (nhds 0)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- Reinterpret a closed submodule as a submodule.  -/
ClosedSubmodule.toSubmodule : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → ClosedSubmodule R M → Submodule R M
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.instSubHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → Sub (S₁ ⟶ S₂)
-- Mathlib.Algebra.GroupWithZero.Associated
associated_one_of_mul_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] {a : M} (b : M), a * b = 1 → Associated a 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F], DifferentiableOn 𝕜 f s → ContinuousOn f s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsLocalRing.primesOverFinset_eq : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_4) [inst_1 : CommRing A] [IsDomain A] [inst_3 : IsLocalRing A]
  [inst_4 : IsDedekindDomain A] [inst_5 : Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R}
  [p.IsMaximal], p ≠ ⊥ → IsDedekindDomain.primesOverFinset p A = {IsLocalRing.maximalIdeal A}
-- Init.Tactics
/-- `mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
It specializes a hypothesis from the stateful context with hypotheses from either the pure
or stateful context or pure terms.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecializeMacro : Lean.ParserDescr
-- Mathlib.Algebra.BrauerGroup.Defs
/-- `BrauerGroup` is the set of all finite-dimensional central simple algebras quotient
by Brauer Equivalence.  -/
BrauerGroup : (K : Type u) → [Field K] → Type (max u (u_1 + 1))
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_mul_left : ∀ {α : Type u_3} [inst : Ring α] {a b : α}, Commute a b → ∀ (m : ℤ), Commute (↑m * a) b
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If for each `x : α`, exactly one of `g • x`, `g : G`, belongs to a measurable set `s`, then `s`
is a fundamental domain for the action of `G` on `α`.  -/
MeasureTheory.IsFundamentalDomain.mk' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.NullMeasurableSet s μ → (∀ (x : α), ∃! g, g • x ∈ s) → MeasureTheory.IsFundamentalDomain G s μ
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.forget₂_monCat_map : ∀ {R S : SemiRingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ SemiRingCat MonCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ SemiRingCat MonCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.ByteArray.toList_toByteArray : ∀ (ba : ByteArray), ba.data.toList.toByteArray = ba
-- Mathlib.FieldTheory.Separable
isSeparable_map_iff : ∀ {F : Type u_1} {L : Type u_2} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K]
  [inst_3 : Ring L] [inst_4 : Algebra F L] {x : K} (f : K →ₐ[F] L),
  Function.Injective ⇑f → (IsSeparable F (f x) ↔ IsSeparable F x)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.coordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
  [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} {g : M → F} {x : M},
  MDiffAt[s] f x →
    MDiffAt[s] g x → f x ∈ e.baseSet → f x ∈ e'.baseSet → (MDiffAt[s] fun y => e.coordChange e' (f y) (g y)) x
-- Mathlib.Data.Int.ModEq
AddCommGroup.modEq_iff_intModEq : ∀ {a b z : ℤ}, a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
-- Mathlib.Order.Hom.Basic
/-- The underlying function of an `OrderHom`.  -/
OrderHom.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → α → β
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.mapₐ_injective_of_injective : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B),
  Function.Injective ⇑f → Function.Injective ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.antilipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : RingHomIsometric σ₂₁]
  (e : E ≃SL[σ₁₂] F), AntilipschitzWith ‖↑e.symm‖₊ ⇑e
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- A special case of `f ∘ id = f`, `f` a Localization map.  -/
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N), f.ofAddEquivOfDom ⋯ = f
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
ContDiff.continuous_iteratedDeriv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ), ContDiff 𝕜 (↑m) f → Continuous (iteratedDeriv m f)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.map_f : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (P : StandardEtalePair R) (f : R →+* S),
  (P.map f).f = Polynomial.map f P.f
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_apply : ∀ {ι : Type u_4} {α : Type u_5} {f : ι → α → ENNReal} {x : α}, (∑' (i : ι), f i) x = ∑' (i : ι), f i x
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M),
  Finsupp.optionElim y f = Finsupp.optionEquiv.invFun (y, f)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β) (h : Monotone (↑↑f).toFun), { toAddMonoidHom := ↑f, monotone' := h } = f
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_mem₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.map_ιFree_mapFreeIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I),
  CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) (SheafOfModules.mapFreeIso F I η).inv =
    CategoryTheory.CategoryStruct.comp η.inv (SheafOfModules.ιFree i)
-- Mathlib.Topology.Sets.Compacts
/-- See Note [custom simps projection].  -/
TopologicalSpace.CompactOpens.Simps.coe : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.CompactOpens α → Set α
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The embedding from `down' a` to itself via (· + b).  -/
ComplexShape.embeddingDown'Add : {A : Type u_3} →
  [inst : AddCommSemigroup A] →
    [inst_1 : IsRightCancelAdd A] → (a : A) → A → (ComplexShape.down' a).Embedding (ComplexShape.down' a)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_injective : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜],
  Function.Injective HomogeneousIdeal.toIdeal
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The functional equation for the derivative of the Jacobi theta function, relating
`jacobiTheta₂' z τ` to `jacobiTheta₂' (z / τ) (-1 / τ)`. This is the key lemma behind the proof of
the functional equation for L-series of odd Dirichlet characters.  -/
jacobiTheta₂'_functional_equation : ∀ (z τ : ℂ),
  jacobiTheta₂' z τ =
    1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-↑Real.pi * Complex.I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑Real.pi * Complex.I * z * jacobiTheta₂ (z / τ) (-1 / τ))
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then `norm` and `algebraMap` commutes.
 -/
Subalgebra.LinearDisjoint.norm_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    A ⊔ B = ⊤ →
      ∀ [Module.Free R ↥B] [Module.Finite R ↥B] (x : ↥B),
        (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_three : ∀ {R : Type u_1} [inst : NatCast R], ↑3 = 3
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_neg : ∀ {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (v : V) (x : E),
  LineDeriv.lineDerivOp v (-x) = -LineDeriv.lineDerivOp v x
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.comp_noncommPiCoprod : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} {P : Type u_4}
  [inst_3 : AddMonoid P] {f : M →+ P}
  (hcomm' : optParam (Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)) ⋯),
  f.comp (AddMonoidHom.noncommPiCoprod ϕ hcomm) = AddMonoidHom.noncommPiCoprod (fun i => f.comp (ϕ i)) hcomm'
-- Mathlib.Analysis.Normed.Group.Completeness
/-- In a normed additive group, every absolutely convergent series converges in the
space iff the space is complete.  -/
NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E],
  (∀ (u : ℕ → E),
      (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds a)) ↔
    CompleteSpace E
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKey?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.getKey?ₘ a = Std.DHashMap.Internal.AssocList.getKey? a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a)
-- Init.Data.AC
Lean.Data.AC.Variable.mk.sizeOf_spec : ∀ {α : Sort u} {op : α → α → α} [inst : SizeOf α] (value : α) (neutral : Option (PLift (Std.LawfulIdentity op value))),
  sizeOf { value := value, neutral := neutral } = 1 + sizeOf value + sizeOf neutral
-- Mathlib.Order.GaloisConnection.Basic
WithTop.giUntopDTop.eq_1 : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α],
  WithTop.giUntopDTop = ⋯.mp (GaloisCoinsertion.mk fun o x => WithTop.untopD ⊤ o) ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The support of the valuation on `R`.  -/
ValuativeRel.supp : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Ideal R
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- `(G × H) / (A × B)` is in bijection with `G / A × H / B`.  -/
QuotientAddGroup.prodEquiv : {G : Type u} →
  [inst : AddGroup G] →
    {H : Type v} →
      [inst_1 : AddGroup H] → (A : AddSubgroup G) → (B : AddSubgroup H) → (G × H) ⧸ A.prod B ≃ (G ⧸ A) × H ⧸ B
-- Init.Data.SInt.Lemmas
Int16.toInt_add : ∀ (a b : Int16), (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 16)
-- Mathlib.RingTheory.IsTensorProduct
instIsPushout_1 : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R S R S
-- Init.Data.Int.DivMod.Bootstrap
Int.neg_ediv_of_dvd : ∀ {a b : ℤ}, b ∣ a → -a / b = -(a / b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X)
  (X_1 : Cᵒᵖ) (a : ↑(F.1 X_1)),
  (MonCat.Hom.hom ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X F α).inv.app X_1)) a = α.homEquiv'.symm a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey? k' = some k
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_2 : Nat.Partrec.Code.succ.eval = ↑Nat.succ
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.mk : Lean.Name → Array Lean.InductiveVal → Array Lean.Name → Bool → Lean.Elab.Deriving.Context
-- Init.Data.SInt.Lemmas
Int8.toBitVec_maxValue : Int8.maxValue.toBitVec = BitVec.intMax 8
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.superset : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  {φ ψ : ι → Set α},
  MeasureTheory.AECover μ l φ → (∀ (i : ι), φ i ⊆ ψ i) → (∀ (i : ι), MeasurableSet (ψ i)) → MeasureTheory.AECover μ l ψ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.decide.sizeOf_spec : ∀ (b : Bool), sizeOf (Nat.EqResult.decide✝ b) = 1 + sizeOf b
-- Std.Time.Date.Unit.Month
/-- Converts a `Ordinal` into a `Nat`.
 -/
Std.Time.Month.Ordinal.toNat : Std.Time.Month.Ordinal → ℕ
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.PolarizationEquiv.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem],
  P.PolarizationEquiv = (P.toInvariantForm.form.toDual ⋯).trans P.flip.toPerfPair.symm
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_lt_add_iff_of_left_lt_aleph0 : ∀ {a b c : Cardinal.{u_1}}, c < Cardinal.aleph0 → (c + a < c + b ↔ a < b)
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instReprOffset : Repr Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_le : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, ⌈a⌉ ≤ z ↔ a ≤ ↑z
-- Mathlib.Algebra.CharP.Defs
CharP.charP_to_charZero : ∀ (R : Type u_1) [inst : AddGroupWithOne R] [CharP R 0], CharZero R
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.assert : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.coe_mk : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] (f : R →ₙ* S)
  {h₁ : ∀ (x : R), 0 ≤ f.toFun x} {h₂ : ∀ (x : R), f.toFun x = 0 ↔ x = 0}
  {h₃ : ∀ (x y : R), f.toFun (x + y) ≤ f.toFun x + f.toFun y},
  ⇑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = ⇑f
-- Mathlib.CategoryTheory.Galois.Basic
/-- The fiber of the pullback is the fiber product of the fibers.  -/
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.PreGaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X A B : C} →
            (f : A ⟶ X) →
              (g : B ⟶ X) →
                (F.obj (CategoryTheory.Limits.pullback f g)).obj ≃
                  { p //
                    (CategoryTheory.ConcreteCategory.hom (F.map f)) p.1 =
                      (CategoryTheory.ConcreteCategory.hom (F.map g)) p.2 }
-- Batteries.Tactic.Init
/-- `eapply e` is like `apply e` but it does not add subgoals for variables that appear
in the types of other goals. Note that this can lead to a failure where there are
no goals remaining but there are still metavariables in the term:
```
example (h : ∀ x : Nat, x = x → True) : True := by
  eapply h
  rfl
  -- no goals
-- (kernel) declaration has metavariables '_example'
```
 -/
Batteries.Tactic.tacticEapply_ : Lean.ParserDescr
-- Init.Data.Array.Lemmas
/-- We can prove that two folds over the same array are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the array,
preserves the relation.
 -/
Array.foldr_rel : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ xs, ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) →
      r (Array.foldr (fun a acc => f a acc) a xs) (Array.foldr (fun a acc => g a acc) b xs)