R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y, y ∈ p ∧ ↑↑e y = x) ↔ ↑(LinearEquiv.symm e) x ∈ p
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ x ∈ map (↑e) p ↔ ↑(LinearEquiv.symm e) x ∈ p
rw [Submodule.mem_map]
case mp
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y, y ∈ p ∧ ↑↑e y = x) → ↑(LinearEquiv.symm e) x ∈ p

case mpr
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ ↑(LinearEquiv.symm e) x ∈ p → ∃ y, y ∈ p ∧ ↑↑e y = x
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y, y ∈ p ∧ ↑↑e y = x) ↔ ↑(LinearEquiv.symm e) x ∈ p
constructor
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
y : M
hy : y ∈ p
hx : ↑↑e y = x
⊢ ↑(LinearEquiv.symm e) x ∈ p
case mp
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y, y ∈ p ∧ ↑↑e y = x) → ↑(LinearEquiv.symm e) x ∈ p
rintro ⟨y, hy, hx⟩
no goals
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
y : M
hy : y ∈ p
hx : ↑↑e y = x
⊢ ↑(LinearEquiv.symm e) x ∈ p
simp [← hx, hy]
case mpr
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : ↑(LinearEquiv.symm e) x ∈ p
⊢ ∃ y, y ∈ p ∧ ↑↑e y = x
case mpr
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ ↑(LinearEquiv.symm e) x ∈ p → ∃ y, y ∈ p ∧ ↑↑e y = x
intro hx
no goals
case mpr
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : ↑(LinearEquiv.symm e) x ∈ p
⊢ ∃ y, y ∈ p ∧ ↑↑e y = x
refine' ⟨e.symm x, hx, by simp⟩
no goals
R : Type u_1
R₁ : Type ?u.2247631
R₂ : Type u_2
R₃ : Type ?u.2247637
R₄ : Type ?u.2247640
S : Type ?u.2247643
K : Type ?u.2247646
K₂ : Type ?u.2247649
M : Type u_3
M' : Type ?u.2247655
M₁ : Type ?u.2247658
M₂ : Type u_4
M₃ : Type ?u.2247664
M₄ : Type ?u.2247667
N : Type ?u.2247670
N₂ : Type ?u.2247673
ι : Type ?u.2247676
V : Type ?u.2247679
V₂ : Type ?u.2247682
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : ↑(LinearEquiv.symm e) x ∈ p
⊢ ↑↑e (↑(LinearEquiv.symm e) x) = x
simp