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.543558
M₆ : Type ?u.543561
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)) = ⊥
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.543558
M₆ : Type ?u.543561
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 : ℕ
⊢ Disjoint (tailing f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
rw [disjoint_iff]
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.543558
M₆ : Type ?u.543561
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 (tunnelAux f (tunnel' f i n)) (Submodule.snd R M N) ⊓
      Submodule.map (tunnelAux f (tunnel' f i (n + 0))) (Submodule.fst R M N) =
    ⊥
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.543558
M₆ : Type ?u.543561
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)) = ⊥
dsimp [tailing, tunnel, tunnel']
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.543558
M₆ : Type ?u.543561
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 (tunnelAux f (tunnel' f i n)) (Submodule.snd R M N) ⊓
      Submodule.map (tunnelAux f (tunnel' f i (n + 0))) (Submodule.fst R M N) =
    ⊥
erw [Submodule.map_inf_eq_map_inf_comap,
  Submodule.comap_map_eq_of_injective (tunnelAux_injective _ i _), inf_comm,
  Submodule.fst_inf_snd, Submodule.map_bot]