Theorem: Matrix.get_set_ne_row (Algdata/Data/Matrix/Basic.lean)

State before:
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ get (set a i₁ j v) i₂ j = get a i₂ j
Tactic:
apply Array.get_set_ne a.entry
State after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i₁ j)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i₁ j v).entry) (Fin.lexFold i₂ j))

State before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i₁ j)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i₁ j v).entry) (Fin.lexFold i₂ j))
Tactic:
dsimp
State after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ¬↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)

State before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ¬↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
Tactic:
intro hcontra
State after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
⊢ False

State before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
⊢ False
Tactic:
have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
State after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
this : i₁ = i₂ ∧ j = j
⊢ False

State before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
this : i₁ = i₂ ∧ j = j
⊢ False
Tactic:
exact absurd this.left h
State after:
no goals