Theorem: WType.SubWType.elimDecodeG_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 β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
s e : ℕ
⊢ WType.SubWType.elimDecodeG β f x (s, e)
      (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))) =
    elimDecode β (f x) s e
Tactic:
simp[elimDecode_eq_induction β (f x) s e, elimDecodeG]
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 : σ
s e : ℕ
⊢ Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM'
                  (fun c =>
                    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))).getI
                      (n.pair c))
                  (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
              fun l => if l.length = Fintype.card (β a) then some l else none))
      s =
    Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM' (elimDecode β (f x) n) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
              if l.length = Fintype.card (β a) then some l else none))
      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 β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
s e : ℕ
⊢ Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM'
                  (fun c =>
                    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))).getI
                      (n.pair c))
                  (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
              fun l => if l.length = Fintype.card (β a) then some l else none))
      s =
    Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM' (elimDecode β (f x) n) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
              if l.length = Fintype.card (β a) then some l else none))
      s
Tactic:
rcases s with (_ | s) <;> simp
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 β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
          if l.length = Fintype.card (β a) then some l else none)

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 β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
          if l.length = Fintype.card (β a) then some l else none)
Tactic:
congr
State after:
case succ.e_a
α : 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 : ℕ
⊢ (fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    fun a =>
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)

State before:
case succ.e_a
α : 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 : ℕ
⊢ (fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    fun a =>
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
funext a
State after:
case succ.e_a.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
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)

State before:
case succ.e_a.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
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
have :
  mapM' (fun c => ((List.range ((s + 1).pair e)).map $ fun i => elimDecode β (f x) i.unpair.fst i.unpair.snd).getI (s.pair c))
    (Denumerable.ofNat (List ℕ) e.unpair.2) =
  mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2) :=
List.mapM'_eq_mapM'_of_eq _ (by
{ intro c hc
  have : s.pair c < (s + 1).pair e := by
    have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
    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))
  simp[List.getI_map_range _ this] })
State after:
case succ.e_a.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
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
this :
  mapM'
      (fun c =>
        (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c))
      (Denumerable.ofNat (List ℕ) e.unpair.2) =
    mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)

State before:
case succ.e_a.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
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
this :
  mapM'
      (fun c =>
        (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c))
      (Denumerable.ofNat (List ℕ) e.unpair.2) =
    mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
rw[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 β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
⊢ ∀ a ∈ Denumerable.ofNat (List ℕ) e.unpair.2,
    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair a) =
      elimDecode β (f x) s a
Tactic:
intro c hc
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
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c

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
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Tactic:
have : s.pair c < (s + 1).pair e := by
  have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
  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))
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 : s.pair c < (s + 1).pair e
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c

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 : s.pair c < (s + 1).pair e
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Tactic:
simp[List.getI_map_range _ 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 β
σ : 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
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

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))
State after:
no goals