Theorem: List.modifyNth_comm_of_comm (One.lean)

State before:
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
cases heq: decide (i = j) with
| true =>
  simp only [decide_eq_true_eq] at heq
  rw [List.modifyNth_modifyNth_eq heq, List.modifyNth_modifyNth_eq (Eq.symm heq), P.comp_eq, heq]
| false =>
  simp only [decide_eq_false_iff_not] at heq
  have heq₂ : j ≠ i := by simp only [ne_eq, ne_comm, heq, not_false_iff]
  rw [List.modifyNth_modifyNth_ne heq, List.modifyNth_modifyNth_ne heq₂]
State after:
no goals

State before:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : decide (i = j) = true
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [decide_eq_true_eq] at heq
State after:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)

State before:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [List.modifyNth_modifyNth_eq heq, List.modifyNth_modifyNth_eq (Eq.symm heq), P.comp_eq, heq]
State after:
no goals

State before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : decide (i = j) = false
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [decide_eq_false_iff_not] at heq
State after:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)

State before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
have heq₂ : j ≠ i := by simp only [ne_eq, ne_comm, heq, not_false_iff]
State after:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
heq₂ : j ≠ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)

State before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
heq₂ : j ≠ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [List.modifyNth_modifyNth_ne heq, List.modifyNth_modifyNth_ne heq₂]
State after:
no goals

State before:
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ j ≠ i
Tactic:
simp only [ne_eq, ne_comm, heq, not_false_iff]
State after:
no goals