case inl
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
⊢ map f (affineSpan k ∅) = affineSpan k (↑f '' ∅)

case inr.intro
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k (↑f '' s)
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k (↑f '' s)
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
case inr.intro.hd
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ direction (map f (affineSpan k s)) = direction (affineSpan k (↑f '' s))

case inr.intro.hn
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ Set.Nonempty (↑(map f (affineSpan k s)) ∩ ↑(affineSpan k (↑f '' s)))
case inr.intro
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k (↑f '' s)
apply ext_of_direction_eq
no goals
case inl
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
⊢ map f (affineSpan k ∅) = affineSpan k (↑f '' ∅)
rw [image_empty, span_empty, span_empty, map_bot]
no goals
case inr.intro.hd
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ direction (map f (affineSpan k s)) = direction (affineSpan k (↑f '' s))
simp [direction_affineSpan]
no goals
case inr.intro.hn
k : Type u_3
V₁ : Type u_5
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.571682
P₃ : Type ?u.571685
inst✝⁹ : Ring k
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₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ Set.Nonempty (↑(map f (affineSpan k s)) ∩ ↑(affineSpan k (↑f '' s)))
exact
  ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
    subset_affineSpan k _ (mem_image_of_mem f hp)⟩