t : ↑I
⊢ Set.projIcc 0 1 qRight.proof_1 (2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd)) = Set.projIcc 0 1 (_ : 0 ≤ 1) ↑t
t : ↑I
⊢ qRight (t, 1) = Set.projIcc 0 1 (_ : 0 ≤ 1) ↑t
rw [qRight]
case e_x
t : ↑I
⊢ 2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd) = ↑t
t : ↑I
⊢ Set.projIcc 0 1 qRight.proof_1 (2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd)) = Set.projIcc 0 1 (_ : 0 ≤ 1) ↑t
congr
case e_x
t : ↑I
⊢ 2 * ↑t / 2 = ↑t
case e_x
t : ↑I
⊢ 2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd) = ↑t
norm_num
case e_x.ha
t : ↑I
⊢ 2 ≠ 0
case e_x
t : ↑I
⊢ 2 * ↑t / 2 = ↑t
apply mul_div_cancel_left
no goals
case e_x.ha
t : ↑I
⊢ 2 ≠ 0
exact two_ne_zero