R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.551452
M₆ : Type ?u.551455
inst✝⁴ : Ring R
N : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
⊢ Submodule.map (comp (comp (Submodule.subtype (tunnel' f i n).fst) ↑(LinearEquiv.symm (tunnel' f i n).snd)) f)
        (Submodule.snd R M N) ⊔
      Submodule.map
        (comp (comp (Submodule.subtype (tunnel' f i (n + 0)).fst) ↑(LinearEquiv.symm (tunnel' f i (n + 0)).snd)) f)
        (Submodule.fst R M N) ≤
    (tunnel' f i n).fst
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.551452
M₆ : Type ?u.551455
inst✝⁴ : Ring R
N : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
⊢ tailing f i n ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (n + 1)) ≤ ↑OrderDual.ofDual (↑(tunnel f i) n)
dsimp [tailing, tunnel, tunnel', tunnelAux]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.551452
M₆ : Type ?u.551455
inst✝⁴ : Ring R
N : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
⊢ Submodule.map (Submodule.subtype (tunnel' f i n).fst)
      (Submodule.map (↑(LinearEquiv.symm (tunnel' f i n).snd)) (Submodule.map f ⊤)) ≤
    (tunnel' f i n).fst
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.551452
M₆ : Type ?u.551455
inst✝⁴ : Ring R
N : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
⊢ Submodule.map (comp (comp (Submodule.subtype (tunnel' f i n).fst) ↑(LinearEquiv.symm (tunnel' f i n).snd)) f)
        (Submodule.snd R M N) ⊔
      Submodule.map
        (comp (comp (Submodule.subtype (tunnel' f i (n + 0)).fst) ↑(LinearEquiv.symm (tunnel' f i (n + 0)).snd)) f)
        (Submodule.fst R M N) ≤
    (tunnel' f i n).fst
erw [← Submodule.map_sup, sup_comm, Submodule.fst_sup_snd, Submodule.map_comp, Submodule.map_comp]
no goals
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.551452
M₆ : Type ?u.551455
inst✝⁴ : Ring R
N : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M × N →ₗ[R] M
i : Injective ↑f
n : ℕ
⊢ Submodule.map (Submodule.subtype (tunnel' f i n).fst)
      (Submodule.map (↑(LinearEquiv.symm (tunnel' f i n).snd)) (Submodule.map f ⊤)) ≤
    (tunnel' f i n).fst
apply Submodule.map_subtype_le