case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ direction

case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ ∈ mk' p₁ direction
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
⊢ p₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ AffineSubspace.direction (mk' p₁ direction)
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ direction
rw [← direction_mk' p₁ direction]
no goals
case refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ AffineSubspace.direction (mk' p₁ direction)
exact vsub_mem_direction h (self_mem_mk' _ _)
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ -ᵥ p₁ +ᵥ p₁ ∈ mk' p₁ direction
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ ∈ mk' p₁ direction
rw [← vsub_vadd p₂ p₁]
no goals
case refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ -ᵥ p₁ +ᵥ p₁ ∈ mk' p₁ direction
exact vadd_mem_mk' p₁ h