X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ (if ↑x.snd ≤ 1 / 2 then ↑x.fst * 2 * ↑x.snd else ↑x.fst * (2 - 2 * ↑x.snd)) ∈ I
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I
dsimp only [reflTransSymmAux]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ∈ I

case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ∈ I
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ (if ↑x.snd ≤ 1 / 2 then ↑x.fst * 2 * ↑x.snd else ↑x.fst * (2 - 2 * ↑x.snd)) ∈ I
split_ifs
case inl.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2 * ↑x.snd

case inl.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ≤ 1
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ∈ I
constructor
case inl.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2

case inl.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
case inl.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2 * ↑x.snd
apply mul_nonneg
case inl.left.ha.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst

case inl.left.ha.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
case inl.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2
apply mul_nonneg
no goals
case inl.left.ha.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
unit_interval
no goals
case inl.left.ha.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
norm_num
no goals
case inl.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
unit_interval
case inl.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 * ↑x.snd) ≤ 1
case inl.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ≤ 1
rw [mul_assoc]
case inl.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1

case inl.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.snd

case inl.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 2 * ↑x.snd ≤ 1
case inl.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 * ↑x.snd) ≤ 1
apply mul_le_one
no goals
case inl.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
unit_interval
case inl.right.hb'.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2

case inl.right.hb'.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
case inl.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.snd
apply mul_nonneg
no goals
case inl.right.hb'.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
norm_num
no goals
case inl.right.hb'.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
unit_interval
no goals
case inl.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 2 * ↑x.snd ≤ 1
linarith
case inr.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * (2 - 2 * ↑x.snd)

case inr.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ≤ 1
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ∈ I
constructor
case inr.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst

case inr.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
case inr.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * (2 - 2 * ↑x.snd)
apply mul_nonneg
no goals
case inr.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
no goals
case inr.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
unit_interval
case inr.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1

case inr.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd

case inr.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 2 - 2 * ↑x.snd ≤ 1
case inr.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ≤ 1
apply mul_le_one
no goals
case inr.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
unit_interval
no goals
case inr.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
no goals
case inr.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 2 - 2 * ↑x.snd ≤ 1
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]