internlm/Lean-Github huggingface dataset:
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h.h₁.a
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f a ↔ x = a
Tactic:
constructor
Proof state after:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f a → x = a

case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ x = a → f x = f a
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h.h₁.a.mp
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f a → x = a
Tactic:
apply h1
Proof state after:
no goals
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ x = a → f x = f a
Tactic:
intro a1
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
a1 : x = a
⊢ f x = f a
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
a1 : x = a
⊢ f x = f a
Tactic:
subst a1
Proof state after:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f x
Theorem: Function.updateITE_comp_right_injective
Proof state before:
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
⊢ updateITE (updateITE f a d) b c = updateITE (updateITE f b c) a d
Tactic:
funext x
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a d) b c x = updateITE (updateITE f b c) a d x
Theorem: Function.updateITE_comm
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a d) b c x = updateITE (updateITE f b c) a d 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 c else if x = a then d else f x) = if x = a then d else if x = b then c else f x
Theorem: Function.updateITE_comm
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ (if x = b then c else if x = a then d else f x) = if x = a then d else if x = b then c else f x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : x = b
h✝ : x = a
⊢ c = d

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : x = b
h✝ : ¬x = a
⊢ c = c

case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : ¬x = b
h✝ : x = a
⊢ d = d

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : ¬x = b
h✝ : ¬x = a
⊢ f x = f x
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = b
c2 : x = a
⊢ c = d
Tactic:
case _ c1 c2 =>
  subst c1 c2
  contradiction
Proof state after:
no goals
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : ¬x = b
h✝ : ¬x = a
⊢ f x = f x
Tactic:
case _ | _ | _ =>
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = b
c2 : x = a
⊢ c = d
Tactic:
subst c1 c2
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
c d : β
x : α
h1 : ¬x = x
⊢ c = d
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
c d : β
x : α
h1 : ¬x = x
⊢ c = d
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateITE_comm
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : ¬x = b
h✝ : ¬x = a
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_idem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
⊢ updateITE (updateITE f a b) a c = updateITE f a c
Tactic:
funext x
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ updateITE (updateITE f a b) a c x = updateITE f a c x
Theorem: Function.updateITE_idem
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ updateITE (updateITE f a b) a c x = updateITE f a c x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ (if x = a then c else if x = a then b else f x) = if x = a then c else f x
Theorem: Function.updateITE_idem
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ (if x = a then c else if x = a then b else f x) = if x = a then c else f x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : x = a
⊢ c = c

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : ¬x = a
⊢ f x = f x
Theorem: Function.updateITE_idem
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : x = a
⊢ c = c
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_idem
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : ¬x = a
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
⊢ updateITE id a a = id
Tactic:
funext x
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ updateITE id a a x = id x
Theorem: Function.updateITE_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ updateITE id a a x = id x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ (if x = a then a else id x) = id x
Theorem: Function.updateITE_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ (if x = a then a else id x) = id x
Tactic:
split_ifs
Proof state after:
case pos
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : x = a
⊢ a = id x

case neg
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a x : α
c1 : x = a
⊢ a = id x
Tactic:
case _ c1 =>
  subst c1
  simp
Proof state after:
no goals
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x
Tactic:
case _ =>
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a x : α
c1 : x = a
⊢ a = id x
Tactic:
subst c1
Proof state after:
α : Type
inst✝ : DecidableEq α
x : α
⊢ x = id x
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
x : α
⊢ x = id x
Tactic:
simp
Proof state after:
no goals
Theorem: Function.updateITE_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_comm_id
Proof state before:
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
⊢ updateITE (updateITE id b c) a a = updateITE id b c
Tactic:
funext x
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ updateITE (updateITE id b c) a a x = updateITE id b c x
Theorem: Function.updateITE_comm_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ updateITE (updateITE id b c) a a x = updateITE id b c x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ (if x = a then a else if x = b then c else id x) = if x = b then c else id x
Theorem: Function.updateITE_comm_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ (if x = a then a else if x = b then c else id x) = if x = b then c else id x
Tactic:
simp
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ x = a → a = if x = b then c else x
Theorem: Function.updateITE_comm_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ x = a → a = if x = b then c else x
Tactic:
intro a1
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
a1 : x = a
⊢ a = if x = b then c else x
Theorem: Function.updateITE_comm_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
a1 : x = a
⊢ a = if x = b then c else x
Tactic:
subst a1
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
b c x : α
h1 : ¬x = b
⊢ x = if x = b then c else x
Theorem: Function.updateITE_comm_id
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
b c x : α
h1 : ¬x = b
⊢ x = if x = b then c else x
Tactic:
simp only [if_neg h1]
Proof state after:
no goals
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
⊢ updateITE f a (g a) = g
Tactic:
funext x
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ updateITE f a (g a) x = g x
Theorem: Function.updateITE_coincide
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ updateITE f a (g a) x = g x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ (if x = a then g a else f x) = g x
Theorem: Function.updateITE_coincide
Proof state before:
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ (if x = a then g a else f x) = g x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
h✝ : x = a
⊢ g a = g x

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
h✝ : ¬x = a
⊢ f x = g x
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : x = a
⊢ g a = g x
Tactic:
case _ c1 =>
  subst c1
  rfl
