internlm/Lean-Github huggingface dataset:
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
rw [foldl_step] <;> try assumption
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data = as.data ++ bs.data.extract start stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data = as.data ++ bs.data.extract start stop
Tactic:
rw [List.extract_step]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

case hstart
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

case hstart
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length
Tactic:
rw [data_append_aux (start+1) stop] <;> try assumption
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (as.push bs[start]).data ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (as.push bs[start]).data ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [push_data]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs[start]] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs[start]] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [getElem_eq_data_get]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [List.append_assoc]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ ([bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop) =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ ([bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop) =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [List.singleton_append]
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.sum_stop
Proof state before:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ ns.sum stop stop = 0
Tactic:
simp only [sum]
Proof state after:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns stop stop = 0
Theorem: Array.sum_stop
Proof state before:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns stop stop = 0
Tactic:
rw [foldl_stop]
Proof state after:
case hstop
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ stop ≤ ns.size
Theorem: Array.sum_stop
Proof state before:
case hstop
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ stop ≤ ns.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.sum_step
Proof state before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
Tactic:
have : start < ns.size := Nat.lt_of_lt_of_le hstart hstop
Proof state after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
Theorem: Array.sum_step
Proof state before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
Tactic:
simp only [sum]
Proof state after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns start stop = ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Theorem: Array.sum_step
Proof state before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns start stop = ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [foldl_step] <;> try assumption
Proof state after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (0 + ns[start]) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Theorem: Array.sum_step
Proof state before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (0 + ns[start]) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [Nat.add_comm 0 ns[start]]
Proof state after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (ns[start] + 0) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Theorem: Array.sum_step
Proof state before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (ns[start] + 0) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [ns.foldl_assoc (.+.) ns[start] 0 (start+1) stop (Nat.succ_le_of_lt hstart) hstop]
Proof state after:
no goals
Theorem: Array.sum_step
Proof state before:
case hstop
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ stop ≤ ns.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.get_ofFn
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ (ofFn f).get i = f (⋯ ▸ i)
Tactic:
rw [get_eq_getElem, getElem_ofFn]
Proof state after:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ f ⟨↑i, ⋯⟩ = f (⋯ ▸ i)
Theorem: Array.get_ofFn
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ f ⟨↑i, ⋯⟩ = f (⋯ ▸ i)
Tactic:
congr 1
Proof state after:
case e_a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ⟨↑i, ⋯⟩ = ⋯ ▸ i
Theorem: Array.get_ofFn
Proof state before:
case e_a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ⟨↑i, ⋯⟩ = ⋯ ▸ i
Tactic:
ext
Proof state after:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑⟨↑i, ⋯⟩ = ↑(⋯ ▸ i)
Theorem: Array.get_ofFn
Proof state before:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑⟨↑i, ⋯⟩ = ↑(⋯ ▸ i)
Tactic:
simp only
Proof state after:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑i = ↑(⋯ ▸ i)
Theorem: Array.get_ofFn
Proof state before:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑i = ↑(⋯ ▸ i)
Tactic:
apply Fin.val_eq_val_of_heq (size_ofFn ..)
Proof state after:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ ⋯ ▸ i
Theorem: Array.get_ofFn
Proof state before:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ ⋯ ▸ i
Tactic:
elim_casts
Proof state after:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ i
Theorem: Array.get_ofFn
Proof state before:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ i
Tactic:
rfl
Proof state after:
no goals
Theorem: eqNdrec_eq_cast
Proof state before:
α : Sort u_1
a b : α
motive : α → Sort u_2
t : motive a
h : a = b
⊢ h ▸ t = cast ⋯ t
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ ⋯ ▸ t = cast ⋯ t
Theorem: eqNdrec_eq_cast
Proof state before:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ ⋯ ▸ t = cast ⋯ t
Tactic:
rfl
Proof state after:
no goals
Theorem: eqNdrec_symm
Proof state before:
α : Sort u_1
motive : α → Sort u_2
a b : α
h : a = b
x : motive a
y : motive b
⊢ h ▸ x = y ↔ x = ⋯ ▸ y
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
motive : α → Sort u_2
a : α
x y : motive a
⊢ ⋯ ▸ x = y ↔ x = ⋯ ▸ y
Theorem: eqNdrec_symm
Proof state before:
case refl
α : Sort u_1
motive : α → Sort u_2
a : α
x y : motive a
⊢ ⋯ ▸ x = y ↔ x = ⋯ ▸ y
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: cast_trans
Proof state before:
α β γ : Sort u_1
h₁ : α = β
h₂ : β = γ
a : α
⊢ cast h₂ (cast h₁ a) = cast ⋯ a
Tactic:
cases h₁
Proof state after:
case refl
α γ : Sort u_1
a : α
h₂ : α = γ
⊢ cast h₂ (cast ⋯ a) = cast ⋯ a
Theorem: cast_trans
Proof state before:
case refl
α γ : Sort u_1
a : α
h₂ : α = γ
⊢ cast h₂ (cast ⋯ a) = cast ⋯ a
Tactic:
cases h₂
Proof state after:
case refl.refl
α : Sort u_1
a : α
⊢ cast ⋯ (cast ⋯ a) = cast ⋯ a
Theorem: cast_trans
Proof state before:
case refl.refl
α : Sort u_1
a : α
⊢ cast ⋯ (cast ⋯ a) = cast ⋯ a
Tactic:
rfl
Proof state after:
no goals
Theorem: cast_symm
Proof state before:
α β : Sort u_1
h : α = β
a : α
b : β
⊢ cast h a = b ↔ a = cast ⋯ b
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a b : α
⊢ cast ⋯ a = b ↔ a = cast ⋯ b
Theorem: cast_symm
Proof state before:
case refl
α : Sort u_1
a b : α
⊢ cast ⋯ a = b ↔ a = cast ⋯ b
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
α : Sort u_1
a : α
s : Set α
⊢ s.insertIf a True = s.insert a
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.insertIf a True ↔ x ∈ s.insert a
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case a
α : Sort u_1
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.insertIf a True ↔ x ∈ s.insert a
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True ↔ x ∈ s.insert a
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case a
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True ↔ x ∈ s.insert a
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True → x ∈ s.insert a

case a.mpr
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insert a → x ∈ s.insertIf a True
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case a.mp
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True → x ∈ s.insert a
Tactic:
intro
| Or.inl ⟨_,_⟩ => left; assumption
| Or.inr _ => right; assumption
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ s.insert a
Tactic:
left
Proof state after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ Set.pure a
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ Set.pure a
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s.insert a
Tactic:
right
Proof state after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case a.mpr
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insert a → x ∈ s.insertIf a True
Tactic:
intro
| Or.inl _ => left; constructor; assumption; trivial
| Or.inr _ => right; assumption
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ s.insertIf a True
Tactic:
left
Proof state after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ Set.pureIf a True
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ Set.pureIf a True
Tactic:
constructor
Proof state after:
case h.left
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x = a

case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h.left
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x = a

case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Tactic:
assumption
Proof state after:
case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: Set.insertIf_true_eq_insert
Proof state before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s.insertIf a True
Tactic:
right
Proof state after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s
Theorem: Set.insertIf_true_eq_insert
Proof state before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.insert_idem
Proof state before:
α : Sort u_1
a : α
s : Set α
⊢ (s.insert a).insert a = ((Set.pure a).union (Set.pure a)).union s
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_idem
Proof state before:
α : Sort u_1
a : α
s : Set α
⊢ ((Set.pure a).union (Set.pure a)).union s = (Set.pure a).union s
Tactic:
rw [union_idem]
Proof state after:
no goals
Theorem: Set.insertIf_idem
Proof state before:
α : Sort u_1
p : Prop
a : α
s : Set α
⊢ (s.insertIf a p).insertIf a p = ((Set.pureIf a p).union (Set.pureIf a p)).union s
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_idem
Proof state before:
α : Sort u_1
p : Prop
a : α
s : Set α
⊢ ((Set.pureIf a p).union (Set.pureIf a p)).union s = (Set.pureIf a p).union s
Tactic:
rw [union_idem]
Proof state after:
no goals
Theorem: Set.insert_comm
Proof state before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ (s.insert a₁).insert a₂ = ((Set.pure a₂).union (Set.pure a₁)).union s
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_comm
Proof state before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ ((Set.pure a₂).union (Set.pure a₁)).union s = ((Set.pure a₁).union (Set.pure a₂)).union s
Tactic:
rw [union_comm (Set.pure a₁) (Set.pure a₂)]
Proof state after:
no goals
Theorem: Set.insert_comm
Proof state before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ ((Set.pure a₁).union (Set.pure a₂)).union s = (Set.pure a₁).union ((Set.pure a₂).union s)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_comm
Proof state before:
α : Sort u_1
p₁ p₂ : Prop
a₁ a₂ : α
s : Set α
⊢ (s.insertIf a₁ p₁).insertIf a₂ p₂ = ((Set.pureIf a₂ p₂).union (Set.pureIf a₁ p₁)).union s
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_comm
Proof state before:
α : Sort u_1
p₁ p₂ : Prop
a₁ a₂ : α
s : Set α
⊢ ((Set.pureIf a₂ p₂).union (Set.pureIf a₁ p₁)).union s = ((Set.pureIf a₁ p₁).union (Set.pureIf a₂ p₂)).union s
Tactic:
rw [union_comm (Set.pureIf a₁ p₁) (Set.pureIf a₂ p₂)]
Proof state after:
no goals
Theorem: Set.insertIf_comm
Proof state before:
α : Sort u_1
p₁ p₂ : Prop
a₁ a₂ : α
s : Set α
⊢ ((Set.pureIf a₁ p₁).union (Set.pureIf a₂ p₂)).union s = (Set.pureIf a₁ p₁).union ((Set.pureIf a₂ p₂).union s)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_union_left
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.insert a).union t = (Set.pure a).union (s.union t)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_union_right
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ s.union (t.insert a) = (s.union (Set.pure a)).union t
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_union_right
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.union (Set.pure a)).union t = ((Set.pure a).union s).union t
Tactic:
rw [union_comm (Set.pure a) s]
Proof state after:
no goals
Theorem: Set.insert_union_right
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ ((Set.pure a).union s).union t = (Set.pure a).union (s.union t)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_union_left
Proof state before:
α : Sort u_1
p : Prop
a : α
s t : Set α
⊢ (s.insertIf a p).union t = (Set.pureIf a p).union (s.union t)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_union_right
Proof state before:
α : Sort u_1
p : Prop
a : α
s t : Set α
⊢ s.union (t.insertIf a p) = (s.union (Set.pureIf a p)).union t
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insertIf_union_right
Proof state before:
α : Sort u_1
p : Prop
a : α
s t : Set α
⊢ (s.union (Set.pureIf a p)).union t = ((Set.pureIf a p).union s).union t
Tactic:
rw [union_comm (Set.pureIf a p) s]
Proof state after:
no goals
Theorem: Set.insertIf_union_right
Proof state before:
α : Sort u_1
p : Prop
a : α
s t : Set α
⊢ ((Set.pureIf a p).union s).union t = (Set.pureIf a p).union (s.union t)
Tactic:
rw [union_assoc]
Proof state after:
no goals
Theorem: Set.insert_inter_left
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.insert a).inter t = ((Set.pure a).inter t).union (s.inter t)
Tactic:
rw [inter_distrib_right]
Proof state after:
no goals
Theorem: Set.insert_inter_left
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ ((Set.pure a).inter t).union (s.inter t) = (Set.pureIf a (a ∈ t)).union (s.inter t)
Tactic:
rw [pure_inter]
Proof state after:
no goals
Theorem: Set.insert_inter_right
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ s.inter (t.insert a) = (s.inter (Set.pure a)).union (s.inter t)
Tactic:
rw [inter_distrib_left]
Proof state after:
no goals
Theorem: Set.insert_inter_right
Proof state before:
α : Sort u_1
a : α
s t : Set α
⊢ (s.inter (Set.pure a)).union (s.inter t) = (Set.pureIf a (a ∈ s)).union (s.inter t)
Tactic:
rw [inter_pure]
Proof state after:
no goals
Theorem: Set.insertIf_inter_left
Proof state before:
α : Sort u_1
a : α
p : Prop
s t : Set α
⊢ (s.insertIf a p).inter t = ((Set.pureIf a p).inter t).union (s.inter t)
Tactic:
rw [inter_distrib_right]
Proof state after:
no goals
Theorem: Set.insertIf_inter_left
Proof state before:
α : Sort u_1
a : α
p : Prop
s t : Set α
⊢ ((Set.pureIf a p).inter t).union (s.inter t) = (Set.pureIf a (p ∧ a ∈ t)).union (s.inter t)
Tactic:
rw [pureIf_inter]
Proof state after:
no goals
Theorem: Set.insertIf_inter_right
Proof state before:
α : Sort u_1
a : α
p : Prop
s t : Set α
⊢ s.inter (t.insertIf a p) = (s.inter (Set.pureIf a p)).union (s.inter t)
Tactic:
rw [inter_distrib_left]
Proof state after:
no goals
Theorem: Set.insertIf_inter_right
Proof state before:
α : Sort u_1
a : α
p : Prop
s t : Set α
⊢ (s.inter (Set.pureIf a p)).union (s.inter t) = (Set.pureIf a (p ∧ a ∈ s)).union (s.inter t)
Tactic:
rw [inter_pureIf]
Proof state after:
no goals
Theorem: Set.insert_map
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
s : Set α
⊢ Set.map f (s.insert a) = (Set.map f (Set.pure a)).union (Set.map f s)
Tactic:
rw [union_map]
Proof state after:
no goals
Theorem: Set.insert_map
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
s : Set α
⊢ (Set.map f (Set.pure a)).union (Set.map f s) = (Set.pure (f a)).union (Set.map f s)
Tactic:
rw [Set.map_pure]
Proof state after:
no goals
Theorem: Set.insertIf_map
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
p : Prop
s : Set α
⊢ Set.map f (s.insertIf a p) = (Set.map f (Set.pureIf a p)).union (Set.map f s)
Tactic:
rw [union_map]
Proof state after:
no goals
Theorem: Set.insertIf_map
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
p : Prop
s : Set α
⊢ (Set.map f (Set.pureIf a p)).union (Set.map f s) = (Set.pureIf (f a) p).union (Set.map f s)
Tactic:
rw [Set.map_pureIf]
Proof state after:
no goals
Theorem: Set.insert_bind
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → Set β
a : α
s : Set α
⊢ (s.insert a).bind f = ((Set.pure a).bind f).union (s.bind f)
Tactic:
rw [union_bind]
Proof state after:
no goals
Theorem: Set.insert_bind
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → Set β
a : α
s : Set α
⊢ ((Set.pure a).bind f).union (s.bind f) = (f a).union (s.bind f)
Tactic:
rw [Set.pure_bind]
Proof state after:
no goals
Theorem: Set.insertIf_bind
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → Set β
a : α
p : Prop
s : Set α
⊢ (s.insertIf a p).bind f = ((Set.pureIf a p).bind f).union (s.bind f)
Tactic:
rw [union_bind]
Proof state after:
no goals
Theorem: Set.insertIf_bind
Proof state before:
α : Sort u_1
β : Sort u_2
f : α → Set β
a : α
p : Prop
s : Set α
⊢ ((Set.pureIf a p).bind f).union (s.bind f) = ((f a).inter (Set.const p)).union (s.bind f)
Tactic:
rw [Set.pureIf_bind]
Proof state after:
no goals