case refine'_1
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x) → ∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x

case refine'_2
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x) → ∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
⊢ x ∈ submoduleImage ϕ N ↔ ∃ y yO x_1, ↑ϕ { val := y, property := yO } = x
refine' Submodule.mem_map.trans ⟨_, _⟩ <;> simp_rw [Submodule.mem_comap]
case refine'_1.intro.mk.intro
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ↑ϕ { val := y, property := yO } = x
⊢ ∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x
case refine'_1
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x) → ∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x
rintro ⟨⟨y, yO⟩, yN : y ∈ N, h⟩
no goals
case refine'_1.intro.mk.intro
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ↑ϕ { val := y, property := yO } = x
⊢ ∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x
exact ⟨y, yO, yN, h⟩
case refine'_2.intro.intro.intro
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ↑ϕ { val := y, property := (_ : y ∈ O) } = x
⊢ ∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x
case refine'_2
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y h h_1, ↑ϕ { val := y, property := (_ : y ∈ O) } = x) → ∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x
rintro ⟨y, yO, yN, h⟩
no goals
case refine'_2.intro.intro.intro
R : Type u_2
R₁ : Type ?u.1587077
R₂ : Type ?u.1587080
R₃ : Type ?u.1587083
R₄ : Type ?u.1587086
S : Type ?u.1587089
K : Type ?u.1587092
K₂ : Type ?u.1587095
M : Type u_3
M'✝ : Type ?u.1587101
M₁ : Type ?u.1587104
M₂ : Type ?u.1587107
M₃ : Type ?u.1587110
M₄ : Type ?u.1587113
N✝ : Type ?u.1587116
N₂ : Type ?u.1587119
ι : Type ?u.1587122
V : Type ?u.1587125
V₂ : Type ?u.1587128
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ↑ϕ { val := y, property := (_ : y ∈ O) } = x
⊢ ∃ y, ↑(Submodule.subtype O) y ∈ N ∧ ↑ϕ y = x
exact ⟨⟨y, yO⟩, yN, h⟩