[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = { val := a, property := (_ : a ∈ Icc a b) }
[PROOFSTEP]
simp [projIcc, hx, hx.trans h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = { val := b, property := (_ : b ∈ Icc a b) }
[PROOFSTEP]
simp [projIcc, hx, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
⊢ projIci a x = { val := a, property := (_ : a ≤ a) } ↔ x ≤ a
[PROOFSTEP]
simp [projIci, Subtype.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
⊢ projIic b x = { val := b, property := (_ : b ≤ b) } ↔ b ≤ x
[PROOFSTEP]
simp [projIic, Subtype.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
⊢ projIcc a b (_ : a ≤ b) x = { val := a, property := (_ : a ∈ Icc a b) } ↔ x ≤ a
[PROOFSTEP]
simp [projIcc, Subtype.ext_iff, h.not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
⊢ projIcc a b (_ : a ≤ b) x = { val := b, property := (_ : b ∈ Icc a b) } ↔ b ≤ x
[PROOFSTEP]
simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Ici a
⊢ projIci a x = { val := x, property := hx }
[PROOFSTEP]
simpa [projIci]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Iic b
⊢ projIic b x = { val := x, property := hx }
[PROOFSTEP]
simpa [projIic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ projIcc a b h x = { val := x, property := hx }
[PROOFSTEP]
simp [projIcc, hx.1, hx.2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Ici a)
⊢ projIci a ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIci_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Iic b)
⊢ projIic b ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIic_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Icc a b)
⊢ projIcc a b h ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIcc_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ projIci a x < projIci a y
[PROOFSTEP]
simpa only [projIci_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ projIic b x < projIic b y
[PROOFSTEP]
simpa only [projIic_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y
[PROOFSTEP]
simpa only [projIcc_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Ici a) → β
⊢ range (IciExtend f) = range f
[PROOFSTEP]
simp only [IciExtend, range_comp f, range_projIci, range_id', image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Iic b) → β
⊢ range (IicExtend f) = range f
[PROOFSTEP]
simp only [IicExtend, range_comp f, range_projIic, range_id', image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Icc a b) → β
⊢ range (IccExtend h f) = range f
[PROOFSTEP]
simp only [IccExtend, range_comp f, range_projIcc, image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
⊢ IccExtend h (f ∘ Subtype.val) = f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
cases' lt_or_le x a with hxa hax
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hxa : x < a
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
cases' le_or_lt x b with hxb hbx
[GOAL]
case h.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
lift x to Icc a b using ⟨hax, hxb⟩
[GOAL]
case h.inr.inl.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x // x ∈ Icc a b }
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) ↑x = f ↑x
[PROOFSTEP]
rw [IccExtend_val, comp_apply]
[GOAL]
case h.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]
