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

State before:
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
⊢ encodeDecode β = encodeDecode α
Tactic:
funext n
State after:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ encodeDecode β n = encodeDecode α n

State before:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ encodeDecode β n = encodeDecode α n
Tactic:
simp[encodeDecode, Encodable.decode_ofEquiv e]
State after:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ (encode (Option.map (⇑e.symm) (decode n))).predO = (encode (decode n)).predO

State before:
case h
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
⊢ (encode (Option.map (⇑e.symm) (decode n))).predO = (encode (decode n)).predO
Tactic:
rcases (decode n : Option α) with (_ | ⟨a⟩) <;> simp
State after:
case h.some
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
a : α
⊢ encode (e.symm a) = encode a

State before:
case h.some
α✝¹ : Type u_1
inst✝³ : Encodable α✝¹
α✝ : Type u_1
P : α✝ → Prop
inst✝² : Encodable α✝
inst✝¹ : DecidablePred P
α : Type u_2
inst✝ : Encodable α
β : Type u_3
e : β ≃ α
n : ℕ
a : α
⊢ encode (e.symm a) = encode a
Tactic:
simpa using Encodable.encode_ofEquiv e (e.symm a)
State after:
no goals