can you take cos of both sides?

Stream: general

[James Arthur]

Hi, I have a proof where I am trying to show that you can divide a version of generalised tangent and it's the same as tangent as $tan_m x = \frac{sin_m x}{cos_m x} = \frac{sin x * f(x)}{cos x * f(x)}$, where $f(x)$ is my radius function. I have got the following code thus far:

import tactic
import basic
import data.real.basic
import data.complex.exponential
import analysis.special_functions.pow

noncomputable theory
open_locale classical

open real

notation `|`x`|` := abs x


/- 002 -/
def radius (x m : ℝ) := 1 / ( |sin x| ^ m + |cos x| ^ m ) ^ (1/m)

/- 003 -/
def sinm (θ m : ℝ) := sin θ * radius θ m
-- trigonometric sin is defined!!

/- 004 -/
def cosm (θ m : ℝ) := cos θ * radius θ m
-- So we can onto prove somethings!
-- actually, let us go and define a few more things

/- 005 -/
def tanm (θ m : ℝ) := sinm θ m / cosm θ m

theorem tanm_eq_tan (x m : ℝ) (n : ℤ) (f : radius x m ≠ 0): tanm x m = tan x :=
begin
  unfold tanm,
  unfold sinm,
  unfold cosm,
  have H : cos x * radius x m ≠ 0,
  {simp only [ne.def, mul_eq_zero],
   intros h,
   cases h with m n,
   swap,
   {apply f, exact n,},
   { by_cases h : ∃ n, x = (2*n+1)/2 * pi,
    {sorry},
    { rw not_exists at h,
      apply h n,
      -- bit stuck here, want to just 'cos' both sides
      --rw [mul_zero, zero_add, mul_comm, ←div_eq_mul_one_div],
      sorry
    },
   },
  }
end

I have also proved this auxillary lemma but it doesn't seem to be much use:

lemma exists_cos_pi_half_eq_zero (x m : ℝ) (n : ℤ) : ∃ n, x = (2*n + 1) * pi / 2 → cos x = 0  :=
begin
  use 0,
  intros f,
  rw [mul_zero, zero_add, one_mul] at f,
  rw f,
  simp,
end

[Chris Hughes]

There's the apply_fun tactic.

[Johan Commelin]

@James Arthur But sides of the goal, or both sides of a hypothesis?

[Johan Commelin]

(I didn't try your code yet.)

[James Arthur]

both sides of the goal

[Chris Hughes]

cosm needs to be injective for that right?

[James Arthur]

current state of the goal:

1 goal
x m: ℝ
n: ℤ
f: radius x m ≠ 0
m: cos x = 0
h: ∀ (x_1 : ℝ), ¬x = (2 * x_1 + 1) / 2 * pi
⊢ x = (2 * ↑n + 1) / 2 * pi

[Chris Hughes]

Is it injective on some interval and you know both sides of the goal are in that interval?

[Sebastien Gouezel]

Wait, your assumption h is wrong, right? (take $x_1 = (2 \pi x -1)/2$). From this, you can deduce anything you want!

[James Arthur]

I believe that $cos x$ isn't injective than on 0 to $\frac{\pi}{2}$ and I haven't actually looked at $cosm x$ but my intuition says no. I removed the problemed areas in this case, i.e. where cosm goes to infinity

[James Arthur]

Sebastien Gouezel said:

Wait, your assumption h is wrong, right? (take $x_1 = (2 \pi x -1)/2$). From this, you can deduce anything you want!

Oh... yeah. it needs to be an integer XD

[Shing Tak Lam]

This was what I was alluding to yesterday. I didn't see your code for very long and the \exists ... may not have been the correct idea.

theorem tanm_eq_tan (x m : ℝ) (f : radius x m ≠ 0): tanm x m = tan x :=
begin
  unfold tanm sinm cosm,
  rw tan_eq_sin_div_cos,
  by_cases h : cos x = 0,
  { rw h, simp },
  rw div_eq_div_iff,
  ring,
  exact mul_ne_zero h f,
  exact h,
end

[Shing Tak Lam]

Since dividing by 0 in Lean gives you 0, so it's true whether cos x is 0 or not

[Shing Tak Lam]

Apologies for (maybe) leading you down a wrong path

[James Arthur]

It's ok. I was following your message. To be perfectly honest I had no idea where I was going

[James Arthur]

Also thankyou all!