Theorem: Encodable.toFinArrowOpt_eq_none_iff (Logic/Vorspiel/Computability.lean)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ toFinArrowOpt f = none ↔ ∃ i, f i = none
Tactic:
simp[toFinArrowOpt, fintypeArrowEquivFinArrow]
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) ↔ ∃ i, f i = none

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) ↔ ∃ i, f i = none
Tactic:
constructor
State after:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none

State before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
{ rintro ⟨i, hi⟩; exact ⟨_, hi⟩ }
State after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none

State before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
{ rintro ⟨i, hi⟩; exact ⟨fintypeEquivFin i, by simp[hi]⟩  }
State after:
no goals

State before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none
Tactic:
rintro ⟨i, hi⟩
State after:
case mp.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : Fin (Fintype.card ι)
hi : f (fintypeEquivFin.symm i) = none
⊢ ∃ i, f i = none

State before:
case mp.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : Fin (Fintype.card ι)
hi : f (fintypeEquivFin.symm i) = none
⊢ ∃ i, f i = none
Tactic:
exact ⟨_, hi⟩
State after:
no goals

State before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
rintro ⟨i, hi⟩
State after:
case mpr.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ ∃ i, f (fintypeEquivFin.symm i) = none

State before:
case mpr.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
exact ⟨fintypeEquivFin i, by simp[hi]⟩
State after:
no goals

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ f (fintypeEquivFin.symm (fintypeEquivFin i)) = none
Tactic:
simp[hi]
State after:
no goals