Dividing values to left side of equation

Stream: new members

[Shadman Sakib]

import analysis.complex.circle
import analysis.special_functions.trigonometric
import group_theory.specific_groups.dihedral
noncomputable theory

open complex dihedral_group

local notation `|` x `|` := complex.abs x
local notation `π` := real.pi

lemma random (θ : ℝ) (a : ℤ) (hyp : 2 ≠ 0)
  (this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
  (ha : (2 : ℂ) = ↑a * ↑π) :
  (a : ℂ) = 2 / (↑π) :=
begin
  sorry,
end

[Shadman Sakib]

How would I finish off this proof? As ring or simp do not work

[Kyle Miller]

import analysis.complex.circle
import analysis.special_functions.trigonometric
noncomputable theory

open complex

local notation `π` := real.pi

lemma random (a : ℤ)
  (ha : (2 : ℂ) = ↑a * ↑π) :
  (a : ℂ) = 2 / (↑π) :=
begin
  rw ha,
  simp [real.pi_ne_zero],
end

[Yakov Pechersky]

  field_simp [real.pi_ne_zero, ha]

[Yakov Pechersky]

Basically, field_simp will get rid of all denominators, as long as it knows that the denoms aren't zero.

[Yakov Pechersky]

But I did it without simp at first:

lemma random (θ : ℝ) (a : ℤ) (hyp : 2 ≠ 0)
  (this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
  (ha : (2 : ℂ) = ↑a * ↑π) :
  (a : ℂ) = 2 / (↑π) :=
begin
  have : (π : ℂ) ≠ 0,
  { simpa using real.pi_ne_zero },
  rw [ha, mul_div_assoc, div_self this, mul_one]
end

[Yakov Pechersky]

Guessed the lemma names.

[Kevin Buzzard]

Shadman Sakib said:

How would I finish off this proof? As ring or simp do not work

ring proves goals in ring theory; your conclusion has a division in. simp is an equational rewriter and won't be able to get from a*pi/pi back to a as the corresponding lemma needs a proof that pi isn't zero, which the simplifier can only look for in the local context and it's not there. You have an unnecessary hypothesis that 2 (probably the natural number 2) isn't zero, but if you put the hypothesis that (pi : C) isn't zero then simp * would have some chance.

[Shadman Sakib]

Ahh okay, thank you!