case zero
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.572984
M₆ : Type ?u.572987
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
⊢ Disjoint (tailings f i Nat.zero) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.zero + 1)))

case succ
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i (Nat.succ n)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ 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.572984
M₆ : Type ?u.572987
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 (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
induction' n with n ih
case zero
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.572984
M₆ : Type ?u.572987
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
⊢ Disjoint (tailings f i Nat.zero) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.zero + 1)))
case zero
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.572984
M₆ : Type ?u.572987
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
⊢ Disjoint (tailings f i Nat.zero) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.zero + 1)))
simp only [tailings_zero]
no goals
case zero
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.572984
M₆ : Type ?u.572987
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
⊢ Disjoint (tailings f i Nat.zero) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.zero + 1)))
apply tailing_disjoint_tunnel_succ
case succ
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n ⊔ tailing f i (n + 1)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
case succ
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i (Nat.succ n)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
simp only [tailings_succ]
case succ.refine'_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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailing f i (n + 1)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))

case succ.refine'_2
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n) (tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
case succ
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n ⊔ tailing f i (n + 1)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
refine' Disjoint.disjoint_sup_left_of_disjoint_sup_right _ _
case succ.refine'_2
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n) (tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
case succ.refine'_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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailing f i (n + 1)) (↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))

case succ.refine'_2
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n) (tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
apply tailing_disjoint_tunnel_succ
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)) ≤ ↑OrderDual.ofDual (↑(tunnel f i) (n + 1))
case succ.refine'_2
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ Disjoint (tailings f i n) (tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)))
apply Disjoint.mono_right _ ih
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.572984
M₆ : Type ?u.572987
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 : ℕ
ih : Disjoint (tailings f i n) (↑OrderDual.ofDual (↑(tunnel f i) (n + 1)))
⊢ tailing f i (n + 1) ⊔ ↑OrderDual.ofDual (↑(tunnel f i) (Nat.succ n + 1)) ≤ ↑OrderDual.ofDual (↑(tunnel f i) (n + 1))
apply tailing_sup_tunnel_succ_le_tunnel