eq one of le mul in the unit

Stream: Is there code for X?

[Ira Fesefeldt]

I have a hard time proving the following

import Mathlib

open unitInterval

example {i j : I} (h_i : i ≠ 0) (h : i ≤ j * i) : j = 1 := by sorry

Is there maybe something related in the reals, that helps me, that I can't find?

[Yaël Dillies]

This isn't true if i = 0, right?

[Ira Fesefeldt]

Right

[Ira Fesefeldt]

Let's add that as a premise (I edited the mwe)

[Ruben Van de Velde]

import Mathlib

open unitInterval

example {i j : I} (h_i : i ≠ 0) (h : i ≤ j * i) : j = 1 := by
  have : 0 ≤ i := sorry
  have : 0 < i := sorry
  have : 0 ≤ j := sorry
  have : i ≤ 1 := sorry
  have : j ≤ 1 := sorry
  apply le_antisymm ‹_›
  contrapose! h
  refine Subtype.coe_lt_coe.mp ?_ -- apply?
  push_cast
  exact mul_lt_of_lt_one_left ‹_› h -- apply?

[Ira Fesefeldt]

Thanks!

[Jireh Loreaux]

@Ira Fesefeldt I think we have some missing API around docs#unitInterval. Do you care to add these first four lemmas to Mathlib? (and if you want, the 5th one too, which was your original question, with an appropriate name).

import Mathlib

namespace unitInterval

@[norm_cast]
lemma coe_pos {x : I} : (0 : ℝ) < x ↔ 0 < x := Iff.rfl

@[norm_cast]
lemma coe_lt_one {x : I} : (x : ℝ) < 1 ↔ x < 1 := Iff.rfl

@[simp]
lemma ne_zero_iff_pos {x : I} : x ≠ 0 ↔ 0 < x := by
  rw [← coe_ne_zero, ← coe_pos, lt_iff_le_and_ne, and_iff_right (nonneg x), ne_comm]

@[simp]
lemma ne_one_iff_lt {x : I} : x ≠ 1 ↔ x < 1 := by
  rw [← coe_lt_one, ← coe_ne_one, lt_iff_le_and_ne, and_iff_right (le_one x)]

example {i j : I} (h_i : i ≠ 0) (h : i ≤ j * i) : j = 1 := by
  contrapose! h
  simp only [ne_eq, ne_one_iff_lt, ← coe_lt_one, ne_zero_iff_pos, ← coe_pos] at h h_i
  exact Subtype.coe_lt_coe.mp <| by simpa using mul_lt_mul_of_pos_right h h_i

[Ira Fesefeldt]

Sure, I can do that tomorrow. I think I also have some other lemmas in my project about the unitInterval that I may just add as well in that PR.