## Stream: new members

### Topic: Rewriting hypotheses in (d)ites

#### Yakov Pechersky (Oct 01 2020 at 02:36):

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 (Oct 01 2020 at 02:57):

Use split_ifs?

#### Yury G. Kudryashov (Oct 01 2020 at 02:58):

In this particular case: by simpa [eq_comm]

#### Yakov Pechersky (Oct 01 2020 at 02:58):

Ah eq_comm is what I was looking for

#### Yury G. Kudryashov (Oct 01 2020 at 03:00):

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

#### Yury G. Kudryashov (Oct 01 2020 at 03:01):

I don't remember details.

#### Yury G. Kudryashov (Oct 01 2020 at 03:01):

In case of an error, I just use split_ifs

#### Yury G. Kudryashov (Oct 01 2020 at 03:01):

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

#### Yakov Pechersky (Oct 01 2020 at 03:06):

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 (Oct 01 2020 at 03:07):

this is just the goal with the conditions reversed.

Almost.

#### Yakov Pechersky (Oct 01 2020 at 03:10):

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

Last updated: May 09 2021 at 18:17 UTC