Is there a proof (or counterexample maybe)? Asking for help

Stream: new members

[Ilmārs Cīrulis]

... again :sweat_smile:
(Wasted enough time to decide that it's probably reasonable to ask for help.)

import Mathlib

lemma aux (x : ℝ) (H : x ∈ Set.Icc 0 (2 * Real.pi)) (H0 : (Real.Angle.coe (- x)).toReal < 0) :
    x ∈ Set.Ioo 0 Real.pi := by
  sorry

[Aaron Liu]

import Mathlib

lemma aux (x : ℝ) (H : x ∈ Set.Icc 0 (2 * Real.pi)) (H0 : (Real.Angle.coe (- x)).toReal < 0) :
    x ∈ Set.Ioo 0 Real.pi := by
  contrapose! H0
  obtain ⟨hl, hr⟩ := H
  apply eq_or_lt_of_le at hl
  obtain rfl | hx := hl
  · simp
  simp only [Set.mem_Ioo, not_and, not_lt, hx, true_imp_iff] at H0
  rw [Real.Angle.toReal_coe, ← toIocMod_add_left, ← sub_eq_add_neg,
    (toIocMod_eq_self Real.two_pi_pos).2 ⟨by linarith, by linarith⟩]
  linarith

[Ilmārs Cīrulis]

Thank you very much! :love:

[Ilmārs Cīrulis]

My try with another similar lemma. It was success! :partying_face:

import Mathlib

lemma angle_def_aux01 (x : ℝ) (H : x ∈ Set.Icc (-Real.pi) Real.pi)
    (H0 : 0 ≤ (Real.Angle.coe x).toReal) :
    x = - Real.pi ∨ x ∈ Set.Icc 0 Real.pi := by
  have H1 : x = - Real.pi ∨ x ∈ Set.Ioc (- Real.pi) Real.pi := by grind
  obtain H1 | H1 := H1
  · left; exact H1
  · right
    contrapose! H0
    simp at *
    obtain ⟨H2, H3⟩ := H1
    apply eq_or_lt_of_le at H3
    obtain H3 | H3 := H3
    · rw [H3] at H0
      linarith [H0 Real.pi_nonneg]
    · obtain H4 | H4 := lt_or_ge x 0
      · rw [Real.Angle.toReal_coe,
           (toIocMod_eq_self Real.two_pi_pos).mpr ⟨by linarith, by linarith⟩]
        exact H4
      · linarith [H0 H4]