K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v
rw [mk_eq_mk_iff K v w hv hw]
case mp
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

case mpr
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v
constructor
case mp.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v
case mp
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
rintro ⟨a, ha⟩
no goals
case mp.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v
exact ⟨a, ha⟩
case mpr.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v
case mpr
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
rintro ⟨a, ha⟩
case mpr.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
case mpr.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v
refine' ⟨Units.mk0 a fun c => hv.symm _, ha⟩
no goals
case mpr.intro
K : Type u_2
V : Type u_1
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
rwa [c, zero_smul] at ha