case mp
R : Type u_1
R₁ : Type ?u.2284641
R₂ : Type u_2
R₃ : Type ?u.2284647
R₄ : Type ?u.2284650
S : Type ?u.2284653
K✝ : Type ?u.2284656
K₂ : Type ?u.2284659
M : Type u_3
M' : Type ?u.2284665
M₁ : Type ?u.2284668
M₂ : Type u_4
M₃ : Type ?u.2284674
M₄ : Type ?u.2284677
N : Type ?u.2284680
N₂ : Type ?u.2284683
ι : Type ?u.2284686
V : Type ?u.2284689
V₂ : Type ?u.2284692
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 τ₂₁ τ₁₂
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map e (map (LinearEquiv.symm e) K) = K

case mpr
R : Type u_1
R₁ : Type ?u.2284641
R₂ : Type u_2
R₃ : Type ?u.2284647
R₄ : Type ?u.2284650
S : Type ?u.2284653
K : Type ?u.2284656
K₂ : Type ?u.2284659
M : Type u_3
M' : Type ?u.2284665
M₁ : Type ?u.2284668
M₂ : Type u_4
M₃ : Type ?u.2284674
M₄ : Type ?u.2284677
N : Type ?u.2284680
N₂ : Type ?u.2284683
ι : Type ?u.2284686
V : Type ?u.2284689
V₂ : Type ?u.2284692
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₂
⊢ map (LinearEquiv.symm e) (map e p) = p
R : Type u_1
R₁ : Type ?u.2284641
R₂ : Type u_2
R₃ : Type ?u.2284647
R₄ : Type ?u.2284650
S : Type ?u.2284653
K✝ : Type ?u.2284656
K₂ : Type ?u.2284659
M : Type u_3
M' : Type ?u.2284665
M₁ : Type ?u.2284668
M₂ : Type u_4
M₃ : Type ?u.2284674
M₄ : Type ?u.2284677
N : Type ?u.2284680
N₂ : Type ?u.2284683
ι : Type ?u.2284686
V : Type ?u.2284689
V₂ : Type ?u.2284692
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₂
K : Submodule R₂ M₂
⊢ map (LinearEquiv.symm e) K = p ↔ map e p = K
constructor <;> rintro rfl
no goals
case mp
R : Type u_1
R₁ : Type ?u.2284641
R₂ : Type u_2
R₃ : Type ?u.2284647
R₄ : Type ?u.2284650
S : Type ?u.2284653
K✝ : Type ?u.2284656
K₂ : Type ?u.2284659
M : Type u_3
M' : Type ?u.2284665
M₁ : Type ?u.2284668
M₂ : Type u_4
M₃ : Type ?u.2284674
M₄ : Type ?u.2284677
N : Type ?u.2284680
N₂ : Type ?u.2284683
ι : Type ?u.2284686
V : Type ?u.2284689
V₂ : Type ?u.2284692
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 τ₂₁ τ₁₂
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map e (map (LinearEquiv.symm e) K) = K
calc
  map e (map e.symm K) = comap e.symm (map e.symm K) := map_equiv_eq_comap_symm _ _
  _ = K := comap_map_eq_of_injective e.symm.injective _
no goals
case mpr
R : Type u_1
R₁ : Type ?u.2284641
R₂ : Type u_2
R₃ : Type ?u.2284647
R₄ : Type ?u.2284650
S : Type ?u.2284653
K : Type ?u.2284656
K₂ : Type ?u.2284659
M : Type u_3
M' : Type ?u.2284665
M₁ : Type ?u.2284668
M₂ : Type u_4
M₃ : Type ?u.2284674
M₄ : Type ?u.2284677
N : Type ?u.2284680
N₂ : Type ?u.2284683
ι : Type ?u.2284686
V : Type ?u.2284689
V₂ : Type ?u.2284692
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₂
⊢ map (LinearEquiv.symm e) (map e p) = p
calc
  map e.symm (map e p) = comap e (map e p) := (comap_equiv_eq_map_symm _ _).symm
  _ = p := comap_map_eq_of_injective e.injective _