# Zulip Chat Archive

## Stream: general

### Topic: can you take cos of both sides?

#### James Arthur (Jul 15 2020 at 09:32):

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 (Jul 15 2020 at 09:40):

There's the `apply_fun`

tactic.

#### Johan Commelin (Jul 15 2020 at 09:40):

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

#### Johan Commelin (Jul 15 2020 at 09:40):

(I didn't try your code yet.)

#### James Arthur (Jul 15 2020 at 09:41):

both sides of the goal

#### Chris Hughes (Jul 15 2020 at 09:41):

`cosm`

needs to be injective for that right?

#### James Arthur (Jul 15 2020 at 09:41):

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 (Jul 15 2020 at 09:42):

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

#### Sebastien Gouezel (Jul 15 2020 at 09:44):

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 (Jul 15 2020 at 09:44):

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 (Jul 15 2020 at 09:45):

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 (Jul 15 2020 at 09:46):

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 (Jul 15 2020 at 09:46):

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

is 0 or not

#### Shing Tak Lam (Jul 15 2020 at 09:47):

Apologies for (maybe) leading you down a wrong path

#### James Arthur (Jul 15 2020 at 09:47):

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

#### James Arthur (Jul 15 2020 at 10:09):

Also thankyou all!

Last updated: Aug 03 2023 at 10:10 UTC