Finding a contradiction

Stream: new members

[Shadman Sakib]

The contradiction should be that since a : Z then a ≠ n would mean a is not in Z but Lean does not understand. How can I make this contradiction more explicit?

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

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

example (R : Type*) (n : ℤ) (θ : ℝ) (a : ℤ) (h : 2 ≠ 0)
  (h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
  [linear_ordered_ring R]
  (this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
  (ha : I * 2 + I * (↑θ / 2) =
          -(I * 2) + I * (↑θ / 2) + ↑a * (2 * ↑π * I))
  (this : (2 : ℂ) = ↑a * ↑π)
  (h₀ : (a :ℂ) = 2 / π)
  (h₂ : 0 < a)
  (h₄ : a < 1)
  (this₁ : a < 1 → 0 < a → ¬a = n)
  (this₃ : ¬a = n) :
  false :=
begin
  admit,
end

[Adam Topaz]

I think you're misunderstanding something here... it looks like a and n are both terms of Z, so there is no contradiction in saying that a and n are different. However, you can get a contradiction from $0<a$ and $a<1$ since a is an integer.

[Shadman Sakib]

Yes, I have a lemma that I proved showing that if 0 < a and a < 1 then a cannot equal any integer and this1 was the result. Lean will not let me create a have statement saying a is not in Z.

[Shadman Sakib]

Maybe this state will help

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

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

example (R : Type*) (n : ℤ) (θ : ℝ) (a : ℤ) (h : 2 ≠ 0)
  (h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
  [linear_ordered_ring R]
  (this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
  (ha : I * 2 + I * (↑θ / 2) =
          -(I * 2) + I * (↑θ / 2) + ↑a * (2 * ↑π * I))
  (this : (2 : ℂ) = ↑a * ↑π)
  (h₀ : (a : ℂ) = 2 / π)
  (h₂ : 0 < a)
  (h₄ : a < 1)
  (this₁ : ∀ (n : ℤ), a < 1 → 0 < a → ¬a = n) :
  false :=
begin
  admit,
end

[Shadman Sakib]

I introduced an n to this1, and applied this1 to h2 and h4, that is why in the previous #mwe this3 has a ≠ n

[Adam Topaz]

Saying "a is not in Z" when a : Z makes no sense in type theory.

[Adam Topaz]

It seems that this is an issue about understanding type theory, so I suggest looking at the relevant sections of #tpil

[Adam Topaz]

(i.e. ch. 2)