lean_workbook_plus_11345
Proved, which indeed fits
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11345 (f : ℝ → ℝ) (hf: f = fun x => x + 1) : ∀ x, f x = x + 1 := by sorry
Source
, which indeed fits
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11345 (f : ℝ → ℝ) (hf: f = fun x => x + 1) : ∀ x, f x = x + 1 := by sorry