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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ toFinArrowOpt f = some g ↔ ∀ (i : ι), f i = some (g i)
Tactic:
simp[toFinArrowOpt, fintypeArrowEquivFinArrow]
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) ↔
    ∀ (i : ι), f i = some (g i)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) ↔
    ∀ (i : ι), f i = some (g i)
Tactic:
constructor
State after:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g

State before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
{ rintro ⟨a, ha, rfl⟩; simp; intro i
  simpa using ha (fintypeEquivFin i) }
State after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g

State before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
{ intro hf; exact ⟨fun i => g (fintypeEquivFin.symm i), by { simp[hf]; funext i; simp }⟩ }
State after:
no goals

State before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)
Tactic:
rintro ⟨a, ha, rfl⟩
State after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a i)

State before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a i)
Tactic:
simp
State after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some (a (fintypeEquivFin i))

State before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some (a (fintypeEquivFin i))
Tactic:
intro i
State after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
i : ι
⊢ f i = some (a (fintypeEquivFin i))

State before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
i : ι
⊢ f i = some (a (fintypeEquivFin i))
Tactic:
simpa using ha (fintypeEquivFin i)
State after:
no goals

State before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
intro hf
State after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ∃ a,
    (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
      (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g

State before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ∃ a,
    (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
      (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
exact ⟨fun i => g (fintypeEquivFin.symm i), by { simp[hf]; funext i; simp }⟩
State after:
no goals

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some ((fun i => g (fintypeEquivFin.symm i)) i)) ∧
    ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g
Tactic:
simp[hf]
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g
Tactic:
funext i
State after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
i : ι
⊢ (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) (fun i => g (fintypeEquivFin.symm i)) i = g i

State before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
i : ι
⊢ (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) (fun i => g (fintypeEquivFin.symm i)) i = g i
Tactic:
simp
State after:
no goals