internlm/Lean-Github huggingface dataset:
Theorem: Real.hasTemperateGrowth_l2inner_const
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth fun v => ∑ i : ι, v i * w i
Tactic:
change Function.HasTemperateGrowth ((fun v : EuclideanSpace ℝ ι => inner v w) ∘ ⇑(EuclideanSpace.equiv ι ℝ).symm.toContinuousLinearMap)
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth ((fun v => ⟪v, w⟫_ℝ) ∘ ⇑↑(ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)))
Theorem: Real.hasTemperateGrowth_l2inner_const
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth ((fun v => ⟪v, w⟫_ℝ) ∘ ⇑↑(ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)))
Tactic:
exact (Real.hasTemperateGrowth_inner_const _).comp (Function.hasTemperateGrowth_clm _)
Proof state after:
no goals
Theorem: Continuous.realFourierChar
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (f x)))
Tactic:
simp_rw [Real.fourierChar_apply]
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp (↑(2 * π * f x) * I)
Theorem: Continuous.realFourierChar
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp (↑(2 * π * f x) * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp ((2 * π * f x) • I)
Theorem: Continuous.realFourierChar
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp ((2 * π * f x) • I)
Tactic:
exact ((continuous_const.mul hf).smul continuous_const).cexp
Proof state after:
no goals
Theorem: deriv.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ deriv (fun x => cexp (f x • I)) x = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
rw [deriv_cexp (hf.smul_const I)]
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * deriv (fun y => f y • I) x = ↑(deriv f x) * I * cexp (f x • I)
Theorem: deriv.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * deriv (fun y => f y • I) x = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
rw [deriv_smul hf (differentiableAt_const I)]
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * (f x • deriv (fun x => I) x + deriv f x • I) = ↑(deriv f x) * I * cexp (f x • I)
Theorem: deriv.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * (f x • deriv (fun x => I) x + deriv f x • I) = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
simp
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (↑(f x) * I) * (↑(deriv f x) * I) = ↑(deriv f x) * I * cexp (↑(f x) * I)
Theorem: deriv.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (↑(f x) * I) * (↑(deriv f x) * I) = ↑(deriv f x) * I * cexp (↑(f x) * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: HasDerivAt.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x
Tactic:
suffices : HasDerivAt (fun x : ℝ => Complex.exp (f x • I)) (f' • (I * Complex.exp (f x • I))) x
Proof state after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x

case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Theorem: HasDerivAt.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x

case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Tactic:
. simpa [← mul_assoc] using this
Proof state after:
case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Theorem: HasDerivAt.cexp_real_smul_I
Proof state before:
case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Tactic:
exact HasDerivAt.comp_of_tower x Complex.hasDerivAt_exp_real_smul_I hf
Proof state after:
no goals
Theorem: HasDerivAt.cexp_real_smul_I
Proof state before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x
Tactic:
simpa [← mul_assoc] using this
Proof state after:
no goals
Theorem: Function.update_eq_add_sum_filter_single
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
⊢ update x i xi = Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = (Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)) j
Theorem: Function.update_eq_add_sum_filter_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = (Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)) j
Tactic:
simp
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Pi.single i xi j + if j = i then 0 else x j
Theorem: Function.update_eq_add_sum_filter_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Pi.single i xi j + if j = i then 0 else x j
Tactic:
by_cases h : j = i <;> simp [h]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j
Theorem: Function.update_eq_add_sum_filter_single
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j
Tactic:
rw [Pi.single]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = update 0 i xi j
Theorem: Function.update_eq_add_sum_filter_single
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = update 0 i xi j
Tactic:
simp [update, h]
Proof state after:
no goals
Theorem: Function.update_eq_sum_single
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
⊢ update x i xi = ∑ j : ι, if j = i then Pi.single i xi else Pi.single j (x j)
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Finset.sum Finset.univ (fun j => if j = i then Pi.single i xi else Pi.single j (x j)) j
Theorem: Function.update_eq_sum_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Finset.sum Finset.univ (fun j => if j = i then Pi.single i xi else Pi.single j (x j)) j
Tactic:
simp [ite_apply]
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = ∑ x_1 : ι, if x_1 = i then Pi.single i xi j else Pi.single x_1 (x x_1) j
Theorem: Function.update_eq_sum_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = ∑ x_1 : ι, if x_1 = i then Pi.single i xi j else Pi.single x_1 (x x_1) j
Tactic:
rw [Finset.sum_eq_single j]
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = if j = i then Pi.single i xi j else Pi.single j (x j) j

case h.h₀
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ ∀ b ∈ Finset.univ, b ≠ j → (if b = i then Pi.single i xi j else Pi.single b (x b) j) = 0

case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Theorem: Function.update_eq_sum_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = if j = i then Pi.single i xi j else Pi.single j (x j) j

case h.h₀
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ ∀ b ∈ Finset.univ, b ≠ j → (if b = i then Pi.single i xi j else Pi.single b (x b) j) = 0

case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Tactic:
. by_cases h : j = i <;> simp [h]
  rw [h]
  simp
Proof state after:
case h.h₀
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ ∀ b ∈ Finset.univ, b ≠ j → (if b = i then Pi.single i xi j else Pi.single b (x b) j) = 0

case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Theorem: Function.update_eq_sum_single
Proof state before:
case h.h₀
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ ∀ b ∈ Finset.univ, b ≠ j → (if b = i then Pi.single i xi j else Pi.single b (x b) j) = 0

case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Tactic:
. simp
  intro k hkj
  simp [hkj]
  intro hki
  rw [hki] at hkj
  simp [hkj]
Proof state after:
case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Theorem: Function.update_eq_sum_single
Proof state before:
case h.h₁
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ j ∉ Finset.univ → (if j = i then Pi.single i xi j else Pi.single j (x j) j) = 0
Tactic:
. simp
Proof state after:
no goals
Theorem: Function.update_eq_sum_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = if j = i then Pi.single i xi j else Pi.single j (x j) j
Tactic:
by_cases h : j = i <;> simp [h]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j
Theorem: Function.update_eq_sum_single
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j
Tactic:
rw [h]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi i = Pi.single i xi i
Theorem: Function.update_eq_sum_single
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi i = Pi.single i xi i
Tactic:
simp
Proof state after:
no goals