case refine'_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_5
P₂ : Type u_4
V₃ : Type ?u.555099
P₃ : Type ?u.555102
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 : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥

case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_5
P₂ : Type u_4
V₃ : Type ?u.555099
P₃ : Type ?u.555102
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 : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_5
P₂ : Type u_4
V₃ : Type ?u.555099
P₃ : Type ?u.555102
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 : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥
refine' ⟨fun h => _, fun h => _⟩
no goals
case refine'_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_5
P₂ : Type u_4
V₃ : Type ?u.555099
P₃ : Type ?u.555102
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 : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥
rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
no goals
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_5
P₂ : Type u_4
V₃ : Type ?u.555099
P₃ : Type ?u.555102
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 : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥
rw [h, map_bot]