calc

Stream: new members

[merle]

hi, I'm not sure why I'm getting an error using calc. it says it's an invalid step, this is what I've written so far:

theorem question_1 : ¬ (∃ z : ℂ, (abs z = 1) ∧ (abs (z + (I * sqrt 5)) = 1)) := by

intro h

rcases h with ⟨z, hz₁, hz₂⟩

have contradiction : 1 < 1 := by

calc

1 < Complex.abs (1 - Real.sqrt 5) := by sorry

_ < 1 := by sorry

[Julian Berman]

Welcome. Can you have a look at #backticks (that's a link) which should give you a tip about how to format your message so it's a bit easier to read!

[Julian Berman]

A quick look at #mwe would also be helpful, what you have there looks like it has some imports that you should share as well.

[merle]

thank you! I'll have a look. I have some imports but at the top of the page, I'll include those once I've read the link

[merle]

import Mathlib.Data.Complex.Abs
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Analysis.Complex.Basic

namespace APPS2

open Real

open Complex


theorem question_1 : ¬ (∃ z : ℂ, (abs z = 1) ∧ (abs (z + (I * sqrt 5)) = 1)) := by
  intro h
  rcases h with ⟨z, hz₁, hz₂⟩
  have contradiction : 1 < 1 := by
    calc
      1 < Complex.abs (1 - Real.sqrt 5) := by sorry
      _ < 1 := by sorry

end APPS2

[Etienne Marion]

The issue is that when you write contradiction : 1 < 1, Lean interprets 1 as a natural integer because it has no way to know you use it as a real number, but then you compare it to real numbers, that's why there's a problem. If you write instead contradiction : (1 : ℝ) < 1 it should work fine.

[merle]

ah ok, thank you for explaining :) that worked