arctan_two_eq

formal source

 148
 149/-- **PROVED**: `arctan(2) = π/4 + arctan(1/3)`.
 150    From the addition formula: `arctan(1) + arctan(1/3) = arctan(2)`. -/
 151theorem arctan_two_eq : arctan 2 = Real.pi / 4 + arctan (1 / 3) := by
 152  have h1 : arctan 1 = Real.pi / 4 := by
 153    rw [← tan_pi_div_four]
 154    exact arctan_tan (by linarith [pi_pos]) (by linarith [pi_pos])
 155  have hadd : arctan 1 + arctan (1 / 3) = arctan 2 := by
 156    rw [arctan_add (by norm_num : (1 : ℝ) * (1 / 3) < 1)]
 157    congr 1; norm_num
 158  linarith
 159
 160/-- Interval containing arctan 2 = π/4 + arctan(1/3) -/
 161def arctanTwoInterval : Interval :=
 162  let pi4 := smulPos (1 / 4) piInterval (by norm_num)
 163  add pi4 arctanOneThirdInterval
 164
 165/-- **PROVED**: arctan(2) is in arctanTwoInterval. -/
 166theorem arctan_two_in_interval :
 167    arctanTwoInterval.contains (arctan 2) := by
 168  rw [arctan_two_eq]
 169  unfold arctanTwoInterval
 170  apply add_contains_add
 171  · -- π/4 is in (1/4) · piInterval
 172    have hpi := pi_in_piInterval
 173    have := smulPos_contains_smul (q := 1 / 4) (by norm_num : (0 : ℚ) < 1 / 4) hpi
 174    simp only [Rat.cast_div, Rat.cast_one, Rat.cast_ofNat] at this
 175    convert this using 1
 176    ring
 177  · exact arctan_one_third_in_interval
 178
 179end IndisputableMonolith.Numerics