internlm/Lean-Github huggingface dataset:
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : ¬S_a = a
⊢ f S_a = f S_a
Tactic:
case _ c1 =>
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : S_a = a
⊢ b = f S_a
Tactic:
subst c1
Proof state after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : S_a ∉ S_S → Finset.image (updateITE f S_a b) S_S = Finset.image f S_S
h1_left : S_a ≠ S_a
h1_right : S_a ∉ S_S
⊢ b = f S_a
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : S_a ∉ S_S → Finset.image (updateITE f S_a b) S_S = Finset.image f S_S
h1_left : S_a ≠ S_a
h1_right : S_a ∉ S_S
⊢ b = f S_a
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : ¬S_a = a
⊢ f S_a = f S_a
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_set
Proof state before:
case h.e'_5
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ Finset.image (updateITE f a b) S_S = Finset.image f S_S
Tactic:
exact S_ih h1_right
Proof state after:
no goals
Theorem: Function.updateITE_symm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
⊢ updateITE (updateITE f a c) b d = updateITE (updateITE f b d) a c
Tactic:
funext x
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a c) b d x = updateITE (updateITE f b d) a c x
Theorem: Function.updateITE_symm
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a c) b d x = updateITE (updateITE f b d) a c x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
by_cases c1 : x = a
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
by_cases c2 : x = b
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
subst c1
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 : x = b
h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 : x = b
h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x
Tactic:
subst c2
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
c d : β
x : α
h1 : ¬x = x
⊢ (if x = x then d else if x = x then c else f x) = if x = x then c else if x = x then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
c d : β
x : α
h1 : ¬x = x
⊢ (if x = x then d else if x = x then c else f x) = if x = x then c else if x = x then d else f x
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
subst c1
Proof state after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x
Tactic:
simp
Proof state after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ x = b → d = c
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ x = b → d = c
Tactic:
intro a1
Proof state after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
a1 : x = b
⊢ d = c
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
a1 : x = b
⊢ d = c
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
by_cases c2 : x = b
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
subst c2
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
c d : β
x : α
c1 : ¬x = a
h1 : ¬a = x
⊢ (if x = x then d else if x = a then c else f x) = if x = a then c else if x = x then d else f x
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
c d : β
x : α
c1 : ¬x = a
h1 : ¬a = x
⊢ (if x = x then d else if x = a then c else f x) = if x = a then c else if x = x then d else f x
Tactic:
simp
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
c d : β
x : α
c1 : ¬x = a
h1 : ¬a = x
⊢ d = if x = a then c else d
Theorem: Function.updateITE_symm
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
c d : β
x : α
c1 : ¬x = a
h1 : ¬a = x
⊢ d = if x = a then c else d
Tactic:
simp only [if_neg c1]
Proof state after:
no goals
Theorem: Function.updateITE_symm
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
simp only [if_neg c1]
Proof state after:
no goals
Theorem: Function.updateITE_comp
Proof state before:
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
⊢ updateITE g c d (updateITE f b c a) = updateITE (g ∘ f) b d a
Tactic:
simp only [Function.updateITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Theorem: Function.updateITE_comp
Proof state before:
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Tactic:
by_cases c1 : a = b
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a

case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Theorem: Function.updateITE_comp
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Tactic:
simp only [c1]
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if True then c else f b) = c then d else g (if True then c else f b)) = if True then d else (g ∘ f) b
Theorem: Function.updateITE_comp
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if True then c else f b) = c then d else g (if True then c else f b)) = if True then d else (g ∘ f) b
Tactic:
simp
Proof state after:
no goals
Theorem: Function.updateITE_comp
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Tactic:
simp only [c1]
Proof state after:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ (if (if False then c else f a) = c then d else g (if False then c else f a)) = if False then d else (g ∘ f) a
Theorem: Function.updateITE_comp
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ (if (if False then c else f a) = c then d else g (if False then c else f a)) = if False then d else (g ∘ f) a
Tactic:
simp
Proof state after:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ f a = c → d = g (f a)
Theorem: Function.updateITE_comp
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ f a = c → d = g (f a)
Tactic:
exact h1
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs : List α
ys : List β
⊢ g ∘ updateListITE f xs ys = updateListITE (g ∘ f) xs (List.map g ys)
Tactic:
induction xs generalizing ys
Proof state after:
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)

case cons
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List β), g ∘ updateListITE f tail✝ ys = updateListITE (g ∘ f) tail✝ (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (head✝ :: tail✝) ys = updateListITE (g ∘ f) (head✝ :: tail✝) (List.map g ys)
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)
Tactic:
case nil =>
  simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) ys = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g ys)
Tactic:
case cons _ xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp
    simp only [Function.updateListITE]
  case cons ys_hd ys_tl =>
    simp
    simp only [Function.updateListITE]
    simp only [← xs_ih]
    apply Function.updateITE_comp_left
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)
Tactic:
simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) ys = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g ys)
Tactic:
cases ys
Proof state after:
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])

case cons
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
head✝ : β
tail✝ : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (head✝ :: tail✝) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (head✝ :: tail✝))
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])
Tactic:
case nil =>
  simp
  simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (ys_hd :: ys_tl))
Tactic:
case cons ys_hd ys_tl =>
  simp
  simp only [Function.updateListITE]
  simp only [← xs_ih]
  apply Function.updateITE_comp_left
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])
Tactic:
simp
Proof state after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) []
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) []
Tactic:
simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (ys_hd :: ys_tl))
Tactic:
simp
Proof state after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (g ys_hd :: List.map g ys_tl)
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (g ys_hd :: List.map g ys_tl)
Tactic:
simp only [Function.updateListITE]
Proof state after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd =
    updateITE (updateListITE (g ∘ f) xs_tl (List.map g ys_tl)) xs_hd (g ys_hd)
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd =
    updateITE (updateListITE (g ∘ f) xs_tl (List.map g ys_tl)) xs_hd (g ys_hd)
Tactic:
simp only [← xs_ih]
Proof state after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd = updateITE (g ∘ updateListITE f xs_tl ys_tl) xs_hd (g ys_hd)
Theorem: Function.updateListITE_comp
Proof state before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd = updateITE (g ∘ updateListITE f xs_tl ys_tl) xs_hd (g ys_hd)
Tactic:
apply Function.updateITE_comp_left
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : f x = g x
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map f ys) x
Tactic:
induction xs generalizing ys
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ updateListITE f [] (List.map f ys) x = updateListITE g [] (List.map f ys) x

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List α), updateListITE f tail✝ (List.map f ys) x = updateListITE g tail✝ (List.map f ys) x
ys : List α
⊢ updateListITE f (head✝ :: tail✝) (List.map f ys) x = updateListITE g (head✝ :: tail✝) (List.map f ys) x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ updateListITE f [] (List.map f ys) x = updateListITE g [] (List.map f ys) x
Tactic:
case nil =>
  simp only [Function.updateListITE]
  exact h1
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ updateListITE f [] (List.map f ys) x = updateListITE g [] (List.map f ys) x
Tactic:
simp only [Function.updateListITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ f x = g x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ f x = g x
Tactic:
exact h1
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f ys) x = updateListITE g (xs_hd :: xs_tl) (List.map f ys) x
Tactic:
cases ys
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
head✝ : α
tail✝ : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f (head✝ :: tail✝)) x =
    updateListITE g (xs_hd :: xs_tl) (List.map f (head✝ :: tail✝)) x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x
Tactic:
case nil =>
  simp
  simp only [Function.updateListITE]
  exact h1
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x
Tactic:
simp
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) [] x = updateListITE g (xs_hd :: xs_tl) [] x