Theorem: FinDenumerable.decode_fin_inj (FormalSystems/Preliminaries/FinDenumerable.lean)

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
⊢ a = b ↔ n = m
Tactic:
have ⟨ _, p₁ ⟩ := fin_preimage_exists n
State after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
⊢ a = b ↔ n = m

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
⊢ a = b ↔ n = m
Tactic:
simp [FinDenumerable.decode_fin, <- p₁] at h₁
State after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
h₁ : a = w✝
⊢ a = b ↔ n = m

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
h₁ : a = w✝
⊢ a = b ↔ n = m
Tactic:
have ⟨ _, p₂ ⟩ := fin_preimage_exists m
State after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
⊢ a = b ↔ n = m

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
⊢ a = b ↔ n = m
Tactic:
simp [FinDenumerable.decode_fin, <- p₂] at h₂
State after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ a = b ↔ n = m

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ a = b ↔ n = m
Tactic:
rw [h₁, h₂, Fin.ext_iff, ← p₁, ← p₂]
State after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ w✝¹ = w✝ ↔ Encodable.encode w✝¹ = Encodable.encode w✝

State before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ w✝¹ = w✝ ↔ Encodable.encode w✝¹ = Encodable.encode w✝
Tactic:
apply Iff.symm
State after:
case h
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ Encodable.encode w✝¹ = Encodable.encode w✝ ↔ w✝¹ = w✝

State before:
case h
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ Encodable.encode w✝¹ = Encodable.encode w✝ ↔ w✝¹ = w✝
Tactic:
apply Encodable.encode_inj
State after:
no goals