Dealing with Type Coercion

Stream: new members

[Taylor Belcher]

I am trying to prove a trig identity, but I am struggling to remove the type coercions that I am showing up in my goals.

import data.nat.basic
import data.int.basic
import init.data.nat.gcd
import data.rat.basic
import data.real.basic
import data.complex.exponential
import analysis.special_functions.trigonometric
import algebra.euclidean_domain
import geometry.euclidean.basic

noncomputable theory
open_locale big_operators
open_locale classical
open_locale real
open_locale real_inner_product_space
open_locale euclidean_geometry

namespace real

variable (α : ℚ)

lemma periodic_cos (r:ℚ) (θ:ℝ) (a b:ℤ) (h0 : b≠0) (h1 : int.gcd a b = 1) (h2: r = a/b) (h3: θ = r * π) : ∀ (m:ℕ), cos (m*θ) = cos ((m % b)*θ) ∨ cos (m*θ) = -1 * cos ((m % b)*θ) :=
begin
intro m,

end

end real

Is the issue with how I am stating my assumptions? I have been unable to make progress on the goal because the coercions mean theorems I try to apply have pattern mismatch errors.

[Yakov Pechersky]

Have you tried just doing a simp first?

[Yakov Pechersky]

Or even a norm_cast?

[Taylor Belcher]

I did try simp, norm_cast unfortunately did not help either.

[Heather Macbeth]

What is the problem exactly? (i.e., what is a lemma you would like to apply which gives you errors.)

[Kevin Buzzard]

Coercions are a bit of an art. I would be tempted to go the whole way and not even have r or theta (they can be immediately eliminated with subst h2 and subst h3 anyway) and then just press on from there. You want to use div_add_mod or mod_add_div or whatever it's called, I guess

[Yakov Pechersky]

Right, you'd first want to get m*theta in a state that looks like some rational or integer times pi.