diff --git a/src/analysis/special_functions/trigonometric/basic.lean b/src/analysis/special_functions/trigonometric/basic.lean
index 6969a50c07909..ccea9b8955f7a 100644
--- a/src/analysis/special_functions/trigonometric/basic.lean
+++ b/src/analysis/special_functions/trigonometric/basic.lean
@@ -761,6 +761,9 @@ tan_periodic.sub_eq x
 lemma tan_pi_sub (x : ℝ) : tan (π - x) = -tan x :=
 tan_neg x ▸ tan_periodic.sub_eq'
 
+lemma tan_pi_div_two_sub (x : ℝ) : tan (π / 2 - x) = (tan x)⁻¹ :=
+by rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
+
 lemma tan_nat_mul_pi (n : ℕ) : tan (n * π) = 0 :=
 tan_zero ▸ tan_periodic.nat_mul_eq n
 
@@ -990,6 +993,9 @@ tan_periodic.sub_eq x
 lemma tan_pi_sub (x : ℂ) : tan (π - x) = -tan x :=
 tan_neg x ▸ tan_periodic.sub_eq'
 
+lemma tan_pi_div_two_sub (x : ℂ) : tan (π / 2 - x) = (tan x)⁻¹ :=
+by rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
+
 lemma tan_nat_mul_pi (n : ℕ) : tan (n * π) = 0 :=
 tan_zero ▸ tan_periodic.nat_mul_eq n