internlm/Lean-Github huggingface dataset:
Theorem: LO.System.ModusPonens.mdp!
Proof state before:
case intro.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
hpq : 𝓢 ⊢ p ⟶ q
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! q
Tactic:
exact ⟨hpq ⨀ hp⟩
Proof state after:
no goals
Theorem: LO.System.unprovable_imp_trans!
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
hpq : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊬! p ⟶ r → 𝓢 ⊬! q ⟶ r
Tactic:
contrapose
Proof state after:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
hpq : 𝓢 ⊢! p ⟶ q
⊢ ¬𝓢 ⊬! q ⟶ r → ¬𝓢 ⊬! p ⟶ r
Theorem: LO.System.unprovable_imp_trans!
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
hpq : 𝓢 ⊢! p ⟶ q
⊢ ¬𝓢 ⊬! q ⟶ r → ¬𝓢 ⊬! p ⟶ r
Tactic:
simp [neg_neg]
Proof state after:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
hpq : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Theorem: LO.System.unprovable_imp_trans!
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
hpq : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Tactic:
exact imp_trans! hpq
Proof state after:
no goals
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r ↔ 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
apply Iff.intro
Proof state after:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r

case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r

case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
. intro ⟨h⟩; exact ⟨andImplyIffImplyImply'.mp h⟩
Proof state after:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
. intro ⟨h⟩; exact ⟨andImplyIffImplyImply'.mpr h⟩
Proof state after:
no goals
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
intro ⟨h⟩
Proof state after:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⋏ q ⟶ r
⊢ 𝓢 ⊢! p ⟶ q ⟶ r
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⋏ q ⟶ r
⊢ 𝓢 ⊢! p ⟶ q ⟶ r
Tactic:
exact ⟨andImplyIffImplyImply'.mp h⟩
Proof state after:
no goals
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⟶ q ⟶ r → 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
intro ⟨h⟩
Proof state after:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⟶ q ⟶ r
⊢ 𝓢 ⊢! p ⋏ q ⟶ r
Theorem: LO.System.andImplyIffImplyImply'!
Proof state before:
case mpr
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⟶ q ⟶ r
⊢ 𝓢 ⊢! p ⋏ q ⟶ r
Tactic:
exact ⟨andImplyIffImplyImply'.mpr h⟩
Proof state after:
no goals
Theorem: List.lookup_map_fun_of_mem
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun x => (x, f x)) as) = some (f a)
Tactic:
induction' as with a' as ih
Proof state after:
case nil
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)