Proof state after:
no goals
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : ¬x = a
⊢ f x = g x
Tactic:
case _ c1 =>
  exact h1 x c1
Proof state after:
no goals
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : x = a
⊢ g a = g x
Tactic:
subst c1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : ∀ (x_1 : α), ¬x_1 = x → f x_1 = g x_1
⊢ g x = g x
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : ∀ (x_1 : α), ¬x_1 = x → f x_1 = g x_1
⊢ g x = g x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateITE_coincide
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : ¬x = a
⊢ f x = g x
Tactic:
exact h1 x c1
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
xs : List α
f : α → β
a : α
b : β
h1 : a ∉ xs
⊢ List.map (updateITE f a b) xs = List.map f xs
Tactic:
induction xs
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []

case cons
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : a ∉ tail✝ → List.map (updateITE f a b) tail✝ = List.map f tail✝
h1 : a ∉ head✝ :: tail✝
⊢ List.map (updateITE f a b) (head✝ :: tail✝) = List.map f (head✝ :: tail✝)
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ∉ hd :: tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
case cons hd tl ih =>
  simp at h1
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    simp
    simp only [Function.updateITE]
    split_ifs <;> tauto
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []
Tactic:
simp
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ∉ hd :: tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
simp at h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : ¬a = hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : ¬a = hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
push_neg at h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ≠ hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ≠ hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
cases h1
Proof state after:
case intro
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
left✝ : a ≠ hd
right✝ : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
case intro h1_left h1_right =>
  simp
  simp only [Function.updateITE]
  split_ifs <;> tauto
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
simp
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ updateITE f a b hd = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ updateITE f a b hd = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Tactic:
simp only [Function.updateITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ (if hd = a then b else f hd) = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Theorem: Function.updateITE_not_mem_list
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ (if hd = a then b else f hd) = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Tactic:
split_ifs <;> tauto
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
f : α → β
a : α
b : β
h1 : a ∉ S
⊢ Finset.image (updateITE f a b) S = Finset.image f S
Tactic:
induction S using Finset.induction_on
Proof state after:
case empty
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅

case insert
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
a✝² : α
s✝ : Finset α
a✝¹ : a✝² ∉ s✝
a✝ : a ∉ s✝ → Finset.image (updateITE f a b) s✝ = Finset.image f s✝
h1 : a ∉ insert a✝² s✝
⊢ Finset.image (updateITE f a b) (insert a✝² s✝) = Finset.image f (insert a✝² s✝)
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅
Tactic:
case empty =>
  simp
Proof state after:
no goals
Theorem: Function.updateITE_not_mem_set
Proof state before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅
Tactic:
simp
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 : a ∉ insert S_a S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
simp at h1
Proof state after:
α β : 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 : ¬a = S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
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 : ¬a = S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
push_neg at h1
Proof state after:
α β : 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 : a ≠ S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
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 : a ≠ S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
cases h1
Proof state after:
case intro
α β : 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
left✝ : a ≠ S_a
right✝ : a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
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
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
simp
Proof state after:
α β : 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
⊢ insert (updateITE f a b S_a) (Finset.image (updateITE f a b) S_S) = insert (f S_a) (Finset.image f S_S)
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
⊢ insert (updateITE f a b S_a) (Finset.image (updateITE f a b) S_S) = insert (f S_a) (Finset.image f S_S)
Tactic:
congr! 1
Proof state after:
case h.e'_4
α β : 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
⊢ updateITE f a b S_a = f S_a

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
Theorem: Function.updateITE_not_mem_set
Proof state before:
case h.e'_4
α β : 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
⊢ updateITE f a b S_a = f S_a
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.e'_4
α β : 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
⊢ (if S_a = a then b else f S_a) = f S_a
Theorem: Function.updateITE_not_mem_set
Proof state before:
case h.e'_4
α β : 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
⊢ (if S_a = a then b else f S_a) = f S_a
Tactic:
split_ifs
Proof state after:
case pos
α β : 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
h✝ : S_a = a
⊢ b = f S_a

case neg
α β : 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
h✝ : ¬S_a = a
⊢ f S_a = f S_a
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:
case _ c1 =>
  subst c1
  contradiction
Proof state after:
no goals