internlm/Lean-Github huggingface dataset:
Theorem: WType.SubWType.depth_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 : ℕ
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
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 : ℕ
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
Theorem: WType.SubWType.depth_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 : ℕ
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⟩
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 : ℕ
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
Theorem: WType.SubWType.depth_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 : ℕ
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]
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 : ℕ
⊢ ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
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
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
e : ℕ
⊢ ∀ (w : SubWType β 0), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 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 β
e : ℕ
w : WType β
h : w.depth ≤ 0
⊢ (↑⟨w, h⟩).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) 0 ⟨w, h⟩
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
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
Proof state after:
no goals
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
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⟩
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 β
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⟩
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
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]
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 β
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)
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
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⟩
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 β
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)
Theorem: WType.SubWType.depth_eq_elimDecode
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 β
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]
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 β
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
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 β
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
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 β
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
Proof state after:
no goals
Theorem: WType.SubWType.depth_decode_primrec
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 β
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
Tactic:
have : Primrec₂ (elimDecode β (fun a l => l.sup + 1)) :=
  primrec_elimDecode β (by simp only [← Nat.succ_eq_add_one]; apply Primrec.succ.comp $ (list_sup nat_max).comp snd)
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 β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
Theorem: WType.SubWType.depth_decode_primrec
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 β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
Tactic:
exact this.of_eq (by simp[depth_eq_elimDecode])
Proof state after:
no goals
Theorem: WType.SubWType.depth_decode_primrec
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 β
⊢ Primrec₂ fun a l => l.sup + 1
Tactic:
simp only [← Nat.succ_eq_add_one]
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 β
⊢ Primrec₂ fun a l => l.sup.succ
Theorem: WType.SubWType.depth_decode_primrec
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 β
⊢ Primrec₂ fun a l => l.sup.succ
Tactic:
apply Primrec.succ.comp $ (list_sup nat_max).comp snd
Proof state after:
no goals
Theorem: WType.SubWType.depth_decode_primrec
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 β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ ∀ (a b : ℕ), elimDecode β (fun a l => l.sup + 1) a b = Option.map (fun w => (↑w).depth) (decode b)
Tactic:
simp[depth_eq_elimDecode]
Proof state after:
no goals
Theorem: WType.encode_decode_eq
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 β
e : ℕ
⊢ (Option.casesOn (Option.map SubWType.toW (decode e)) 0 fun w => encode (SubWType.ofW w) + 1) =
    encode
      ((encodeDecode (SubWType β e.unpair.1) e.unpair.2).bind fun c =>
        Option.map (fun d => d.pair c) (Option.map (fun w => (↑w).depth) (decode c)))
Tactic:
simp[Function.comp, 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 β
e : ℕ
⊢ Option.rec 0 (fun val => encode (SubWType.ofW val) + 1)
      (Option.map (fun x => SubWType.toW ⟨e.unpair.1, x⟩) (decode e.unpair.2)) =
    encode ((Option.map encode (decode e.unpair.2)).bind fun a => Option.map (fun x => (↑x).depth.pair a) (decode a))
Theorem: WType.encode_decode_eq
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 β
e : ℕ
⊢ Option.rec 0 (fun val => encode (SubWType.ofW val) + 1)
      (Option.map (fun x => SubWType.toW ⟨e.unpair.1, x⟩) (decode e.unpair.2)) =
    encode ((Option.map encode (decode e.unpair.2)).bind fun a => Option.map (fun x => (↑x).depth.pair a) (decode a))
Tactic:
rcases (decode e.unpair.2) with (_ | w) <;> simp[SubWType.toW, SubWType.ofW]
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 β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
Theorem: WType.encode_decode_eq
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 β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
Tactic:
{ simp[SubWType.encode_eq_elim']; apply SubWType.elim_const; simp }
Proof state after:
no goals
Theorem: WType.encode_decode_eq
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 β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
Tactic:
simp[SubWType.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 β
e : ℕ
w : SubWType β e.unpair.1
⊢ SubWType.elim' ℕ encode (↑w).depth (SubWType.ofWType (↑w) (↑w).depth ⋯) = SubWType.elim' ℕ encode e.unpair.1 w
Theorem: WType.encode_decode_eq
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 β
e : ℕ
w : SubWType β e.unpair.1
⊢ SubWType.elim' ℕ encode (↑w).depth (SubWType.ofWType (↑w) (↑w).depth ⋯) = SubWType.elim' ℕ encode e.unpair.1 w
Tactic:
apply SubWType.elim_const
Proof state after:
case some.h
α : 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 β e.unpair.1
⊢ ↑(SubWType.ofWType (↑w) (↑w).depth ⋯) = ↑w
Theorem: WType.encode_decode_eq
Proof state before:
case some.h
α : 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 β e.unpair.1
⊢ ↑(SubWType.ofWType (↑w) (↑w).depth ⋯) = ↑w
Tactic:
simp
Proof state after:
no goals
Theorem: WType.elimL_mk
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
f : α → List γ → γ
a : α
v : β a → WType β
⊢ elimL f (mk a v) = f a (List.ofFn (fintypeArrowEquivFinArrow fun b => elimL f (v b)))
Tactic:
simp[elimL, elim]
Proof state after:
no goals
Theorem: WType.elim_eq_elimL
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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elimL (fun a l => f ⟨a, fintypeArrowEquivFinArrow.symm fun i => l.getI ↑i⟩) w
Tactic:
simp[elimL]
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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elim γ (fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩) w
Theorem: WType.elim_eq_elimL
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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elim γ (fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩) w
Tactic:
congr
Proof state after:
case e_fγ
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ f = fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩
Theorem: WType.elim_eq_elimL
Proof state before:
case e_fγ
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ f = fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩
Tactic:
funext ⟨a, j⟩
Proof state after:
case 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 β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨⟨a, j⟩.fst, fintypeArrowEquivFinArrow.symm fun i => ⟨a, j⟩.snd (fintypeEquivFin.symm i)⟩
Theorem: WType.elim_eq_elimL
Proof state before:
case 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 β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨⟨a, j⟩.fst, fintypeArrowEquivFinArrow.symm fun i => ⟨a, j⟩.snd (fintypeEquivFin.symm i)⟩
Tactic:
simp
Proof state after:
case 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 β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨a, fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)⟩
Theorem: WType.elim_eq_elimL
Proof state before:
case 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 β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨a, fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)⟩
Tactic:
congr
Proof state after:
case e_fγ.h.e_a.e_snd
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ j = fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)
Theorem: WType.elim_eq_elimL
Proof state before:
case e_fγ.h.e_a.e_snd
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ j = fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)
Tactic:
funext b
Proof state after:
case e_fγ.h.e_a.e_snd.h
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
b : β a
⊢ j b = fintypeArrowEquivFinArrow.symm (fun i => j (fintypeEquivFin.symm i)) b
Theorem: WType.elim_eq_elimL
Proof state before:
case e_fγ.h.e_a.e_snd.h
α : 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
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
b : β a
⊢ j b = fintypeArrowEquivFinArrow.symm (fun i => j (fintypeEquivFin.symm i)) b
Tactic:
simp
Proof state after:
no goals
Theorem: WType.decode_elimL_eq
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
e : ℕ
f : α → List γ → γ
⊢ Option.map (elimL f) (decode e) = SubWType.elimDecode β f e.unpair.1 e.unpair.2
Tactic:
unfold elimL
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
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (elim γ fun x =>
        match x with
        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
      (decode e) =
    SubWType.elimDecode β f e.unpair.1 e.unpair.2