k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) s
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map f (v +ᵥ s) = ↑f.linear v +ᵥ map f s
erw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
case e_f
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v) = AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) s
congr 1
case e_f.h
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ ↑(AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) p✝ =
    ↑(AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) p✝
case e_f
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v) = AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f
ext
no goals
case e_f.h
k : Type u_1
inst✝⁹ : Ring k
V : Type ?u.30849
P : Type ?u.30852
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ ↑(AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) p✝ =
    ↑(AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) p✝
exact f.map_vadd _ _