Theorem: WType.SubWType.encode_eq_elim' (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 : ℕ
⊢ ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
Tactic:
induction' s with s ih
State after:
case zero
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ ∀ (w : SubWType β 0), encode w = elim' ℕ encode 0 w

case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
⊢ ∀ (w : SubWType β (s + 1)), encode w = elim' ℕ encode (s + 1) w

State before:
case zero
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ ∀ (w : SubWType β 0), encode w = elim' ℕ encode 0 w
Tactic:
intro ⟨w, h⟩
State after:
case zero
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
w : WType β
h : w.depth ≤ 0
⊢ encode ⟨w, h⟩ = elim' ℕ encode 0 ⟨w, h⟩

State before:
case zero
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
w : WType β
h : w.depth ≤ 0
⊢ encode ⟨w, h⟩ = elim' ℕ encode 0 ⟨w, h⟩
Tactic:
simpa using lt_of_lt_of_le (depth_pos w) h
State after:
no goals

State before:
case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
⊢ ∀ (w : SubWType β (s + 1)), encode w = elim' ℕ encode (s + 1) w
Tactic:
letI : Primcodable { t : WType β // t.depth ≤ s } := Primcodable.SubWType (β := β) s
State after:
case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
⊢ ∀ (w : SubWType β (s + 1)), encode w = elim' ℕ encode (s + 1) w

State before:
case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
⊢ ∀ (w : SubWType β (s + 1)), encode w = elim' ℕ encode (s + 1) w
Tactic:
rintro ⟨⟨a, f⟩, hw⟩
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode ⟨WType.mk a f, hw⟩ = elim' ℕ encode (s + 1) ⟨WType.mk a f, hw⟩

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode ⟨WType.mk a f, hw⟩ = elim' ℕ encode (s + 1) ⟨WType.mk a f, hw⟩
Tactic:
simp only [primcodable_succ, ofEquiv_toEncodable, sigma_toEncodable_eq, elim', elim, encode_sigma_val]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode ⟨WType.mk a f, hw⟩ = (encode a).pair (encode fun b => elim ℕ encode (f b))

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode ⟨WType.mk a f, hw⟩ = (encode a).pair (encode fun b => elim ℕ encode (f b))
Tactic:
rw [Encodable.encode_ofEquiv equiv_succ]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (equiv_succ ⟨WType.mk a f, hw⟩) = (encode a).pair (encode fun b => elim ℕ encode (f b))

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (equiv_succ ⟨WType.mk a f, hw⟩) = (encode a).pair (encode fun b => elim ℕ encode (f b))
Tactic:
simp only [equiv_succ, Equiv.coe_fn_mk, encode_sigma_val, Nat.pair_eq_pair, true_and]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => elim ℕ encode (f b)

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => elim ℕ encode (f b)
Tactic:
rw [encode_fintypeArrow, encode_finArrow, encode_list]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (List.map encode (List.ofFn (fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩))) =
    encode fun b => elim ℕ encode (f b)

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (List.map encode (List.ofFn (fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩))) =
    encode fun b => elim ℕ encode (f b)
Tactic:
simp only [List.map_ofFn]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (List.ofFn (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩)) = encode fun b => elim ℕ encode (f b)

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (List.ofFn (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩)) = encode fun b => elim ℕ encode (f b)
Tactic:
rw[←encode_finArrow, encode_fintypeArrow (β a)]
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) =
    encode (fintypeArrowEquivFinArrow fun b => elim ℕ encode (f b))

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) =
    encode (fintypeArrowEquivFinArrow fun b => elim ℕ encode (f b))
Tactic:
simp
State after:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) = fintypeArrowEquivFinArrow fun b => elim ℕ encode (f b)

State before:
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) = fintypeArrowEquivFinArrow fun b => elim ℕ encode (f b)
Tactic:
funext i
State after:
case succ.mk.mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
i : Fin (Fintype.card (β a))
⊢ (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) i = fintypeArrowEquivFinArrow (fun b => elim ℕ encode (f b)) i

State before:
case succ.mk.mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
i : Fin (Fintype.card (β a))
⊢ (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) i = fintypeArrowEquivFinArrow (fun b => elim ℕ encode (f b)) i
Tactic:
simp
State after:
case succ.mk.mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
i : Fin (Fintype.card (β a))
⊢ encode ⟨f (fintypeEquivFin.symm i), ⋯⟩ = elim ℕ encode (f (fintypeEquivFin.symm i))

State before:
case succ.mk.mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
i : Fin (Fintype.card (β a))
⊢ encode ⟨f (fintypeEquivFin.symm i), ⋯⟩ = elim ℕ encode (f (fintypeEquivFin.symm i))
Tactic:
rw[ih]
State after:
no goals