-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem reflTransSymmAux_mem_I (x : I × I) : reflTransSymmAux x ∈ I

Proof state:
case neg.left
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
apply mul_nonneg

Result:
case neg.left.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

case neg.left.hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

Proof state:
case neg.right
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ≤ 1

Tactic:
apply mul_le_one₀

Result:
case neg.right.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case neg.right.hb₀
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

case neg.right.hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 2 - 2 * ↑x.2 ≤ 1

Proof state:
case pos.left
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2 * ↑x.2

Tactic:
apply mul_nonneg

Result:
case pos.left.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2

case pos.left.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2

Proof state:
case neg.right.hb₀
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

Tactic:
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]

Result:
no goals

Proof state:
case pos.right.hb₀.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2

Tactic:
unit_interval

Result:
no goals

Proof state:
x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I

Tactic:
dsimp only [reflTransSymmAux]

Result:
x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then ↑x.1 * 2 * ↑x.2 else ↑x.1 * (2 - 2 * ↑x.2)) ∈ I

Proof state:
case neg.left.hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

Tactic:
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]

Result:
no goals

Proof state:
x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then ↑x.1 * 2 * ↑x.2 else ↑x.1 * (2 - 2 * ↑x.2)) ∈ I

Tactic:
split_ifs

Result:
case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I

Proof state:
case pos.left.ha.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

Tactic:
unit_interval

Result:
no goals

Proof state:
case pos.left.ha.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
case pos.right.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 2 * ↑x.2 ≤ 1

Tactic:
linarith

Result:
no goals

Proof state:
case neg.left.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

Tactic:
unit_interval

Result:
no goals

Proof state:
case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

Tactic:
constructor

Result:
case pos.left
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2 * ↑x.2

case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ≤ 1

Proof state:
case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I

Tactic:
constructor

Result:
case neg.left
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * (2 - 2 * ↑x.2)

case neg.right
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ≤ 1

Proof state:
case neg.right.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

Tactic:
unit_interval

Result:
no goals

Proof state:
case neg.right.hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 2 - 2 * ↑x.2 ≤ 1

Tactic:
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]

Result:
no goals

Proof state:
case pos.right.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

Tactic:
unit_interval

Result:
no goals

Proof state:
case pos.right.hb₀.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
case pos.left.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2

Tactic:
apply mul_nonneg

Result:
case pos.left.ha.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1

case pos.left.ha.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2

Proof state:
case pos.left.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2

Tactic:
unit_interval

Result:
no goals

Proof state:
case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 * ↑x.2) ≤ 1

Tactic:
apply mul_le_one₀

Result:
case pos.right.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case pos.right.hb₀
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.2

case pos.right.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 2 * ↑x.2 ≤ 1

Proof state:
case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ≤ 1

Tactic:
rw [mul_assoc]

Result:
case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 * ↑x.2) ≤ 1

Proof state:
case pos.right.hb₀
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.2

Tactic:
apply mul_nonneg

Result:
case pos.right.hb₀.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2

case pos.right.hb₀.hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.2