## Stream: new members

### Topic: linarith on coerced fins

#### Yakov Pechersky (Sep 16 2020 at 20:17):

Is there a way to get linarith to simplify this proof at all? It is just dealing with a lot of inequalities.

import data.matrix.notation
import tactic.wlog
import tactic.linarith

variables {n : }

lemma nat.sub_add_one (hpos : 0 < n) : n - 1 + 1 = n :=
begin
cases n,
{ exact absurd hpos (lt_irrefl 0) },
simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero],
end

lemma nat.not_lt_pred_ge {m n : } (h : m < n - 1) (H : n  m) : false :=
begin
have hn : n < n - 1 := lt_of_le_of_lt H h,
cases n,
{ rw [nat.nat_zero_eq_zero, nat.zero_sub] at hn,
exact absurd hn (lt_irrefl 0) },
{ rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at hn,
exact nat.not_succ_lt_self hn },
end

example (x y : fin (n + 2)) (j : fin n) (h : y  x) :
x.succ_above ((x.pred_above y h).succ_above j) = y.succ_above ((y.pred_above x (ne.symm h)).succ_above j) :=
begin
wlog H : y < x using [x y],
{ rcases lt_trichotomy x y with H|rfl|H,
{ exact or.inr H },
{ exact or.inl H } },
unfold fin.pred_above,
rw [dif_pos H, dif_neg (not_lt_of_lt H)],
have H' := fin.lt_iff_coe_lt_coe.mp H,
have posx : 0 < x.val := lt_of_le_of_lt (fin.zero_le y) y < x,
unfold fin.succ_above,
all_goals { simp_rw [fin.lt_iff_coe_lt_coe] at * },
split_ifs,
any_goals { refl <|> rw fin.cast_succ_fin_succ },
all_goals {
simp only [fin.val_eq_coe, fin.coe_cast_lt,
fin.coe_succ, fin.coe_cast_succ, fin.coe_pred,
not_lt, ne.def, fin.cast_succ_inj] at * },
{ have hj : (x : ) - 1 = j :=
le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
rw hj at *,
exact absurd (y : ) < x (not_lt_of_lt (x : ) < y) },
{ have hj : (x : ) - 1 = j :=
le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
rw hj at *,
have hy : y = x :=
le_antisymm (y : )  x (nat.le_of_pred_lt (x : ) - 1 < y),
exact absurd hy h },
{ exact absurd (x : )  j (nat.not_lt_pred_ge (j : ) < x - 1) },
{ have hy : (y : ) = j + 1 :=
le_antisymm (y : )  j + 1 (j : ) < y,
have : (j : ) < x,
{ refine lt_trans (nat.lt_succ_self j) _,
convert fin.lt_iff_coe_lt_coe.mp H,
rw hy },
exact absurd (j : ) < x (not_lt_of_ge (x : )  j) },
{ have : (x : )  j + 1 :=
nat.le_add_of_sub_le_right (x : ) - 1  j,
exact absurd (j : ) + 1 < x (not_lt_of_ge (x : )  j + 1) },
{ have : (j : ) + 1 < x :=
nat.add_lt_of_lt_sub_right (j : ) < x - 1,
exact absurd (j : ) + 1 < x (not_lt_of_ge (x : )  j + 1) },
{ have : (j : ) < y :=
lt_trans (nat.lt_succ_self j) (j : ) + 1 < y,
exact absurd (j : ) < y (not_lt_of_ge (y : )  j) },
end

#### Yakov Pechersky (Sep 16 2020 at 20:17):

For reference, here is a (not fully-golfed) proof that does not use split_ifs:

import data.matrix.notation
import tactic.wlog
import tactic.linarith

variables {n : }

lemma nat.sub_add_one (hpos : 0 < n) : n - 1 + 1 = n :=
begin
cases n,
{ exact absurd hpos (lt_irrefl 0) },
simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero],
end

lemma nat.not_lt_pred_ge {m n : } (h : m < n - 1) (H : n  m) : false :=
begin
have hn : n < n - 1 := lt_of_le_of_lt H h,
cases n,
{ rw [nat.nat_zero_eq_zero, nat.zero_sub] at hn,
exact absurd hn (lt_irrefl 0) },
{ rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at hn,
exact nat.not_succ_lt_self hn },
end

