Trivial ite lemma

Stream: Is there code for X?

[Moritz Doll]

How do I prove this?

example {R₁ : Type u_2} {n : Type u_6}
  [comm_semiring R₁]
  [fintype n]
  [decidable_eq n]
  (i i' : n) :
  ite (i' = i) 1 0 = ite (i = i') 1 0 :=
begin
  sorry,
end

[Eric Rodriguez]

if_congr should be helpful, you could also just do congr', even simp could make progress

[Patrick Massot]

split_ifs ; tauto,

[Patrick Massot]

or congr' 1, simp

[Eric Wieser]

Does rw eq_comm work?

[Moritz Doll]

@Eric Wieser no it rewrites the equality itself

[Eric Wieser]

@eq_comm n?

[Moritz Doll]

thanks everyone, I used Patrick's first suggestion now

[Moritz Doll]

Eric: rewrite tactic failed, motive is not type correct
λ (_a : Prop), ite (i' = i) 1 0 = ite (i = i') 1 0 = (ite _a 1 0 = ite (i = i') 1 0)

[Moritz Doll]

@Eric Rodriguez simp didn't help, which surprised me

[Moritz Doll]

congr was doing crazy things and I forgot that there is congr'

[Moritz Doll]

Follow-up question: which of these lemmas (if any) should be in mathlib?

@[simp] lemma std_basis_apply' (i i' : n) : (std_basis R₁ (λ (_x : n), R₁) i) 1 i' =
  ite (i = i') 1 0  :=
begin
  rw [linear_map.std_basis_apply, function.update_apply, pi.zero_apply],
  split_ifs;
  tauto,
end

@[simp] lemma ring_hom_ite_zero_one (p : Prop) [decidable p] : σ₁ (ite p 0 1) = ite p 0 1 :=
by { split_ifs; simp [h] }

@[simp] lemma ring_hom_ite_one_zero (p : Prop) [decidable p] : σ₁ (ite p 1 0) = ite p 1 0 :=
by { split_ifs; simp [h] }

[Moritz Doll]

σ₁ is obviously a ring_hom

[Patrick Massot]

My second suggestion was morally more correct (closer to what you tried with rw)

[Moritz Doll]

but it was less Lean-correct. congr' 1, rw [eq_iff_iff], exact eq_commworks though

[Moritz Doll]

or better congr' 1, rw [eq_iff_iff, eq_comm]

[Damiano Testa]

Eric's suggestion can be made to work, but Lean resists: simp_rw (@eq_comm n i _).

[FR]

What about simp_rw eq_comm or simp only [eq_comm]?

[Jake Levinson]

Eric Rodriguez said:

if_congr should be helpful, you could also just do congr', even simp could make progress

This works for me, a one line proof is exact if_congr eq_comm rfl rfl