internlm/Lean-Github huggingface dataset:
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
have lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1 :=
  lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at has))
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
have lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2 :=
  lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at hbs))
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
simpa using lt_trans (Nat.pair_lt_pair_left e.unpair.2.pred.unpair.2 lt₁) (Nat.pair_lt_pair_right e.unpair.1 lt₂)
Proof state after:
no goals
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
eq : e.unpair.1 = 0
⊢ False
Tactic:
simp[eq] at has
Proof state after:
no goals
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
eq : e.unpair.2 = 0
⊢ False
Tactic:
simp[eq] at hbs
Proof state after:
no goals
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = Option.map (fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2) (decode e)
Tactic:
simp only [Option.map_eq_bind]
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = (decode e).bind (some ∘ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2)
Theorem: Primrec.list_zipWith_param
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = (decode e).bind (some ∘ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2)
Tactic:
rfl
Proof state after:
no goals
Theorem: Primrec.nat_predO
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
⊢ ∀ (n : ℕ), (Nat.casesOn n none fun a => some (id a)) = n.predO
Tactic:
intro n
Proof state after:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn n none fun a => some (id a)) = n.predO
Theorem: Primrec.nat_predO
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn n none fun a => some (id a)) = n.predO
Tactic:
cases n <;> simp
Proof state after:
no goals
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
⊢ Primrec List.sup
Tactic:
have e : ∀ l : List α, l.sup = l.foldr Sup.sup ⊥ := by
  intro l; induction' l with a as ih <;> simp[sup_eq_max, *]
Proof state after:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Tactic:
have : Primrec (fun l => l.foldr Sup.sup ⊥ : List α → α) :=
  list_foldr Primrec.id (const _) (hsup.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right))
Proof state after:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ Primrec List.sup
Tactic:
exact this.of_eq (by simp[e])
Proof state after:
no goals
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
⊢ ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
Tactic:
intro l
Proof state after:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
l : List α
⊢ l.sup = List.foldr Sup.sup ⊥ l
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
l : List α
⊢ l.sup = List.foldr Sup.sup ⊥ l
Tactic:
induction' l with a as ih <;> simp[sup_eq_max, *]
Proof state after:
no goals
Theorem: Primrec.list_sup
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ ∀ (n : List α), List.foldr Sup.sup ⊥ n = n.sup
Tactic:
simp[e]
Proof state after:
no goals
Theorem: Primrec.option_get!
Proof state before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁸ : Primcodable α✝
inst✝⁷ : Primcodable α₁
inst✝⁶ : Primcodable α₂
inst✝⁵ : Primcodable β
inst✝⁴ : Primcodable γ
inst✝³ : Primcodable σ
inst✝² : Primcodable τ
α : Type u_8
inst✝¹ : Primcodable α
inst✝ : Inhabited α
⊢ ∀ (n : Option α), (Option.casesOn (id n) default fun b => b) = n.get!
Tactic:
rintro (_ | a) <;> simp
Proof state after:
no goals
Theorem: Encodable.decode_list
Proof state before:
β : Type u_1
inst✝ : Encodable β
⊢ decode 0 = mapM' decode (Denumerable.ofNat (List ℕ) 0)
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.decode_list
Proof state before:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ decode (e + 1) = mapM' decode (Denumerable.ofNat (List ℕ) (e + 1))
Tactic:
simp
Proof state after:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) =
    (decode e.unpair.1).bind fun __do_lift =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Theorem: Encodable.decode_list
Proof state before:
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) =
    (decode e.unpair.1).bind fun __do_lift =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Tactic:
