-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_mk' (p : P) (direction : Submodule k V) :
    (mk' p direction).direction = direction

Proof state:
case h
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
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) ↔ v ∈ direction

Tactic:
constructor

Result:
case h.mp
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
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) → v ∈ direction

case h.mpr
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
direction : Submodule k V
v : V
⊢ v ∈ direction → ∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂

Proof state:
case h.mpr
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
direction : Submodule k V
v : V
⊢ v ∈ direction → ∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂

Tactic:
exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩

Result:
no goals

Proof state:
case h
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
direction : Submodule k V
v : V
⊢ v ∈ (mk' p direction).direction ↔ v ∈ direction

Tactic:
rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]

Result:
case h
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
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) ↔ v ∈ direction

Proof state:
case h.mp
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
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) → v ∈ direction

Tactic:
rintro ⟨p₁, ⟨v₁, hv₁, hp₁⟩, p₂, ⟨v₂, hv₂, hp₂⟩, hv⟩

Result:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
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
direction : Submodule k V
v : V
p₁ : P
v₁ : V
hv₁ : v₁ ∈ direction
hp₁ : p₁ = v₁ +ᵥ p
p₂ : P
hv : v = p₁ -ᵥ p₂
v₂ : V
hv₂ : v₂ ∈ direction
hp₂ : p₂ = v₂ +ᵥ p
⊢ v ∈ direction

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
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
direction : Submodule k V
v : V
p₁ : P
v₁ : V
hv₁ : v₁ ∈ direction
hp₁ : p₁ = v₁ +ᵥ p
p₂ : P
hv : v = p₁ -ᵥ p₂
v₂ : V
hv₂ : v₂ ∈ direction
hp₂ : p₂ = v₂ +ᵥ p
⊢ v₁ - v₂ ∈ direction

Tactic:
exact direction.sub_mem hv₁ hv₂

Result:
no goals

Proof state:
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
direction : Submodule k V
⊢ (mk' p direction).direction = direction

Tactic:
ext v

Result:
case h
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
direction : Submodule k V
v : V
⊢ v ∈ (mk' p direction).direction ↔ v ∈ direction

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
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
direction : Submodule k V
v : V
p₁ : P
v₁ : V
hv₁ : v₁ ∈ direction
hp₁ : p₁ = v₁ +ᵥ p
p₂ : P
hv : v = p₁ -ᵥ p₂
v₂ : V
hv₂ : v₂ ∈ direction
hp₂ : p₂ = v₂ +ᵥ p
⊢ v ∈ direction

Tactic:
rw [hv, hp₁, hp₂, vadd_vsub_vadd_cancel_right]

Result:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro
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
direction : Submodule k V
v : V
p₁ : P
v₁ : V
hv₁ : v₁ ∈ direction
hp₁ : p₁ = v₁ +ᵥ p
p₂ : P
hv : v = p₁ -ᵥ p₂
v₂ : V
hv₂ : v₂ ∈ direction
hp₂ : p₂ = v₂ +ᵥ p
⊢ v₁ - v₂ ∈ direction