internlm/Lean-Github huggingface dataset:
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
⊢ s.pair c < (s + 1).pair e
Tactic:
have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
Proof state after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
this : c < e.unpair.2
⊢ s.pair c < (s + 1).pair e
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
this : c < e.unpair.2
⊢ s.pair c < (s + 1).pair e
Tactic:
exact lt_of_lt_of_le (Nat.pair_lt_pair_right s this) (Nat.pair_le_pair_of_le (Nat.le_succ s) (Nat.unpair_right_le e))
Proof state after:
no goals
Theorem: WType.SubWType.primrec_elimDecode_param
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
Tactic:
have : Primrec₂ (fun p ih => some $ elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih : σ × (ℕ × ℕ) → List (Option γ) → Option (Option γ)) :=
  option_some.comp (elimDecodeG_primrec β hf)
Proof state after:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
Theorem: WType.SubWType.primrec_elimDecode_param
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
Tactic:
exact nat_strong_rec'2 _ this (by simp[elimDecodeG_eq_elimDecode β])
Proof state after:
no goals
Theorem: WType.SubWType.primrec_elimDecode_param
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ ∀ (a : σ) (n m : ℕ),
    some
        (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) (a, n, m).1 (a, n, m).2
          (List.map (fun i => elimDecode β (fun a_1 ih => f a (a_1, ih)) i.unpair.1 i.unpair.2)
            (List.range (n.pair m)))) =
      some (elimDecode β (fun a_1 ih => f a (a_1, ih)) (n, m).1 (n, m).2)
Tactic:
simp[elimDecodeG_eq_elimDecode β]
Proof state after:
no goals
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof 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
Theorem: WType.SubWType.encode_eq_elim'
Proof 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⟩
Proof 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⟩
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof state after:
no goals
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof 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
Theorem: WType.SubWType.encode_eq_elim'
Proof 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⟩
Proof 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⟩
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof 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))
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof 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))
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof 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)
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof 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)
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof 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)
Theorem: WType.SubWType.encode_eq_elim'
Proof 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)]
Proof 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))
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof 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)
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof 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
Theorem: WType.SubWType.encode_eq_elim'
Proof 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
Proof 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))
Theorem: WType.SubWType.encode_eq_elim'
Proof 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]
Proof state after:
no goals
Theorem: WType.SubWType.encodeDecode_eq_elimDecode
Proof 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 : ℕ
⊢ encodeDecode (SubWType β s) e = elimDecode β (fun a l => encode (a, l)) s e
Tactic:
simp[elimDecode, encodeDecode_eq_encode_map_decode]
Proof 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 : ℕ
⊢ Option.map encode (decode e) =
    Option.map (elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s)
      (decode e)
Theorem: WType.SubWType.encodeDecode_eq_elimDecode
Proof 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 : ℕ
⊢ Option.map encode (decode e) =
    Option.map (elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s)
      (decode e)
Tactic:
rcases (decode e) <;> simp[encode_eq_elim']
Proof 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 : ℕ
val✝ : SubWType β s
⊢ elim' ℕ encode s val✝ =
    elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s val✝
Theorem: WType.SubWType.encodeDecode_eq_elimDecode
Proof 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 : ℕ
val✝ : SubWType β s
⊢ elim' ℕ encode s val✝ =
    elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s val✝
Tactic:
congr
Proof 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 : ℕ
val✝ : SubWType β s
⊢ encode = fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
Theorem: WType.SubWType.encodeDecode_eq_elimDecode
Proof 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 : ℕ
val✝ : SubWType β s
⊢ encode = fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
Tactic:
funext ⟨a, f⟩
Proof 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 : ℕ
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ encode ⟨a, f⟩ = (encode ⟨a, f⟩.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)))
Theorem: WType.SubWType.encodeDecode_eq_elimDecode
Proof 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 : ℕ
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ encode ⟨a, f⟩ = (encode ⟨a, f⟩.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)))
Tactic:
simp[encode_fintypeArrow, encode_finArrow]
Proof state after:
no goals
Theorem: WType.SubWType.depth_eq_elimDecode
Proof 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]
Proof 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)
Theorem: WType.SubWType.depth_eq_elimDecode
Proof 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]
Proof 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✝