Rewriting hypotheses in (d)ites

Stream: new members

[Yakov Pechersky]

What could be a short proof for this (and similar statements)?

lemma dif_symm {p q : Prop} {x y : ℕ} (h : dite (x = y) (λ _, p) (λ _, q)) :
  dite (y = x) (λ _, p) (λ _, q) := sorry

[Yury G. Kudryashov]

Use split_ifs?

[Yury G. Kudryashov]

In this particular case: by simpa [eq_comm]

[Yakov Pechersky]

Ah eq_comm is what I was looking for

[Yury G. Kudryashov]

There might be a problem if the types inside dite actually depend on the condition (or only for Type-values dites?)

[Yury G. Kudryashov]

I don't remember details.

[Yury G. Kudryashov]

In case of an error, I just use split_ifs

[Yury G. Kudryashov]

(or by_cases + simp [dif_pos ...])

[Yakov Pechersky]

The larger issue is that this is my goal after a wlog. I could for sure solve it without the wlog, but thought it'd be cleaner with.

      /-
R : Type u_1,
_inst_1 : field R,
n : ℕ,
A : matrix (fin (n + 3)) (fin (n + 3)) R,
x y : fin (n + 2 + 1),
H : y ≤ x,
this :
  dite (y = x) (λ (_x : y = x), 0)
      (λ (h : ¬y = x),
         -A 0 x * (-1) ^ ↑x * A 1 y * (-1) ^ ↑(x.pred_above y h) * det' ((A.drop 0 x).drop 0 (x.pred_above y h))) =
    dite (x = y) (λ (_x : x = y), 0)
      (λ (h : ¬x = y),
         A 1 y * (-1) ^ ↑y * A 0 x * (-1) ^ ↑(y.pred_above x h) * det' ((A.drop 0 y).drop 0 (y.pred_above x h)))
⊢ dite (x = y) (λ (_x : x = y), 0)
      (λ (h : ¬x = y),
         -A 0 y * (-1) ^ ↑y * A 1 x * (-1) ^ ↑(y.pred_above x h) * det' ((A.drop 0 y).drop 0 (y.pred_above x h))) =
    dite (y = x) (λ (_x : y = x), 0)
      (λ (h : ¬y = x),
         A 1 x * (-1) ^ ↑x * A 0 y * (-1) ^ ↑(x.pred_above y h) * det' ((A.drop 0 x).drop 0 (x.pred_above y h)))
-/

[Yakov Pechersky]

this is just the goal with the conditions reversed.

[Yakov Pechersky]

Almost.

[Yakov Pechersky]

I'll just go back to my wlog-free proof.