rcases (decode e.unpair.1 : Option β) with (_ | b) <;> simp[seq_eq_bind, Option.bind_eq_bind]
Proof state after:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
b : β
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Theorem: Encodable.decode_list
Proof state before:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
b : β
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Tactic:
have := decode_list (e.unpair.2)
Proof state after:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this✝ : e.unpair.2 < e + 1
b : β
this : decode e.unpair.2 = mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Theorem: Encodable.decode_list
Proof state before:
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this✝ : e.unpair.2 < e + 1
b : β
this : decode e.unpair.2 = mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)
Tactic:
simp[this, Option.pure_eq_some, Option.map_eq_bind, Function.comp]
Proof state after:
no goals
Theorem: Encodable.decode_vector
Proof state before:
β : Type u_1
inst✝ : Encodable β
k e : ℕ
⊢ decode e = (decode e).bind (List.toVector k)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Encodable.decode_finArrow
Proof state before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ decode e = (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
simp[Primcodable.ofEquiv_toEncodable, Encodable.decode_ofEquiv]
Proof state after:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) (decode e) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Theorem: Encodable.decode_finArrow
Proof state before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) (decode e) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
rw[decode_vector]
Proof state after:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) ((decode e).bind (List.toVector k)) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Theorem: Encodable.decode_finArrow
Proof state before:
β✝ : Type u_1
inst✝¹ : Encodable β✝
k : ℕ
β : Type u_2
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑(Equiv.vectorEquivFin β k)) ((decode e).bind (List.toVector k)) =
    (decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)
Tactic:
rcases (decode e : Option (List β)) with (_ | bs) <;> simp
Proof state after:
no goals
Theorem: Encodable.decode_fintypeArrow
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ decode e = (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)
Tactic:
simp [Primcodable.ofEquiv_toEncodable, Encodable.decode_ofEquiv, decode_vector]
Proof state after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      ((decode e).bind (List.toVector (Fintype.card ι))) =
    (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)
Theorem: Encodable.decode_fintypeArrow
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      ((decode e).bind (List.toVector (Fintype.card ι))) =
    (decode e).bind fun l => Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)
Tactic:
rcases (decode e : Option (List β)) with (_ | bs) <;> simp
Proof state after:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)
Theorem: Encodable.decode_fintypeArrow
Proof state before:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)
Tactic:
{ rfl }
Proof state after:
no goals
Theorem: Encodable.decode_fintypeArrow
Proof state before:
case some
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
e : ℕ
bs : List β
⊢ Option.map (⇑fintypeArrowEquivFinArrow.symm ∘ ⇑(Equiv.vectorEquivFin β (Fintype.card ι)))
      (List.toVector (Fintype.card ι) bs) =
    Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) bs)
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.encode_list
Proof state before:
β : Type u_1
inst✝ : Encodable β
l : List β
⊢ encode l = encode (List.map encode l)
Tactic:
induction l <;> simp[*]
Proof state after:
no goals
Theorem: Encodable.encode_finArrow
Proof state before:
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode f = encode (List.ofFn f)
Tactic:
rw[Encodable.encode_ofEquiv, encode_vector]
Proof state after:
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode ((Equiv.vectorEquivFin β n).symm f).toList = encode (List.ofFn f)
Theorem: Encodable.encode_finArrow
Proof state before:
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode ((Equiv.vectorEquivFin β n).symm f).toList = encode (List.ofFn f)
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.encode_finArrow'
Proof state before:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode f = encode fun i => encode (f i)
Tactic:
simp[encode_finArrow, encode_list (List.ofFn f)]
Proof state after:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode ∘ f = fun i => encode (f i)
Theorem: Encodable.encode_finArrow'
Proof state before:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode ∘ f = fun i => encode (f i)
Tactic:
funext i
Proof state after:
case h
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
i : Fin k
⊢ (encode ∘ f) i = encode (f i)
Theorem: Encodable.encode_finArrow'
Proof state before:
case h
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
i : Fin k
⊢ (encode ∘ f) i = encode (f i)
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.encode_fintypeArrow
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode (fintypeArrowEquivFinArrow f)
Tactic:
rw[Encodable.encode_ofEquiv]
Proof state after:
no goals
Theorem: Encodable.encode_fintypeArrow'
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode fun i => encode (f i)
Tactic:
simp[encode_fintypeArrow, encode_finArrow, encode_list (List.ofFn $ fintypeArrowEquivFinArrow f)]
Proof state after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode ∘ fintypeArrowEquivFinArrow f = fintypeArrowEquivFinArrow fun i => encode (f i)