case h
k : Type u_2
inst✝⁹ : Ring k
V : Type u_3
P : Type u_1
V₁ : Type ?u.20295
P₁ : Type ?u.20298
V₂ : Type ?u.20301
P₂ : Type ?u.20304
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₂
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥
k : Type u_2
inst✝⁹ : Ring k
V : Type u_3
P : Type u_1
V₁ : Type ?u.20295
P₁ : Type ?u.20298
V₂ : Type ?u.20301
P₂ : Type ?u.20304
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₂
v : V
⊢ v +ᵥ ⊥ = ⊥
ext
no goals
case h
k : Type u_2
inst✝⁹ : Ring k
V : Type u_3
P : Type u_1
V₁ : Type ?u.20295
P₁ : Type ?u.20298
V₂ : Type ?u.20301
P₂ : Type ?u.20304
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₂
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥
simp [pointwise_vadd_eq_map, map_bot]