Theorem: WType.SubWType.encode_mk (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
b : β a
⊢ (f b).depth ≤ s
Tactic:
simp[depth] at h
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
b : β a
h : ∀ (b : β a), (f b).depth ≤ s
⊢ (f b).depth ≤ s

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
b : β a
h : ∀ (b : β a), (f b).depth ≤ s
⊢ (f b).depth ≤ s
Tactic:
exact h b
State after:
no goals

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode (ofWType (WType.mk a f) (s + 1) h) = (encode a).pair (encode fun b => encode (ofWType (f b) s ⋯))
Tactic:
rw [Encodable.encode_ofEquiv equiv_succ, equiv_succ, ofWType, Equiv.coe_fn_mk, Encodable.encode_sigma_val, Nat.pair_eq_pair]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode a = encode a ∧ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode a = encode a ∧ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Tactic:
simp
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Tactic:
exact encode_fintypeArrow' (β a) (SubWType β s) _
State after:
no goals