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

State before:
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ ¬↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)

State before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
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 : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
this : i = i ∧ j₁ = j₂
⊢ False
Tactic:
exact absurd this.right h
State after:
no goals