k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ toMatrix f = toMatrix g → f = g
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix
intro f g
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬toMatrix f = toMatrix g
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ toMatrix f = toMatrix g → f = g
refine' not_imp_not.1 _
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ∀ (x : m), ¬↑f x = ↑g x → ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬toMatrix f = toMatrix g
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ∀ (x : m), ¬↑f x = ↑g x → ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
intro i hi
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x, ¬(if x ∈ ↑f i then 1 else 0) = if x ∈ ↑g i then 1 else 0
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
use i
case none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ ↑g i then 1 else 0

case some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ ↑g i then 1 else 0
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x, ¬(if x ∈ ↑f i then 1 else 0) = if x ∈ ↑g i then 1 else 0
cases' hf : f i with fi
case none.none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0

case none.some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0
case none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ ↑g i then 1 else 0
cases' hg : g i with gi
case none.none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
case none.none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
rw [hf, hg] at hi
no goals
case none.none
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
exact (hi rfl).elim
case none.some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ¬(if gi ∈ none then 1 else 0) = if gi ∈ some gi then 1 else 0
case none.some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0
use gi
no goals
case none.some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ¬(if gi ∈ none then 1 else 0) = if gi ∈ some gi then 1 else 0
simp
case some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ¬(if fi ∈ some fi then 1 else 0) = if fi ∈ ↑g i then 1 else 0
case some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ ↑g i then 1 else 0
use fi
no goals
case some
k : Type ?u.21960
l : Type ?u.21963
m : Type u_2
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ¬(if fi ∈ some fi then 1 else 0) = if fi ∈ ↑g i then 1 else 0
simp [hf.symm, Ne.symm hi]