case h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v : ℙ K V
h✝ : map f hf u✝ = map f hf v
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u v : ℙ K V
h : map f hf u = map f hf v
⊢ u = v
induction' u using ind with u hu
case h.h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ mk K u hu = mk K v hv
case h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v : ℙ K V
h✝ : map f hf u✝ = map f hf v
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v
induction' v using ind with v hv
case h.h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : ∃ a, a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
case h.h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ mk K u hu = mk K v hv
simp only [map_mk, mk_eq_mk_iff'] at h ⊢
case h.h.intro
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
case h.h
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : ∃ a, a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
rcases h with ⟨a, ha⟩
case h.h.intro
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ↑f (↑τ a • v) = ↑f u
case h.h.intro
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
refine ⟨τ a, hf ?_⟩
no goals
case h.h.intro
K : Type u_1
V : Type u_3
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_2
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ↑f (↑τ a • v) = ↑f u
rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]