case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case nil
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)
Tactic:
simp at h
Proof state after:
no goals
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
simp at h
Proof state after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
have : a = a' ∨ (a ≠ a' ∧ a ∈ as) := by { by_cases ha : a = a'; { simp[ha] }; { simp[ha] at h; exact Or.inr ⟨ha, h⟩ } }
Proof state after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
this : a = a' ∨ a ≠ a' ∧ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
this : a = a' ∨ a ≠ a' ∧ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
rcases this with (rfl | ⟨hne, hmem⟩) <;> simp[lookup]
Proof state after:
case cons.inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
hne : a ≠ a'
hmem : a ∈ as
⊢ (match a == a' with
    | true => some (f a')
    | false => lookup a (map (fun x => (x, f x)) as)) =
    some (f a)
Theorem: List.lookup_map_fun_of_mem
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
by_cases ha : a = a'
Proof state after:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
{ simp[ha] }
Proof state after:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
{ simp[ha] at h; exact Or.inr ⟨ha, h⟩ }
Proof state after:
no goals
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
simp[ha]
Proof state after:
no goals
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
simp[ha] at h
Proof state after:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
ha : ¬a = a'
h : a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
ha : ¬a = a'
h : a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
exact Or.inr ⟨ha, h⟩
Proof state after:
no goals
Theorem: List.lookup_map_fun_of_mem
Proof state before:
case cons.inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
hne : a ≠ a'
hmem : a ∈ as
⊢ (match a == a' with
    | true => some (f a')
    | false => lookup a (map (fun x => (x, f x)) as)) =
    some (f a)
Tactic:
simp[beq_false_of_ne hne, ih hmem]
Proof state after:
no goals
Theorem: List.mapGraph_graph
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as as' : List α
has : as' ⊆ as
⊢ (map (fun x => (x, f x)) as).mapGraph as' = map f as'
Tactic:
induction' as' with a as' ih <;> simp[mapGraph]
Proof state after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Theorem: List.mapGraph_graph
Proof state before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
have : a ∈ as ∧ as' ⊆ as := by simpa using has
Proof state after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
this : a ∈ as ∧ as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Theorem: List.mapGraph_graph
Proof state before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
this : a ∈ as ∧ as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
rcases this with ⟨ha, has'⟩
Proof state after:
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Theorem: List.mapGraph_graph
Proof state before:
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
simp[lookup_map_fun_of_mem f ha]
Proof state after:
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ (as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) = map f as'
Theorem: List.mapGraph_graph
Proof state before:
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ (as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) = map f as'
Tactic:
exact ih has'
Proof state after:
no goals
Theorem: List.mapGraph_graph
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ a ∈ as ∧ as' ⊆ as
Tactic:
simpa using has
Proof state after:
no goals
Theorem: List.subset_bind_of_mem
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
⊢ f a ⊆ as.bind f
Tactic:
intro a' ha'
Proof state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
a' : α
ha' : a' ∈ f a
⊢ a' ∈ as.bind f
Theorem: List.subset_bind_of_mem
Proof state before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
a' : α
ha' : a' ∈ f a
⊢ a' ∈ as.bind f
Tactic:
simpa using ⟨a, h, ha'⟩
Proof state after:
no goals
Theorem: Primrec.option_toList
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ Primrec Option.toList
Tactic:
have : Primrec (fun a => [a] : α → List α) := list_cons.comp Primrec.id (const [])
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
⊢ Primrec Option.toList
Theorem: Primrec.option_toList
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
⊢ Primrec Option.toList
Tactic:
exact (option_casesOn Primrec.id (const []) (this.comp₂ Primrec₂.right)).of_eq
  (fun o => by rcases o <;> simp)
Proof state after:
no goals
Theorem: Primrec.option_toList
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
o : Option α
⊢ (Option.casesOn (id o) [] fun b => [b]) = o.toList
Tactic:
rcases o <;> simp
Proof state after:
no goals
Theorem: Primrec.iterate
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
⊢ Primrec₂ fun x x_1 => f^[x] x_1
Tactic:
have : Primrec₂ (fun s a => s.rec a (fun _ => f) : ℕ → α → α) :=
  to₂ (nat_rec' fst snd (hf.comp₂ (snd.comp₂ Primrec₂.right)))
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
⊢ Primrec₂ fun x x_1 => f^[x] x_1
Theorem: Primrec.iterate
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
⊢ Primrec₂ fun x x_1 => f^[x] x_1
Tactic:
exact this.of_eq (fun s a => by
  induction' s with s ih <;> simp[*]; { exact Eq.symm (Function.iterate_succ_apply' f s a) })
Proof state after:
no goals
Theorem: Primrec.iterate
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
s : ℕ
a : α
⊢ Nat.rec a (fun x => f) s = f^[s] a
Tactic:
induction' s with s ih <;> simp[*]
Proof state after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
Theorem: Primrec.iterate
Proof state before:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
Tactic:
{ exact Eq.symm (Function.iterate_succ_apply' f s a) }
Proof state after:
no goals
Theorem: Primrec.iterate
Proof state before:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
Tactic:
exact Eq.symm (Function.iterate_succ_apply' f s a)
Proof state after:
no goals
Theorem: Primrec.list_take
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ Primrec₂ List.take
Tactic:
have : Primrec₂ (fun s a => s.rec [] (fun n as => as ++ (a.get? n).toList) : ℕ → List α → List α) :=
  to₂ (nat_rec' fst (const [])
    (list_append.comp₂ (snd.comp₂ Primrec₂.right)
      (option_toList.comp₂ $ list_get?.comp₂ (snd.comp₂ Primrec₂.left) (fst.comp₂ Primrec₂.right))))
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec₂ fun s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
⊢ Primrec₂ List.take
Theorem: Primrec.list_take
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec₂ fun s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
⊢ Primrec₂ List.take
Tactic:
exact this.of_eq (fun n as => by induction' n with n ih <;> simp[List.take_succ, *])
Proof state after:
no goals