Theorem: contDiff_ofReal (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
have key x : HasDerivAt ofReal' 1 x := hasDerivAt_id x |>.ofReal_comp
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ ContDiff ℝ ⊤ ofReal'

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
have key' : deriv ofReal' = fun _ => 1 := by ext x ; exact (key x).deriv
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ ofReal'

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
refine contDiff_top_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ (deriv ofReal')

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ (deriv ofReal')
Tactic:
simpa [key'] using contDiff_const
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ deriv ofReal' = fun x => 1
Tactic:
ext x
State after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
x : ℝ
⊢ deriv ofReal' x = 1

State before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
x : ℝ
⊢ deriv ofReal' x = 1
Tactic:
exact (key x).deriv
State after:
no goals