ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>f : α →₀ M<GOAL>Finsupp.single a (f a) + Finsupp.erase a f = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>f : α →₀ M<GOAL>Finsupp.erase a f + Finsupp.single a (f a) = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>f f' : α →₀ M<GOAL>Finsupp.erase a (f + f') = Finsupp.erase a f + Finsupp.erase a f'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>f : α →₀ M<GOAL>(Finsupp.eraseAddHom a) f = Finsupp.erase a f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (Finsupp.single a b + f)<GOAL>p f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + Finsupp.single a b)<GOAL>p f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f : α →₀ M<VAR>h0 : p 0<VAR>hadd : ∀ (f g : α →₀ M), p f → p g → p (f + g)<VAR>hsingle : ∀ (a : α) (b : M), p (Finsupp.single a b)<GOAL>p f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<GOAL>AddSubmonoid.closure {f | ∃ a b, f = Finsupp.single a b} = ⊤
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f g : (α →₀ M) →+ N<VAR>H : ∀ (x : α) (y : M), f (Finsupp.single x y) = g (Finsupp.single x y)<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f g : (α →₀ M) →+ N<VAR>H : ∀ (x : α), f.comp (Finsupp.singleAddHom x) = g.comp (Finsupp.singleAddHom x)<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (Finsupp.single x y)) = g (Multiplicative.ofAdd (Finsupp.single x y))<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x y : M), f (x + y) = f x + f y<VAR>v₁ v₂ : α →₀ M<GOAL>Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>FunLike β M N<VAR>AddMonoidHomClass β M N<VAR>f : β<VAR>v₁ v₂ : α →₀ M<GOAL>Finsupp.mapRange ⇑f ⋯ (v₁ + v₂) = Finsupp.mapRange ⇑f ⋯ v₁ + Finsupp.mapRange ⇑f ⋯ v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α ↪ β<VAR>v : α →₀ M<GOAL>(Finsupp.embDomain.addMonoidHom f) v = Finsupp.embDomain f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α ↪ β<VAR>v w : α →₀ M<GOAL>Finsupp.embDomain f (v + w) = Finsupp.embDomain f v + Finsupp.embDomain f w
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>NegZeroClass G<VAR>g : α →₀ G<GOAL>⇑(-g) = -⇑g
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>NegZeroClass G<VAR>g : α →₀ G<VAR>a : α<GOAL>(-g) a = -g a
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>H : Type u_10<VAR>NegZeroClass G<VAR>NegZeroClass H<VAR>f : G → H<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x : G), f (-x) = -f x<VAR>v : α →₀ G<GOAL>Finsupp.mapRange f hf (-v) = -Finsupp.mapRange f hf v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_9<VAR>H : Type u_10<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>FunLike β G H<VAR>AddMonoidHomClass β G H<VAR>f : β<VAR>v : α →₀ G<GOAL>Finsupp.mapRange ⇑f ⋯ (-v) = -Finsupp.mapRange ⇑f ⋯ v
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubNegZeroMonoid G<VAR>g₁ g₂ : α →₀ G<GOAL>⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubNegZeroMonoid G<VAR>g₁ g₂ : α →₀ G<VAR>a : α<GOAL>(g₁ - g₂) a = g₁ a - g₂ a
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>H : Type u_10<VAR>SubNegZeroMonoid G<VAR>SubNegZeroMonoid H<VAR>f : G → H<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x y : G), f (x - y) = f x - f y<VAR>v₁ v₂ : α →₀ G<GOAL>Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_9<VAR>H : Type u_10<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>FunLike β G H<VAR>AddMonoidHomClass β G H<VAR>f : β<VAR>v₁ v₂ : α →₀ G<GOAL>Finsupp.mapRange ⇑f ⋯ (v₁ - v₂) = Finsupp.mapRange ⇑f ⋯ v₁ - Finsupp.mapRange ⇑f ⋯ v₂
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>k l m n : α<VAR>u v : M<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>f : α →₀ G<GOAL>(-f).support = f.support
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>DecidableEq α<VAR>AddGroup G<VAR>f g : α →₀ G<GOAL>(f - g).support ⊆ f.support ∪ g.support
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>f : α →₀ G<VAR>a : α<GOAL>Finsupp.erase a f = f - Finsupp.single a (f a)
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>AddGroup G<VAR>f : α →₀ G<VAR>a : α<VAR>b : G<GOAL>f.update a b = f - Finsupp.single a (f a) + Finsupp.single a b
<GOAL>|Real.exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10
<GOAL>|Real.exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20
<GOAL>|Real.log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
<VAR>z : ℂ<GOAL>√(Complex.normSq z) * √(Complex.normSq z) = Complex.normSq z
<VAR>z : ℂ<GOAL>0 ≤ √(Complex.normSq z)
<VAR>z : ℂ<GOAL>√(Complex.normSq ((starRingEnd ℂ) z)) = √(Complex.normSq z)
<VAR>z : ℂ<GOAL>|z.re| ≤ √(Complex.normSq z)
<VAR>z : ℂ<GOAL>z.re ≤ √(Complex.normSq z)
<VAR>z w : ℂ<GOAL>√(Complex.normSq (z * w)) = √(Complex.normSq z) * √(Complex.normSq w)
<VAR>z w : ℂ<GOAL>√(Complex.normSq (z + w)) ≤ √(Complex.normSq z) + √(Complex.normSq w)
<GOAL>⇑Complex.abs = fun z => √(Complex.normSq z)
<VAR>z : ℂ<GOAL>Complex.abs z = √(Complex.normSq z)
<VAR>r : ℝ<GOAL>Complex.abs ↑r = |r|
<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>Complex.abs ↑r = r
<VAR>n : ℕ<GOAL>Complex.abs ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Complex.abs (OfNat.ofNat n) = OfNat.ofNat n
<VAR>z : ℂ<GOAL>Complex.abs z * Complex.abs z = Complex.normSq z
<VAR>z : ℂ<GOAL>Complex.abs z ^ 2 = Complex.normSq z
<VAR>z : ℂ<GOAL>Complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2
<VAR>z : ℂ<GOAL>Complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2
<VAR>x y : ℝ<GOAL>Complex.abs (↑x + ↑y * Complex.I) = √(x ^ 2 + y ^ 2)
<VAR>z : ℂ<GOAL>Complex.abs z = √(z.re ^ 2 + z.im ^ 2)
<GOAL>Set.range ⇑Complex.abs = Set.Ici 0
<VAR>z : ℂ<GOAL>Complex.abs ((starRingEnd ℂ) z) = Complex.abs z
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℂ<GOAL>Complex.abs (s.prod f) = ∏ I ∈ s, Complex.abs (f I)
<VAR>z : ℂ<VAR>n : ℕ<GOAL>Complex.abs (z ^ n) = Complex.abs z ^ n
<VAR>z : ℂ<VAR>n : ℤ<GOAL>Complex.abs (z ^ n) = Complex.abs z ^ n
<VAR>z : ℂ<GOAL>|z.re| ≤ Complex.abs z
<VAR>z : ℂ<GOAL>|z.im| ≤ Complex.abs z
<VAR>z : ℂ<GOAL>z.re ≤ Complex.abs z
<VAR>z : ℂ<GOAL>z.im ≤ Complex.abs z
<VAR>z : ℂ<GOAL>|z.re| < Complex.abs z ↔ z.im ≠ 0
<VAR>z : ℂ<GOAL>|z.im| < Complex.abs z ↔ z.re ≠ 0
<VAR>z : ℂ<GOAL>|z.re| = Complex.abs z ↔ z.im = 0
<VAR>z : ℂ<GOAL>|z.im| = Complex.abs z ↔ z.re = 0
<VAR>z : ℂ<GOAL>|Complex.abs z| = Complex.abs z
<VAR>z : ℂ<GOAL>Complex.abs z ≤ |z.re| + |z.im|
<VAR>z : ℂ<GOAL>Complex.abs z ≤ √2 * max |z.re| |z.im|
<VAR>z : ℂ<GOAL>|z.re / Complex.abs z| ≤ 1
<VAR>z : ℂ<GOAL>|z.im / Complex.abs z| ≤ 1
<VAR>n : ℤ<GOAL>Complex.abs ↑n = |↑n|
<VAR>n : ℤ<GOAL>|↑n| = Complex.abs ↑n
<VAR>x : ℂ<GOAL>Complex.normSq x = Complex.abs x ^ 2
<GOAL>Set.range ⇑Complex.normSq = Set.Ici 0
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>IsCauSeq abs fun n => (↑f n).re
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>IsCauSeq abs fun n => (↑f n).im
<VAR>f : ℕ → ℂ<VAR>hf : IsCauSeq (⇑Complex.abs) f<GOAL>IsCauSeq abs (⇑Complex.abs ∘ f)
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>f ≈ CauSeq.const (⇑Complex.abs) (Complex.limAux f)
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>f.lim = ↑(Complex.cauSeqRe f).lim + ↑(Complex.cauSeqIm f).lim * Complex.I
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>(Complex.cauSeqRe f).lim = f.lim.re
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>(Complex.cauSeqIm f).lim = f.lim.im
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>IsCauSeq ⇑Complex.abs fun n => (starRingEnd ℂ) (↑f n)
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>(Complex.cauSeqConj f).lim = (starRingEnd ℂ) f.lim
<VAR>f : CauSeq ℂ ⇑Complex.abs<GOAL>(Complex.cauSeqAbs f).lim = Complex.abs f.lim
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>s ≠ 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>(-s).re ≠ 0
<VAR>z : ℂ<GOAL>Complex.equivRealProd z = (z.re, z.im)
<VAR>z : ℂ<GOAL>{ re := z.re, im := z.im } = z
<VAR>z w : ℂ<GOAL>z.re = w.re → z.im = w.im → z = w
<VAR>z w : ℂ<GOAL>z = w ↔ z.re = w.re ∧ z.im = w.im
<VAR>r : ℝ<GOAL>(↑r).re = r
<VAR>r : ℝ<GOAL>(↑r).im = 0
<VAR>r : ℝ<GOAL>↑r = { re := r, im := 0 }
<VAR>z w : ℝ<GOAL>↑z = ↑w ↔ z = w
<VAR>z : ℂ<VAR>s t : Set ℝ<GOAL>z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t
<VAR>z : ℝ<GOAL>↑z = 0 ↔ z = 0
<VAR>z : ℝ<GOAL>↑z ≠ 0 ↔ z ≠ 0
<VAR>z : ℝ<GOAL>↑z = 1 ↔ z = 1
<VAR>z : ℝ<GOAL>↑z ≠ 1 ↔ z ≠ 1
<VAR>z w : ℂ<GOAL>(z + w).re = z.re + w.re
<VAR>z w : ℂ<GOAL>(z + w).im = z.im + w.im
<VAR>r s : ℝ<GOAL>↑(r + s) = ↑r + ↑s
<VAR>z : ℂ<GOAL>(-z).re = -z.re
<VAR>z : ℂ<GOAL>(-z).im = -z.im
<VAR>r : ℝ<GOAL>↑(-r) = -↑r
<VAR>z w : ℂ<GOAL>(z * w).re = z.re * w.re - z.im * w.im
<VAR>z w : ℂ<GOAL>(z * w).im = z.re * w.im + z.im * w.re
<VAR>r s : ℝ<GOAL>↑(r * s) = ↑r * ↑s
<VAR>r : ℝ<VAR>z : ℂ<GOAL>(↑r * z).re = r * z.re
<VAR>r : ℝ<VAR>z : ℂ<GOAL>(↑r * z).im = r * z.im
<VAR>z : ℂ<VAR>r : ℝ<GOAL>(z * ↑r).re = z.re * r
<VAR>z : ℂ<VAR>r : ℝ<GOAL>(z * ↑r).im = z.im * r
<VAR>r : ℝ<VAR>z : ℂ<GOAL>↑r * z = { re := r * z.re, im := r * z.im }
<VAR>z : ℂ<GOAL>Complex.I * z = { re := -z.im, im := z.re }
<VAR>a b : ℝ<GOAL>{ re := a, im := b } = ↑a + ↑b * Complex.I
<VAR>z : ℂ<GOAL>↑z.re + ↑z.im * Complex.I = z
<VAR>z : ℂ<GOAL>(z * Complex.I).re = -z.im
<VAR>z : ℂ<GOAL>(z * Complex.I).im = z.re
<VAR>z : ℂ<GOAL>(Complex.I * z).re = -z.im
<VAR>z : ℂ<GOAL>(Complex.I * z).im = z.re
<VAR>p : ℝ × ℝ<GOAL>Complex.equivRealProd.symm p = ↑p.1 + ↑p.2 * Complex.I
<VAR>p : ℝ × ℝ<GOAL>(Complex.equivRealProdAddHom.symm p).re = p.1
<VAR>z : ℂ<GOAL>Complex.equivRealProdAddHom z = (z.re, z.im)
<VAR>p : ℝ × ℝ<GOAL>(Complex.equivRealProdAddHom.symm p).im = p.2
<VAR>p : ℝ × ℝ<GOAL>Complex.equivRealProdAddHom.symm p = ↑p.1 + ↑p.2 * Complex.I
<VAR>R : Type u_1<VAR>SMul R ℝ<VAR>r : R<VAR>z : ℂ<GOAL>(r • z).re = r • z.re
<VAR>R : Type u_1<VAR>SMul R ℝ<VAR>r : R<VAR>z : ℂ<GOAL>(r • z).im = r • z.im
<VAR>x : ℝ<VAR>z : ℂ<GOAL>x • z = ↑x * z
<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>q : ℚ<GOAL>↑↑q = ↑q
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).re = OfNat.ofNat n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).im = 0
<VAR>n : ℕ<GOAL>(↑n).re = ↑n
<VAR>n : ℕ<GOAL>(↑n).im = 0
<VAR>n : ℤ<GOAL>(↑n).re = ↑n
<VAR>n : ℤ<GOAL>(↑n).im = 0
<VAR>q : ℚ≥0<GOAL>(↑q).re = ↑q
<VAR>q : ℚ≥0<GOAL>(↑q).im = 0
<VAR>q : ℚ<GOAL>(↑q).re = ↑q
<VAR>q : ℚ<GOAL>(↑q).im = 0
<VAR>n : ℕ<VAR>r : ℝ<GOAL>↑(n • r) = n • ↑r
<VAR>n : ℤ<VAR>r : ℝ<GOAL>↑(n • r) = n • ↑r
<VAR>z : ℂ<GOAL>((starRingEnd ℂ) z).re = z.re
<VAR>z : ℂ<GOAL>((starRingEnd ℂ) z).im = -z.im
<VAR>r : ℝ<GOAL>(starRingEnd ℂ) ↑r = ↑r
<GOAL>(starRingEnd ℂ) Complex.I = -Complex.I
<VAR>n : ℕ<GOAL>(starRingEnd ℂ) ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(starRingEnd ℂ) (OfNat.ofNat n) = OfNat.ofNat n
<GOAL>(starRingEnd ℂ) (-Complex.I) = Complex.I
<VAR>z : ℂ<GOAL>(starRingEnd ℂ) z = z ↔ ∃ r, z = ↑r
<VAR>z : ℂ<GOAL>(starRingEnd ℂ) z = z ↔ ↑z.re = z
<VAR>z : ℂ<GOAL>(starRingEnd ℂ) z = z ↔ z.im = 0
<VAR>z : ℂ<GOAL>Complex.normSq z = z.re * z.re + z.im * z.im
<VAR>r : ℝ<GOAL>Complex.normSq ↑r = r * r
<VAR>n : ℕ<GOAL>Complex.normSq ↑n = ↑n * ↑n
<VAR>z : ℤ<GOAL>Complex.normSq ↑z = ↑z * ↑z
<VAR>q : ℚ<GOAL>Complex.normSq ↑q = ↑q * ↑q
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Complex.normSq (OfNat.ofNat n) = OfNat.ofNat n * OfNat.ofNat n
<VAR>x y : ℝ<GOAL>Complex.normSq { re := x, im := y } = x * x + y * y
<VAR>x y : ℝ<GOAL>Complex.normSq (↑x + ↑y * Complex.I) = x ^ 2 + y ^ 2
<VAR>z : ℂ<GOAL>↑(Complex.normSq z) = (starRingEnd ℂ) z * z
<VAR>z : ℂ<GOAL>0 ≤ Complex.normSq z
<VAR>z : ℂ<GOAL>Complex.normSq z = 0 ↔ z = 0
<VAR>z : ℂ<GOAL>0 < Complex.normSq z ↔ z ≠ 0
<VAR>z : ℂ<GOAL>Complex.normSq (-z) = Complex.normSq z
<VAR>z : ℂ<GOAL>Complex.normSq ((starRingEnd ℂ) z) = Complex.normSq z
<VAR>z w : ℂ<GOAL>Complex.normSq (z * w) = Complex.normSq z * Complex.normSq w
<VAR>z w : ℂ<GOAL>Complex.normSq (z + w) = Complex.normSq z + Complex.normSq w + 2 * (z * (starRingEnd ℂ) w).re
<VAR>z : ℂ<GOAL>z.re * z.re ≤ Complex.normSq z
<VAR>z : ℂ<GOAL>z.im * z.im ≤ Complex.normSq z
<VAR>z : ℂ<GOAL>z * (starRingEnd ℂ) z = ↑(Complex.normSq z)
<VAR>z : ℂ<GOAL>z + (starRingEnd ℂ) z = ↑(2 * z.re)
<VAR>r : ℝ<GOAL>Complex.ofReal r = ↑r
<VAR>z w : ℂ<GOAL>(z - w).re = z.re - w.re
<VAR>z w : ℂ<GOAL>(z - w).im = z.im - w.im
<VAR>r s : ℝ<GOAL>↑(r - s) = ↑r - ↑s
<VAR>z : ℂ<GOAL>z - (starRingEnd ℂ) z = ↑(2 * z.im) * Complex.I
<VAR>z w : ℂ<GOAL>Complex.normSq (z - w) = Complex.normSq z + Complex.normSq w - 2 * (z * (starRingEnd ℂ) w).re
<VAR>z : ℂ<GOAL>z⁻¹ = (starRingEnd ℂ) z * ↑(Complex.normSq z)⁻¹
<VAR>z : ℂ<GOAL>z⁻¹.re = z.re / Complex.normSq z
<VAR>z : ℂ<GOAL>z⁻¹.im = -z.im / Complex.normSq z
<VAR>r : ℝ<GOAL>↑r⁻¹ = (↑r)⁻¹
<VAR>z w : ℂ<GOAL>(z / w).re = z.re * w.re / Complex.normSq w + z.im * w.im / Complex.normSq w
<VAR>z w : ℂ<GOAL>(z / w).im = z.im * w.re / Complex.normSq w - z.re * w.im / Complex.normSq w
<VAR>x : ℂ<GOAL>(starRingEnd ℂ) x⁻¹ = ((starRingEnd ℂ) x)⁻¹
<VAR>r s : ℝ<GOAL>↑(r / s) = ↑r / ↑s
<VAR>r : ℝ<VAR>n : ℤ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>z : ℂ<GOAL>z / Complex.I = -(z * Complex.I)
<VAR>z : ℂ<GOAL>Complex.normSq z⁻¹ = (Complex.normSq z)⁻¹
<VAR>z w : ℂ<GOAL>Complex.normSq (z / w) = Complex.normSq z / Complex.normSq w
<VAR>z : ℂ<VAR>n : ℕ<GOAL>z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
<VAR>z : ℂ<VAR>n : ℤ<GOAL>z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
<VAR>z : ℂ<VAR>x : ℚ<GOAL>z / ↑x = { re := z.re / ↑x, im := z.im / ↑x }
<VAR>z : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }
<VAR>z : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(z / OfNat.ofNat n).re = z.re / OfNat.ofNat n
<VAR>z : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(z / OfNat.ofNat n).im = z.im / OfNat.ofNat n
<VAR>z : ℂ<GOAL>↑z.im = (z - (starRingEnd ℂ) z) / (2 * Complex.I)
<VAR>α : Type u<VAR>l : List (Computation α)<VAR>S : Stream'.WSeq (Computation α)<VAR>c : Computation α<GOAL>c ∈ l → c.Terminates → (Computation.corec Computation.parallel.aux1 (l, S)).Terminates
<VAR>α : Type u<VAR>S : Stream'.WSeq (Computation α)<VAR>c : Computation α<VAR>h : c ∈ S<VAR>T : c.Terminates<GOAL>(Computation.parallel S).Terminates
<VAR>α : Type u<VAR>S : Stream'.WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ Computation.parallel S<GOAL>∃ c, c ∈ S ∧ a ∈ c
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : Stream'.WSeq (Computation α)<GOAL>Computation.map f (Computation.parallel S) = Computation.parallel (Stream'.WSeq.map (Computation.map f) S)
<VAR>α : Type u<VAR>S : Stream'.WSeq (Computation α)<VAR>h : S.head.Promises none<GOAL>Computation.parallel S = Computation.empty α
<VAR>α : Type u<VAR>S : Stream'.WSeq (Computation α)<VAR>a : α<VAR>H : ∀ (s : Computation α), s ∈ S → s.Promises a<GOAL>(Computation.parallel S).Promises a
<VAR>α : Type u<VAR>S : Stream'.WSeq (Computation α)<VAR>a : α<VAR>H : ∀ (s : Computation α), s ∈ S → s.Promises a<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>ac : a ∈ c<GOAL>a ∈ Computation.parallel S
<VAR>α : Type u<VAR>S T : Stream'.WSeq (Computation α)<VAR>a : α<VAR>H : Stream'.WSeq.LiftRel Computation.Equiv S T<GOAL>(∀ (s : Computation α), s ∈ S → s.Promises a) ↔ ∀ (t : Computation α), t ∈ T → t.Promises a
<VAR>α : Type u<VAR>S T : Stream'.WSeq (Computation α)<VAR>a : α<VAR>h1 : ∀ (s : Computation α), s ∈ S → s.Promises a<VAR>H : Stream'.WSeq.LiftRel Computation.Equiv S T<GOAL>(Computation.parallel S).Equiv (Computation.parallel T)
<VAR>α : Type u<VAR>S T : Stream'.WSeq (Computation α)<VAR>a : α<VAR>h2 : ∀ (t : Computation α), t ∈ T → t.Promises a<VAR>H : Stream'.WSeq.LiftRel Computation.Equiv S T<GOAL>(Computation.parallel S).Equiv (Computation.parallel T)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>m : M<VAR>f : α →₀ M<GOAL>(a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>c : α × M<VAR>f : α →₀ M<GOAL>c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>ha : a ∈ f.support<GOAL>(a, f a) ∈ f.graph
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>m : M<VAR>f : α →₀ M<VAR>h : (a, m) ∈ f.graph<GOAL>f a = m
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>f : α →₀ M<GOAL>(a, 0) ∉ f.graph
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>f : α →₀ M<GOAL>Finset.image Prod.fst f.graph = f.support
<VAR>α : Type u_13<VAR>M : Type u_14<VAR>Zero M<GOAL>Function.Injective Finsupp.graph
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f g : α →₀ M<GOAL>f.graph = g.graph ↔ f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.graph 0 = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.graph = ∅ ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.equiv f hf hf') g = Finsupp.mapRange (⇑f) hf g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.mapRange.equiv (Equiv.refl M) ⋯ ⋯ = Equiv.refl (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>f₂ : N ≃ P<VAR>hf₂ : f₂ 0 = 0<VAR>hf₂' : f₂.symm 0 = 0<GOAL>Finsupp.mapRange.equiv (f.trans f₂) ⋯ ⋯ = (Finsupp.mapRange.equiv f hf hf').trans (Finsupp.mapRange.equiv f₂ hf₂ hf₂')
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<GOAL>(Finsupp.mapRange.equiv f hf hf').symm = Finsupp.mapRange.equiv f.symm hf' hf
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.zeroHom f) g = Finsupp.mapRange ⇑f ⋯ g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.mapRange.zeroHom (ZeroHom.id M) = ZeroHom.id (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : ZeroHom N P<VAR>f₂ : ZeroHom M N<GOAL>Finsupp.mapRange.zeroHom (f.comp f₂) = (Finsupp.mapRange.zeroHom f).comp (Finsupp.mapRange.zeroHom f₂)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.addMonoidHom f) g = Finsupp.mapRange ⇑f ⋯ g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<GOAL>Finsupp.mapRange.addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>f : N →+ P<VAR>f₂ : M →+ N<GOAL>Finsupp.mapRange.addMonoidHom (f.comp f₂) = (Finsupp.mapRange.addMonoidHom f).comp (Finsupp.mapRange.addMonoidHom f₂)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M →+ N<GOAL>↑(Finsupp.mapRange.addMonoidHom f) = Finsupp.mapRange.zeroHom ↑f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>F : Type u_13<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>m : Multiset (α →₀ M)<GOAL>Finsupp.mapRange ⇑f ⋯ m.sum = (Multiset.map (fun x => Finsupp.mapRange ⇑f ⋯ x) m).sum
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>F : Type u_13<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>s : Finset ι<VAR>g : ι → α →₀ M<GOAL>Finsupp.mapRange ⇑f ⋯ (∑ x ∈ s, g x) = ∑ x ∈ s, Finsupp.mapRange ⇑f ⋯ (g x)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M ≃+ N<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.addEquiv f) g = Finsupp.mapRange ⇑f ⋯ g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<GOAL>Finsupp.mapRange.addEquiv (AddEquiv.refl M) = AddEquiv.refl (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>f : M ≃+ N<VAR>f₂ : N ≃+ P<GOAL>Finsupp.mapRange.addEquiv (f.trans f₂) = (Finsupp.mapRange.addEquiv f).trans (Finsupp.mapRange.addEquiv f₂)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M ≃+ N<GOAL>(Finsupp.mapRange.addEquiv f).symm = Finsupp.mapRange.addEquiv f.symm
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M ≃+ N<GOAL>↑(Finsupp.mapRange.addEquiv f) = Finsupp.mapRange.addMonoidHom f.toAddMonoidHom
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M ≃+ N<GOAL>↑(Finsupp.mapRange.addEquiv f) = Finsupp.mapRange.equiv ↑f ⋯ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>l : α →₀ M<VAR>b : β<GOAL>(Finsupp.equivMapDomain f l) b = l (f.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>l : β →₀ M<VAR>a : α<GOAL>(Finsupp.equivMapDomain f.symm l) a = l (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>l : α →₀ M<GOAL>Finsupp.equivMapDomain (Equiv.refl α) l = l
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.equivMapDomain (Equiv.refl α) = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>g : β ≃ γ<VAR>l : α →₀ M<GOAL>Finsupp.equivMapDomain (f.trans g) l = Finsupp.equivMapDomain g (Finsupp.equivMapDomain f l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>g : β ≃ γ<GOAL>Finsupp.equivMapDomain (f.trans g) = Finsupp.equivMapDomain g ∘ Finsupp.equivMapDomain f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>a : α<VAR>b : M<GOAL>Finsupp.equivMapDomain f (Finsupp.single a b) = Finsupp.single (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<GOAL>Finsupp.equivMapDomain f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α ≃ β<VAR>l : α →₀ M<VAR>g : β → M → N<GOAL>(Finsupp.equivMapDomain f l).sum g = l.sum fun a m => g (f a) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>CommMonoid N<VAR>f : α ≃ β<VAR>l : α →₀ M<VAR>g : β → M → N<GOAL>(Finsupp.equivMapDomain f l).prod g = l.prod fun a m => g (f a) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<VAR>l : α →₀ M<GOAL>(Finsupp.equivCongrLeft f) l = Finsupp.equivMapDomain f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ≃ β<GOAL>(Finsupp.equivCongrLeft f).symm = Finsupp.equivCongrLeft f.symm
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>CommSemiring R<VAR>g : α → M → ℕ<GOAL>↑(f.prod g) = f.prod fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>CommSemiring R<VAR>g : α → M → ℕ<GOAL>↑(f.sum g) = f.sum fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>CommRing R<VAR>g : α → M → ℤ<GOAL>↑(f.prod g) = f.prod fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>CommRing R<VAR>g : α → M → ℤ<GOAL>↑(f.sum g) = f.sum fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>DivisionRing R<VAR>CharZero R<VAR>g : α → M → ℚ<GOAL>↑(f.sum g) = f.sum fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>R : Type u_11<VAR>Zero M<VAR>f : α →₀ M<VAR>Field R<VAR>CharZero R<VAR>g : α → M → ℚ<GOAL>↑(f.prod g) = f.prod fun a b => ↑(g a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x : α →₀ M<VAR>a : α<GOAL>(Finsupp.mapDomain f x) (f a) = x a