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
α : 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
ext x
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

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
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
cases' lt_or_le x a with hxa hax
no goals
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
simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]
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

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
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
cases' le_or_lt x b with hxb hbx
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
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
lift x to Icc a b using ⟨hax, hxb⟩
no goals
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
rw [IccExtend_val, comp_apply]
no goals
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
simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]