example (x y : fin (n + 2)) (j : fin n) (h : y  x) :
x.succ_above ((x.pred_above y h).succ_above j) = y.succ_above ((y.pred_above x (ne.symm h)).succ_above j) :=
begin
wlog H : y < x using [x y],
{ rcases lt_trichotomy x y with H|rfl|H,
{ exact or.inr H },
{ exact or.inl H } },
unfold fin.pred_above,
rw [dif_pos H, dif_neg (not_lt_of_lt H)],
have lessy : y.val < n + 1 := lt_of_lt_of_le y < x (fin.le_last x),
have posx : 0 < x.val := lt_of_le_of_lt (fin.zero_le y) y < x,
have hx : x  0 := ne_of_gt posx,
cases fin.succ_above_lt_ge y j.succ with Hyj Hyj,
{ have hyj : j.cast_succ < y.cast_lt lessy,
{ rw fin.lt_iff_coe_lt_coe at Hyj ,
refine lt_trans _ Hyj,
fin.coe_succ, fin.coe_cast_succ] },
rw fin.succ_above_below _ _ hyj,
cases fin.succ_above_lt_ge (x.pred hx) j with hxj hxj,
{ rw fin.succ_above_below _ _ hxj,
rw fin.succ_above_below,
rw fin.succ_above_below,
{ exact hyj },
{ rw fin.lt_iff_coe_lt_coe,
refine lt_trans hxj _,
rw [fin.val_eq_coe, fin.coe_pred],
exact nat.pred_lt (ne_of_gt posx) } },
{ cases eq_or_lt_of_le hxj with Hxj Hxj,
{ rw [fin.cast_succ_fin_succ, Hxj, fin.succ_pred] at Hyj,
exact absurd H (not_lt_of_lt Hyj) },
{ rw fin.succ_above_above _ _ hxj,
rw fin.succ_above_above x,
rw fin.succ_above_below y _ Hyj,
{ rw fin.cast_succ_fin_succ },
{ rw fin.le_iff_coe_le_coe,
rw [fin.coe_cast_succ],
refine nat.le_of_pred_lt _,
convert Hxj,
simpa only [fin.val_eq_coe, fin.coe_pred] } } } },
{ rcases eq_or_lt_of_le Hyj with hyj|hyj,
{ simp_rw [hyj, fin.cast_lt_cast_succ],
rw fin.succ_above_below _ _ (fin.cast_succ_lt_succ j),
rw fin.succ_above_below x,
rw fin.succ_above_below (x.pred hx),
rw fin.cast_succ_fin_succ,
rw fin.succ_above_below _ _ (fin.cast_succ_lt_succ j.cast_succ),
{ rw fin.lt_iff_coe_lt_coe,
rw [fin.coe_cast_succ, fin.coe_pred],
refine nat.le_pred_of_lt _,
convert y < x,
simp only [hyj, fin.val_eq_coe, fin.coe_succ, fin.coe_cast_succ] },
{ refine lt_trans _ y < x,
rw [hyj, fin.cast_succ_fin_succ],
exact fin.cast_succ_lt_succ _ } },
{ replace Hyj : y  j.cast_succ.cast_succ,
{ rw fin.lt_iff_coe_lt_coe at hyj,
rw [fin.coe_cast_succ, fin.coe_succ] at hyj,
exact nat.lt_succ_iff.mp hyj },
have hyj' : y.cast_lt lessy  j.cast_succ,
{ rw fin.le_iff_coe_le_coe at Hyj ,
refine le_trans Hyj _,
rw fin.coe_cast_succ },
rw fin.succ_above_above _ _ hyj',
cases fin.succ_above_lt_ge (x.pred hx) j with hxj hxj,
{ rw fin.succ_above_below _ _ hxj,
rw fin.succ_above_above y _,
rw fin.succ_above_below,
{ rw fin.cast_succ_fin_succ },
{ rw fin.lt_iff_coe_lt_coe,
rw [fin.coe_cast_succ, fin.coe_succ],
convert hxj,
rw [fin.val_eq_coe, fin.coe_pred] },
{ rw fin.le_iff_coe_le_coe,
exact hyj' } },
{ rw fin.succ_above_above _ _ hxj,
rw fin.succ_above_above x,
rw fin.succ_above_above y _ (le_of_lt hyj),
rw [fin.le_iff_coe_le_coe, fin.coe_cast_succ, fin.coe_succ],
convert hxj,
rw [fin.val_eq_coe, fin.coe_pred] } } }
end

#### Reid Barton (Sep 16 2020 at 20:23):

I guess this is what omega is supposed to be for

#### Yakov Pechersky (Sep 16 2020 at 20:28):

omega didn't work, even for the seemingly simple

{ have hj : (x : ) - 1 = j :=
le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
rw hj at *,