t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
t : ↑I
⊢ ↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
simp only [qRight, coe_zero, add_zero, div_one]
case inl
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 2 * ↑t

case inr
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 1
t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
split_ifs
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
case inl
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 2 * ↑t
rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
refine' ⟨t.2.1, _⟩
no goals
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2
tauto
case inr
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
case inr
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 1
rw [(Set.projIcc_eq_right _).2]
no goals
case inr
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t
linarith
no goals
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
exact zero_lt_one