Theorem: Insert.mem_into_iff (LeanColls/Classes/Ops/Insert.lean)

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ into C' c ↔ x ∈ c
Tactic:
unfold into
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
have ⟨L, perm, h⟩ := Fold.ToList.fold_eq_fold_toList c
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
conv at h => ext; ext; ext; rw [← List.foldr_reverse]
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
replace perm := (List.reverse_perm ..).trans perm
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
perm : L.reverse.Perm (toList c)
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
perm : L.reverse.Perm (toList c)
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
generalize L.reverse = L' at perm h
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
clear L
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
conv => lhs; rw [h]
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L'
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Tactic:
clear h
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ c
Tactic:
conv => rhs; rw [Mem.ToList.mem_iff_mem_toList, ← perm.mem_iff]
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
perm : L'.Perm (toList c)
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Tactic:
clear perm
State after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'

State before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L' : List τ
⊢ x ∈ List.foldr (fun y x => insert x y) empty L' ↔ x ∈ L'
Tactic:
induction L' with
| nil =>
  simp [Mem.mem_empty]
| cons hd tl ih =>
  simp [Mem.mem_insert, ih]
State after:
no goals

State before:
case nil
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ List.foldr (fun y x => insert x y) empty [] ↔ x ∈ []
Tactic:
simp [Mem.mem_empty]
State after:
no goals

State before:
case cons
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
hd : τ
tl : List τ
ih : x ∈ List.foldr (fun y x => insert x y) empty tl ↔ x ∈ tl
⊢ x ∈ List.foldr (fun y x => insert x y) empty (hd :: tl) ↔ x ∈ hd :: tl
Tactic:
simp [Mem.mem_insert, ih]
State after:
no goals