-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_injective [DecidableEq n] [MonoidWithZero α] [Nontrivial α] :
    Function.Injective (@toMatrix m n α _ _ _)

Proof state:
case h.some
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
use fi

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
rcases hf : f i with - | fi

Result:
case h.none
m : Type u_3
n : Type u_4
α : Type u_5
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 h.some
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
exact (hi rfl).elim

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
intro i hi

Result:
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
use i

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬f.toMatrix = g.toMatrix

Tactic:
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]

Result:
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
case h.none
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
rcases hg : g i with - | gi

Result:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
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 h.none.some
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix

Tactic:
intro f g

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ f.toMatrix = g.toMatrix → f = g

Proof state:
case h.none.some
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
use gi

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ f.toMatrix = g.toMatrix → f = g

Tactic:
refine not_imp_not.1 ?_

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬f.toMatrix = g.toMatrix

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
simp [hf.symm, Ne.symm hi]

Result:
no goals

Proof state:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
rw [hf, hg] at hi

Result:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
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

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
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

Tactic:
simp

Result:
no goals