case h.a
R : Type u_2
R₁ : Type ?u.1814068
R₂ : Type ?u.1814071
R₃ : Type ?u.1814074
R₄ : Type ?u.1814077
S : Type ?u.1814080
K : Type ?u.1814083
K₂ : Type ?u.1814086
M : Type u_1
M' : Type ?u.1814092
M₁ : Type ?u.1814095
M₂ : Type ?u.1814098
M₃ : Type ?u.1814101
M₄ : Type ?u.1814104
N : Type ?u.1814107
N₂ : Type ?u.1814110
ι : Type ?u.1814113
V : Type ?u.1814116
V₂ : Type ?u.1814119
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : Semiring R₄
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
x✝ : { x // x ∈ p }
⊢ ↑(↑(ofEq p p (_ : p = p)) x✝) = ↑(↑(refl R { x // x ∈ p }) x✝)
R : Type u_2
R₁ : Type ?u.1814068
R₂ : Type ?u.1814071
R₃ : Type ?u.1814074
R₄ : Type ?u.1814077
S : Type ?u.1814080
K : Type ?u.1814083
K₂ : Type ?u.1814086
M : Type u_1
M' : Type ?u.1814092
M₁ : Type ?u.1814095
M₂ : Type ?u.1814098
M₃ : Type ?u.1814101
M₄ : Type ?u.1814104
N : Type ?u.1814107
N₂ : Type ?u.1814110
ι : Type ?u.1814113
V : Type ?u.1814116
V₂ : Type ?u.1814119
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : Semiring R₄
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
⊢ ofEq p p (_ : p = p) = refl R { x // x ∈ p }
ext
no goals
case h.a
R : Type u_2
R₁ : Type ?u.1814068
R₂ : Type ?u.1814071
R₃ : Type ?u.1814074
R₄ : Type ?u.1814077
S : Type ?u.1814080
K : Type ?u.1814083
K₂ : Type ?u.1814086
M : Type u_1
M' : Type ?u.1814092
M₁ : Type ?u.1814095
M₂ : Type ?u.1814098
M₃ : Type ?u.1814101
M₄ : Type ?u.1814104
N : Type ?u.1814107
N₂ : Type ?u.1814110
ι : Type ?u.1814113
V : Type ?u.1814116
V₂ : Type ?u.1814119
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : Semiring R₄
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
x✝ : { x // x ∈ p }
⊢ ↑(↑(ofEq p p (_ : p = p)) x✝) = ↑(↑(refl R { x // x ∈ p }) x✝)
rfl