ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℝ × ℝ<GOAL>Complex.equivRealProdLm.symm p = ↑p.1 + ↑p.2 * Complex.I
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℝ A<VAR>I' : A<VAR>hI' : I' * I' = -1<VAR>z : ℂ<GOAL>(Complex.liftAux I' hI') z = (algebraMap ℝ A) z.re + z.im • I'
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℝ A<VAR>I' : A<VAR>hI' : I' * I' = -1<GOAL>(Complex.liftAux I' hI') Complex.I = I'
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℝ A<VAR>F : ℂ →ₐ[ℝ] A<GOAL>↑(Complex.lift.symm F) = F Complex.I
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℝ A<VAR>I' : { I' // I' * I' = -1 }<GOAL>Complex.lift I' = Complex.liftAux ↑I' ⋯
<GOAL>Complex.liftAux Complex.I Complex.I_mul_I = AlgHom.id ℝ ℂ
<GOAL>Complex.liftAux (-Complex.I) ⋯ = ↑Complex.conjAe
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : ↥(skewAdjoint A)<GOAL>↑(skewAdjoint.negISMul a) = -Complex.I • ↑a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : ↥(skewAdjoint A)<GOAL>Complex.I • ↑(skewAdjoint.negISMul a) = ↑a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : A<GOAL>↑(realPart a) = 2⁻¹ • (a + star a)
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : A<GOAL>↑(imaginaryPart a) = -Complex.I • 2⁻¹ • (a - star a)
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : A<GOAL>↑(realPart a) + Complex.I • ↑(imaginaryPart a) = a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : A<GOAL>realPart (Complex.I • a) = -imaginaryPart a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>a : A<GOAL>imaginaryPart (Complex.I • a) = realPart a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>z : ℂ<VAR>a : A<GOAL>realPart (z • a) = z.re • realPart a - z.im • imaginaryPart a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>z : ℂ<VAR>a : A<GOAL>imaginaryPart (z • a) = z.re • imaginaryPart a + z.im • realPart a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>↑((skewAdjointPart ℝ) x) = Complex.I • ↑(imaginaryPart x)
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>↑(imaginaryPart x) = -Complex.I • ↑((skewAdjointPart ℝ) x)
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>↑(realPart x) = x
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>imaginaryPart x = 0
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<GOAL>realPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = LinearMap.id
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<GOAL>imaginaryPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>imaginaryPart ↑(realPart x) = 0
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>imaginaryPart ↑(imaginaryPart x) = 0
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>realPart ↑(realPart x) = realPart x
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<VAR>x : A<GOAL>realPart ↑(imaginaryPart x) = imaginaryPart x
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<GOAL>Function.Surjective ⇑realPart
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<GOAL>Function.Surjective ⇑imaginaryPart
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℂ A<VAR>StarAddMonoid A<VAR>StarModule ℂ A<GOAL>Submodule.span ℂ ↑(selfAdjoint A) = ⊤
<VAR>z : ↥(selfAdjoint ℂ)<GOAL>Complex.selfAdjointEquiv z = (↑z).re
<VAR>x : ℝ<GOAL>Complex.selfAdjointEquiv.symm x = ⟨↑x, ⋯⟩
<VAR>z : ↥(selfAdjoint ℂ)<GOAL>↑(Complex.selfAdjointEquiv z) = ↑z
<VAR>r : ℝ<GOAL>↑(realPart ↑r) = ↑r
<VAR>r : ℝ<GOAL>imaginaryPart ↑r = 0
<VAR>z : ℂ<GOAL>↑(realPart z) = ↑z.re
<VAR>A : Type u_2<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℂ A<VAR>IsScalarTower ℂ A A<VAR>SMulCommClass ℂ A A<VAR>StarModule ℂ A<VAR>a : A<GOAL>star a * a + a * star a = 2 • (↑(realPart a) * ↑(realPart a) + ↑(imaginaryPart a) * ↑(imaginaryPart a))
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>f : Π₀ (i : ι), β i<GOAL>f.toFun = ⇑f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>f g : Π₀ (i : ι), β i<VAR>h : ∀ (i : ι), f i = g i<GOAL>f = g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>f g : Π₀ (i : ι), β i<GOAL>f ≠ g ↔ ∃ i, f i ≠ g i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>f : (i : ι) → β i<VAR>s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<GOAL>⇑{ toFun := f, support' := s } = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<GOAL>⇑0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>i : ι<GOAL>0 i = 0
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>i : ι<GOAL>(DFinsupp.mapRange f hf g) i = f i (g i)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>(i : ι) → Zero (β₁ i)<VAR>h : ∀ (i : ι), id 0 = 0 := ⋯<VAR>g : Π₀ (i : ι), β₁ i<GOAL>DFinsupp.mapRange (fun i => id) h g = g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>f₂ : (i : ι) → β i → β₁ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>hf₂ : ∀ (i : ι), f₂ i 0 = 0<VAR>h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0<VAR>g : Π₀ (i : ι), β i<GOAL>DFinsupp.mapRange (fun i => f i ∘ f₂ i) h g = DFinsupp.mapRange f hf (DFinsupp.mapRange f₂ hf₂ g)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<GOAL>DFinsupp.mapRange f hf 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>g₁ : Π₀ (i : ι), β₁ i<VAR>g₂ : Π₀ (i : ι), β₂ i<VAR>i : ι<GOAL>(DFinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>x y : Π₀ (i : ι), β i<VAR>s : Set ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>i : ι<GOAL>(x.piecewise y s) i = if i ∈ s then x i else y i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>x y : Π₀ (i : ι), β i<VAR>s : Set ι<VAR>(i : ι) → Decidable (i ∈ s)<GOAL>⇑(x.piecewise y s) = s.piecewise ⇑x ⇑y
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>g₁ g₂ : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(g₁ + g₂) i = g₁ i + g₂ i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>g₁ g₂ : Π₀ (i : ι), β i<GOAL>⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddMonoid (β i)<VAR>b : ℕ<VAR>v : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(b • v) i = b • v i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddMonoid (β i)<VAR>b : ℕ<VAR>v : Π₀ (i : ι), β i<GOAL>⇑(b • v) = b • ⇑v
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>α : Type u_1<VAR>(i : ι) → AddCommMonoid (β i)<VAR>s : Finset α<VAR>g : α → Π₀ (i : ι), β i<GOAL>⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>α : Type u_1<VAR>(i : ι) → AddCommMonoid (β i)<VAR>s : Finset α<VAR>g : α → Π₀ (i : ι), β i<VAR>i : ι<GOAL>(∑ a ∈ s, g a) i = ∑ a ∈ s, (g a) i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>g : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(-g) i = -g i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>g : Π₀ (i : ι), β i<GOAL>⇑(-g) = -⇑g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>g₁ g₂ : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(g₁ - g₂) i = g₁ i - g₂ i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>g₁ g₂ : Π₀ (i : ι), β i<GOAL>⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>b : ℤ<VAR>v : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(b • v) i = b • v i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>b : ℤ<VAR>v : Π₀ (i : ι), β i<GOAL>⇑(b • v) = b • ⇑v
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>b : γ<VAR>v : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(b • v) i = b • v i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>b : γ<VAR>v : Π₀ (i : ι), β i<GOAL>⇑(b • v) = b • ⇑v
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.filter p f) i = if p i then f i else 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>h : p i<GOAL>(DFinsupp.filter p f) i = f i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>h : ¬p i<GOAL>(DFinsupp.filter p f) i = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>DFinsupp.filter p f + DFinsupp.filter (fun i => ¬p i) f = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>DFinsupp.filter p 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : Π₀ (i : ι), β i<GOAL>DFinsupp.filter p (f + g) = DFinsupp.filter p f + DFinsupp.filter p g
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.filter p (r • f) = r • DFinsupp.filter p f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>x : Π₀ (i : ι), β i<GOAL>(DFinsupp.filterAddMonoidHom β p) x = DFinsupp.filter p x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Semiring γ<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → Module γ (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>x : Π₀ (i : ι), β i<GOAL>(DFinsupp.filterLinearMap γ β p) x = DFinsupp.filter p x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.filter p (-f) = -DFinsupp.filter p f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : Π₀ (i : ι), β i<GOAL>DFinsupp.filter p (f - g) = DFinsupp.filter p f - DFinsupp.filter p g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>DFinsupp.subtypeDomain p 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>i : Subtype p<VAR>v : Π₀ (i : ι), β i<GOAL>(DFinsupp.subtypeDomain p v) i = v ↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>v v' : Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p (v + v') = DFinsupp.subtypeDomain p v + DFinsupp.subtypeDomain p v'
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p (r • f) = r • DFinsupp.subtypeDomain p f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>x : Π₀ (i : ι), β i<GOAL>(DFinsupp.subtypeDomainAddMonoidHom β p) x = DFinsupp.subtypeDomain p x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>Semiring γ<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → Module γ (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>x : Π₀ (i : ι), β i<GOAL>(DFinsupp.subtypeDomainLinearMap γ β p) x = DFinsupp.subtypeDomain p x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>v : Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p (-v) = -DFinsupp.subtypeDomain p v
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>v v' : Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p (v - v') = DFinsupp.subtypeDomain p v - DFinsupp.subtypeDomain p v'
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>f : Π₀ (i : ι), β i<GOAL>{i | f i ≠ 0}.Finite
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(DFinsupp.mk s x) i = if H : i ∈ s then x ⟨i, H⟩ else 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(DFinsupp.mk s x) i = x ⟨i, hi⟩
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<VAR>hi : i ∉ s<GOAL>(DFinsupp.mk s x) i = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>s : Finset ι<GOAL>Function.Injective (DFinsupp.mk s)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>Fintype ι<GOAL>∀ (a : Π₀ (i : ι), β i) (a_1 : ι), DFinsupp.equivFunOnFintype a a_1 = a a_1
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>(i : ι) → Zero (β i)<VAR>Fintype ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.equivFunOnFintype.symm ⇑f = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>b : β i<GOAL>⇑(DFinsupp.single i b) = Pi.single i b
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i i' : ι<VAR>b : β i<GOAL>(DFinsupp.single i b) i' = if h : i = i' then Eq.recOn h b else 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<GOAL>DFinsupp.single i 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>b : β i<GOAL>(DFinsupp.single i b) i = b
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i i' : ι<VAR>b : β i<VAR>h : i ≠ i'<GOAL>(DFinsupp.single i b) i' = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<GOAL>Function.Injective (DFinsupp.single i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i j : ι<VAR>xi : β i<VAR>xj : β j<GOAL>DFinsupp.single i xi = DFinsupp.single j xj ↔ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>b : (i : ι) → β i<VAR>h : ∀ (i : ι), b i ≠ 0<GOAL>Function.Injective fun i => DFinsupp.single i (b i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>xi : β i<GOAL>DFinsupp.single i xi = 0 ↔ xi = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>i : ι<VAR>x : β i<GOAL>DFinsupp.filter p (DFinsupp.single i x) = if p i then DFinsupp.single i x else 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>h : p i<GOAL>DFinsupp.filter p (DFinsupp.single i x) = DFinsupp.single i x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>h : ¬p i<GOAL>DFinsupp.filter p (DFinsupp.single i x) = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i j : ι<VAR>xi : β i<VAR>xj : β j<VAR>h : ⟨i, xi⟩ = ⟨j, xj⟩<GOAL>DFinsupp.single i xi = DFinsupp.single j xj
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>Fintype ι<VAR>i : ι<VAR>m : β i<GOAL>DFinsupp.equivFunOnFintype (DFinsupp.single i m) = Pi.single i m
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>Fintype ι<VAR>i : ι<VAR>m : β i<GOAL>DFinsupp.equivFunOnFintype.symm (Pi.single i m) = DFinsupp.single i m
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>i : ι<VAR>b₁ : β₁ i<VAR>b₂ : β₂ i<GOAL>DFinsupp.zipWith f hf (DFinsupp.single i b₁) (DFinsupp.single i b₂) = DFinsupp.single i (f i b₁ b₂)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i j : ι<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.erase i f) j = if j = i then 0 else f j
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.erase i f) i = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i i' : ι<VAR>f : Π₀ (i : ι), β i<VAR>h : i' ≠ i<GOAL>(DFinsupp.erase i f) i' = f i'
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>x : Π₀ (i : ι), β i<VAR>i : ι<VAR>(i' : ι) → Decidable (i' ∈ {i})<GOAL>(DFinsupp.single i (x i)).piecewise (DFinsupp.erase i x) {i} = x
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type u_1<VAR>(i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>DFinsupp.erase i f = f - DFinsupp.single i (f i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<GOAL>DFinsupp.erase i 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>DFinsupp.filter (fun x => x ≠ i) f = DFinsupp.erase i f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>DFinsupp.filter (fun x => i ≠ x) f = DFinsupp.erase i f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>j i : ι<VAR>x : β i<GOAL>DFinsupp.erase j (DFinsupp.single i x) = if i = j then 0 else DFinsupp.single i x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>x : β i<GOAL>DFinsupp.erase i (DFinsupp.single i x) = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i j : ι<VAR>x : β i<VAR>h : i ≠ j<GOAL>DFinsupp.erase j (DFinsupp.single i x) = DFinsupp.single i x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<VAR>b : β i<GOAL>⇑(DFinsupp.update i f b) = Function.update (⇑f) i b
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.update i f (f i) = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.update i f 0 = DFinsupp.erase i f
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>DFinsupp.update i f b = DFinsupp.single i b + DFinsupp.erase i f
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>DFinsupp.update i f b = DFinsupp.erase i f + DFinsupp.single i b
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type u_1<VAR>(i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>DFinsupp.update i f b = f - DFinsupp.single i (f i) + DFinsupp.single i b
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>DFinsupp.single i (b₁ + b₂) = DFinsupp.single i b₁ + DFinsupp.single i b₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f₁ f₂ : Π₀ (i : ι), β i<GOAL>DFinsupp.erase i (f₁ + f₂) = DFinsupp.erase i f₁ + DFinsupp.erase i f₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>b : β i<GOAL>(DFinsupp.singleAddHom β i) b = DFinsupp.single i b
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>x : Π₀ (i : ι), β i<GOAL>(DFinsupp.eraseAddHom β i) x = DFinsupp.erase i x
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>i : ι<VAR>x : β i<GOAL>DFinsupp.single i (-x) = -DFinsupp.single i x
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>i : ι<VAR>x y : β i<GOAL>DFinsupp.single i (x - y) = DFinsupp.single i x - DFinsupp.single i y
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.erase i (-f) = -DFinsupp.erase i f
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>β : ι → Type v<VAR>(i : ι) → AddGroup (β i)<VAR>i : ι<VAR>f g : Π₀ (i : ι), β i<GOAL>DFinsupp.erase i (f - g) = DFinsupp.erase i f - DFinsupp.erase i g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.single i (f i) + DFinsupp.erase i f = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.erase i f + DFinsupp.single i (f i) = f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : (Π₀ (i : ι), β i) → Prop<VAR>f : Π₀ (i : ι), β i<VAR>h0 : p 0<VAR>ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (DFinsupp.single i b + f)<GOAL>p f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>p : (Π₀ (i : ι), β i) → Prop<VAR>f : Π₀ (i : ι), β i<VAR>h0 : p 0<VAR>ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + DFinsupp.single i b)<GOAL>p f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<GOAL>AddSubmonoid.closure (⋃ i, Set.range (DFinsupp.single i)) = ⊤
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>γ : Type w<VAR>AddZeroClass γ<VAR>f g : (Π₀ (i : ι), β i) →+ γ<VAR>H : ∀ (i : ι) (y : β i), f (DFinsupp.single i y) = g (DFinsupp.single i y)<GOAL>f = g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>γ : Type w<VAR>AddZeroClass γ<VAR>f g : (Π₀ (i : ι), β i) →+ γ<VAR>H : ∀ (x : ι), f.comp (DFinsupp.singleAddHom β x) = g.comp (DFinsupp.singleAddHom β x)<GOAL>f = g
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<GOAL>DFinsupp.mk s (x + y) = DFinsupp.mk s x + DFinsupp.mk s y
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>s : Finset ι<GOAL>DFinsupp.mk s 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<GOAL>DFinsupp.mk s (-x) = -DFinsupp.mk s x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<GOAL>DFinsupp.mk s (x - y) = DFinsupp.mk s x - DFinsupp.mk s y
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>s : Finset ι<VAR>c : γ<VAR>x : (i : ↑↑s) → β ↑i<GOAL>DFinsupp.mk s (c • x) = c • DFinsupp.mk s x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>i : ι<VAR>c : γ<VAR>x : β i<GOAL>DFinsupp.single i (c • x) = c • DFinsupp.single i x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<GOAL>(DFinsupp.mk s x).support ⊆ s