k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ ↑f '' Set.uIcc a b = Set.uIcc (↑f a) (↑f b)
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ↑f '' Set.uIcc a b = Set.uIcc (↑f a) (↑f b)
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
  ext x
  change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
  rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
  simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ (fun x => x + ↑f 0) '' ((fun x => x * (↑f 1 - ↑f 0)) '' Set.uIcc a b) =
    Set.uIcc (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) a)
      (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) b)
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ ↑f '' Set.uIcc a b = Set.uIcc (↑f a) (↑f b)
rw [this, Set.image_comp]
no goals
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ (fun x => x + ↑f 0) '' ((fun x => x * (↑f 1 - ↑f 0)) '' Set.uIcc a b) =
    Set.uIcc (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) a)
      (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) b)
simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) x
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
ext x
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = x • (↑f 1 -ᵥ ↑f 0) +ᵥ ↑f 0
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) x
change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ↑f (x • (1 -ᵥ 0) +ᵥ 0)
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = x • (↑f 1 -ᵥ ↑f 0) +ᵥ ↑f 0
rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
no goals
case h
k✝ : Type ?u.614974
V1 : Type ?u.614977
P1 : Type ?u.614980
V2 : Type ?u.614983
P2 : Type ?u.614986
V3 : Type ?u.614989
P3 : Type ?u.614992
V4 : Type ?u.614995
P4 : Type ?u.614998
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_1
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ↑f (x • (1 -ᵥ 0) +ᵥ 0)
simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]