Theorem: WType.SubWType.depth_eq_elimDecode (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 e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ Option.map (fun w => (↑w).depth) (decode e) = elimDecode β (fun a l => l.sup + 1) s e
Tactic:
simp[elimDecode, encodeDecode_eq_encode_map_decode]
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 e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ Option.map (fun w => (↑w).depth) (decode e) =
    Option.map (elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s) (decode e)

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 e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ Option.map (fun w => (↑w).depth) (decode e) =
    Option.map (elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s) (decode e)
Tactic:
rcases (decode e) <;> simp[this]
State after:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
⊢ elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s val✝ =
    elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s val✝

State before:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
⊢ elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s val✝ =
    elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s val✝
Tactic:
congr
State after:
case some.e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
⊢ (fun p => Finset.univ.sup p.snd + 1) = fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1

State before:
case some.e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
⊢ (fun p => Finset.univ.sup p.snd + 1) = fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1
Tactic:
funext ⟨a, f⟩
State after:
case some.e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ Finset.univ.sup ⟨a, f⟩.snd + 1 = (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)).sup + 1

State before:
case some.e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ Finset.univ.sup ⟨a, f⟩.snd + 1 = (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)).sup + 1
Tactic:
simp[List.sup_ofFn, fintypeArrowEquivFinArrow_eq]
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 e : ℕ
⊢ ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e : ℕ
⊢ ∀ (w : SubWType β 0), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ ∀ (w : SubWType β (s + 1)), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) (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 β
e : ℕ
⊢ ∀ (w : SubWType β 0), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e : ℕ
w : WType β
h : w.depth ≤ 0
⊢ (↑⟨w, h⟩).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e : ℕ
w : WType β
h : w.depth ≤ 0
⊢ (↑⟨w, h⟩).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ ∀ (w : SubWType β (s + 1)), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) (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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (↑⟨WType.mk a f, hw⟩).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) (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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (↑⟨WType.mk a f, hw⟩).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) (s + 1) ⟨WType.mk a f, hw⟩
Tactic:
simp[depth, ih, elim', elim]
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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (Finset.univ.sup fun n => (f n).depth) = Finset.univ.sup fun b => elim ℕ (fun p => Finset.univ.sup p.snd + 1) (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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ (Finset.univ.sup fun n => (f n).depth) = Finset.univ.sup fun b => elim ℕ (fun p => Finset.univ.sup p.snd + 1) (f b)
Tactic:
have : ∀ (b : β a), depth (f b) = elim ℕ (fun p => Finset.sup Finset.univ p.snd + 1) (f b) :=
  fun b => ih ⟨f b, by simp[depth, Nat.succ_eq_add_one] at hw; exact hw b⟩
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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
this : ∀ (b : β a), (f b).depth = elim ℕ (fun p => Finset.univ.sup p.snd + 1) (f b)
⊢ (Finset.univ.sup fun n => (f n).depth) = Finset.univ.sup fun b => elim ℕ (fun p => Finset.univ.sup p.snd + 1) (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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
this : ∀ (b : β a), (f b).depth = elim ℕ (fun p => Finset.univ.sup p.snd + 1) (f b)
⊢ (Finset.univ.sup fun n => (f n).depth) = Finset.univ.sup fun b => elim ℕ (fun p => Finset.univ.sup p.snd + 1) (f b)
Tactic:
simp[this]
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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
b : β a
⊢ (f b).depth ≤ s
Tactic:
simp[depth, Nat.succ_eq_add_one] at hw
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
b : β a
hw : ∀ (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 β
e s : ℕ
ih : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
a : α
f : β a → WType β
b : β a
hw : ∀ (b : β a), (f b).depth ≤ s
⊢ (f b).depth ≤ s
Tactic:
exact hw b
State after:
no goals