lean_workbook_plus_9177
ProvedFind given and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9177 (a b : ℝ) (h₁ : a = 3) (h₂ : b = a * Real.sqrt 2) : b = 3 * Real.sqrt 2 := by sorry
Source
Find given and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9177 (a b : ℝ) (h₁ : a = 3) (h₂ : b = a * Real.sqrt 2) : b = 3 * Real.sqrt 2 := by sorry