-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiff_update [DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) :
    ContDiff 𝕜 k (update x i)

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
h : ¬j = i
⊢ ContDiff 𝕜 k fun x_1 => x j

Tactic:
exact contDiff_const

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
h : j = i
⊢ ContDiff 𝕜 k fun x => ⋯ ▸ x

Tactic:
subst h

Result:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
j : ι
⊢ ContDiff 𝕜 k fun x => ⋯ ▸ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i : ι
⊢ ContDiff 𝕜 k (update x i)

Tactic:
rw [contDiff_pi]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i : ι
⊢ ∀ (i_1 : ι), ContDiff 𝕜 k fun x_1 => update x i x_1 i_1

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 k fun x_1 => if h : j = i then ⋯ ▸ x_1 else x j

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
h : j = i
⊢ ContDiff 𝕜 k fun x => ⋯ ▸ x

case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
h : ¬j = i
⊢ ContDiff 𝕜 k fun x_1 => x j

Proof state:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
j : ι
⊢ ContDiff 𝕜 k fun x => ⋯ ▸ x

Tactic:
exact contDiff_id

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 k fun x_1 => update x i x_1 j

Tactic:
dsimp [Function.update]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 k fun x_1 => if h : j = i then ⋯ ▸ x_1 else x j

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i : ι
⊢ ∀ (i_1 : ι), ContDiff 𝕜 k fun x_1 => update x i x_1 i_1

Tactic:
intro j

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : WithTop ℕ∞
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 k fun x_1 => update x i x_1 j