[GOAL]
α : Type u_1
a : Lists α
l : Lists' α true
⊢ toList (cons a l) = a :: toList l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List (Lists α)
⊢ toList (ofList l) = l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
⊢ toList (ofList []) = []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α true
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b
[PROOFSTEP]
exact l
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α b) l;
  ofList (toList l') = l'
[PROOFSTEP]
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α b) l;
  ofList (toList l') = l'
[PROOFSTEP]
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α false) (atom a✝);
  ofList (toList l') = l'
[PROOFSTEP]

| atom => cases h
[GOAL]
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α false) (atom a✝);
  ofList (toList l') = l'
[PROOFSTEP]
cases h
[GOAL]
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) nil;
  ofList (toList l') = l'
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) nil;
  ofList (toList l') = l'
[PROOFSTEP]
simp
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a);
  ofList (toList l') = l'
[PROOFSTEP]

| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a);
  ofList (toList l') = l'
[PROOFSTEP]
intro l'
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
l' : Lists' α true := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a)
⊢ ofList (toList l') = l'
[PROOFSTEP]
simpa [cons] using IH rfl
[GOAL]
α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l
[PROOFSTEP]
simp [mem_def, or_and_right, exists_or]
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
generalize h' : Lists'.cons a l₁ = l₁' at h 
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases' h with l a' a'' l l' e m s
[GOAL]
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a
[GOAL]
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = nil
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases h'
[GOAL]
case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
h' : cons a l₁ = cons a' l
m : a'' ∈ toList l₂
s : Subset l l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a
[GOAL]
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = cons a' l
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a'
[GOAL]
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
l : Lists' α true
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
h' : cons { fst := fst✝¹, snd := snd✝¹ } l₁ = cons { fst := fst✝, snd := snd✝ } l
⊢ { fst := fst✝¹, snd := snd✝¹ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases h'
[GOAL]
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
m : a'' ∈ toList l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
s : Subset l₁ l₂
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
exact ⟨⟨_, m, e⟩, s⟩
[GOAL]
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂
[PROOFSTEP]
induction' l₁ with _ _ l₁_ih
[GOAL]
case nil
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂
[PROOFSTEP]
exact Subset.nil
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ ofList (head✝ :: tail✝) ⊆ ofList l₂
[PROOFSTEP]
refine' Subset.cons (Lists.Equiv.refl _) _ (l₁_ih (List.subset_of_cons_subset h))
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
[PROOFSTEP]
simp at h 
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ l ⊆ l
[PROOFSTEP]
rw [← Lists'.of_toList l]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ ofList (toList l)
[PROOFSTEP]
exact ofList_subset (List.Subset.refl _)
[GOAL]
α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil
[PROOFSTEP]
rw [← of_toList l]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ nil → ofList (toList l) = nil
[PROOFSTEP]
induction toList l
[GOAL]
case nil
α : Type u_1
l : Lists' α true
⊢ ofList [] ⊆ nil → ofList [] = nil
[PROOFSTEP]
intro h
[GOAL]
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
⊢ ofList (head✝ :: tail✝) ⊆ nil → ofList (head✝ :: tail✝) = nil
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil
[PROOFSTEP]
rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩
[GOAL]
α : Type u_1
a : Lists α
x✝ : Lists' α true
h : a ∈ toList nil
⊢ a ∈ x✝
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
a : Lists α
b✝ : Bool
a0 : Lists' α b✝
l0 l₂ : Lists' α true
s : cons' a0 l0 ⊆ l₂
h : a ∈ toList (cons' a0 l0)
⊢ a ∈ l₂
[PROOFSTEP]
cases' s with _ _ _ _ _ e m s
[GOAL]
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
h : a ∈ toList (cons' a✝.snd l0)
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
⊢ a ∈ l₂
[PROOFSTEP]
simp only [toList, Sigma.eta, List.find?, List.mem_cons] at h 
[GOAL]
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
h : a = a✝ ∨ a ∈ toList l0
⊢ a ∈ l₂
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case cons.inl
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
e : a ~ a'✝
⊢ a ∈ l₂
[PROOFSTEP]
exact ⟨_, m, e⟩
[GOAL]
case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
h : a ∈ toList l0
⊢ a ∈ l₂
[PROOFSTEP]
exact mem_of_subset' s h
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ l₁ ⊆ l₂
[PROOFSTEP]
rw [← of_toList l₁]
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ ofList (toList l₁) ⊆ l₂
[PROOFSTEP]
revert H
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂) → ofList (toList l₁) ⊆ l₂
[PROOFSTEP]
induction' toList l₁ with h t t_ih
[GOAL]
case nil
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ [] → a ∈ l₂) → ofList [] ⊆ l₂
[PROOFSTEP]
intro H
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
⊢ (∀ (a : Lists α), a ∈ h :: t → a ∈ l₂) → ofList (h :: t) ⊆ l₂
[PROOFSTEP]
intro H
[GOAL]
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ [] → a ∈ l₂
⊢ ofList [] ⊆ l₂
[PROOFSTEP]
exact Subset.nil
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ h :: t → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
[PROOFSTEP]
simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂
[PROOFSTEP]
exact cons_subset.2 ⟨H.1, t_ih H.2⟩
[GOAL]
α : Type u_1
l : List (Lists α)
⊢ toList (ofList l) = l
[PROOFSTEP]
simp [ofList, of']
[GOAL]
α : Type u_1
l : Lists' α true
x✝ : IsList { fst := true, snd := l }
⊢ ofList (toList { fst := true, snd := l }) = { fst := true, snd := l }
[PROOFSTEP]
simp_all [ofList, of']
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Lists α)
[PROOFSTEP]
unfold Lists
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq ((b : Bool) × Lists' α b)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : SizeOf α
⊢ SizeOf (Lists α)
[PROOFSTEP]
unfold Lists
[GOAL]
α : Type u_1
inst✝ : SizeOf α
⊢ SizeOf ((b : Bool) × Lists' α b)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ PProd ((l : Lists α) → C l) ((l : Lists' α true) → D l)
[PROOFSTEP]
suffices
  ∀ {b} (l : Lists' α b),
    PProd (C ⟨_, l⟩)
      (match b, l with
      | true, l => D l
      | false, _ => PUnit)
  by exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
this :
  {b : Bool} →
    (l : Lists' α b) →
      PProd (C { fst := b, snd := l })
        (match b, l with
        | true, l => D l
        | false, x => PUnit)
⊢ PProd ((l : Lists α) → C l) ((l : Lists' α true) → D l)
[PROOFSTEP]
exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ {b : Bool} →
    (l : Lists' α b) →
      PProd (C { fst := b, snd := l })
        (match b, l with
        | true, l => D l
        | false, x => PUnit)
[PROOFSTEP]
intros b l
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
⊢ PProd (C { fst := b, snd := l })
    (match b, l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
induction' l with a b a l IH₁ IH
[GOAL]
case atom
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
a : α
⊢ PProd (C { fst := false, snd := Lists'.atom a })
    (match false, Lists'.atom a with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C0 _, ⟨⟩⟩
[GOAL]
case nil
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
⊢ PProd (C { fst := true, snd := Lists'.nil })
    (match true, Lists'.nil with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C1 _ D0, D0⟩
[GOAL]
case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b✝ b : Bool
a : Lists' α b
l : Lists' α true
IH₁ :
  PProd (C { fst := b, snd := a })
    (match b, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd (C { fst := true, snd := l })
    (match true, l with
    | true, l => D l
    | false, x => PUnit)
⊢ PProd (C { fst := true, snd := Lists'.cons' a l })
    (match true, Lists'.cons' a l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
[GOAL]
case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b✝ b : Bool
a : Lists' α b
l : Lists' α true
IH₁ :
  PProd (C { fst := b, snd := a })
    (match b, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd (C { fst := true, snd := l })
    (match true, l with
    | true, l => D l
    | false, x => PUnit)
this : D (Lists'.cons' a l)
⊢ PProd (C { fst := true, snd := Lists'.cons' a l })
    (match true, Lists'.cons' a l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C1 _ this, this⟩
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂
[GOAL]
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
[PROOFSTEP]
simp [Lists'.Subset.refl]
[GOAL]
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : Lists'.Subset l₁ l₂
h₂ : Lists'.Subset l₂ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
exact ⟨h₁, h₂⟩
[GOAL]
α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
a : α
⊢ atom a = atom a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂ <;> [rfl; exact Equiv.antisymm h₂ h₁]
[GOAL]
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂
[GOAL]
case refl
α : Type u_1
l₁ : Lists α
⊢ l₁ ~ l₁
[PROOFSTEP]
rfl
[GOAL]
case antisymm
α : Type u_1
l₁✝ l₂✝ : Lists' α true
h₁ : Lists'.Subset l₁✝ l₂✝
h₂ : Lists'.Subset l₂✝ l₁✝
⊢ { fst := true, snd := l₂✝ } ~ { fst := true, snd := l₁✝ }
[PROOFSTEP]
exact Equiv.antisymm h₂ h₁
[GOAL]
α : Type u_1
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
let trans := fun l₁ : Lists α => ∀ ⦃l₂ l₃⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : PProd (∀ (l₁ : Lists α), trans l₁) (∀ (l : Lists' α true) (l' : Lists α), l' ∈ Lists'.toList l → trans l')
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
exact this.1
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ PProd (∀ (l₁ : Lists α), trans l₁) (∀ (l : Lists' α true) (l' : Lists α), l' ∈ Lists'.toList l → trans l')
[PROOFSTEP]
apply inductionMut
[GOAL]
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : α), trans (atom a)
[PROOFSTEP]
intro a l₂ l₃ h₁ h₂
[GOAL]
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃
[PROOFSTEP]
rwa [← equiv_atom.1 h₁] at h₂ 
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l') → trans (of' l)
[PROOFSTEP]
intro l₁ IH l₂ l₃ h₁ h₂
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
have h₁' := h₁
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
h₁' : of' l₁ ~ l₂
⊢ of' l₁ ~ l₃
[PROOFSTEP]
have h₂' := h₂
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
h₁' : of' l₁ ~ l₂
h₂' : l₂ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
cases' h₁ with _ _ l₂
[GOAL]
case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₃ : Lists α
h₂ : of' l₁ ~ l₃
h₁' : of' l₁ ~ of' l₁
h₂' : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
exact h₂
[GOAL]
case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₃ : Lists α
l₂ : Lists' α true
a✝¹ : Lists'.Subset l₁ l₂
a✝ : Lists'.Subset l₂ l₁
h₂ : { fst := true, snd := l₂ } ~ l₃
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
h₂' : { fst := true, snd := l₂ } ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
cases' h₂ with _ _ l₃
[GOAL]
case C1.antisymm.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝¹ : Lists'.Subset l₁ l₂
a✝ : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₂ }
⊢ of' l₁ ~ { fst := true, snd := l₂ }
[PROOFSTEP]
exact h₁'
[GOAL]
case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
cases' Equiv.antisymm_iff.1 h₁' with hl₁ hr₁
[GOAL]
case C1.antisymm.antisymm.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
cases' Equiv.antisymm_iff.1 h₂' with hl₂ hr₂
[GOAL]
case C1.antisymm.antisymm.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
apply Equiv.antisymm_iff.2
[GOAL]
case C1.antisymm.antisymm.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₁ ⊆ l₃ ∧ l₃ ⊆ l₁
[PROOFSTEP]
constructor
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₁ ⊆ l₃
[PROOFSTEP]
apply Lists'.subset_def.2
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₃ ⊆ l₁
[PROOFSTEP]
apply Lists'.subset_def.2
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l₁ → a ∈ l₃
[PROOFSTEP]
intro a₁ m₁
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
⊢ a₁ ∈ l₃
[PROOFSTEP]
rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.left.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₁₂ : a₁ ~ a₂
⊢ a₁ ∈ l₃
[PROOFSTEP]
rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.left.intro.intro.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₁₂ : a₁ ~ a₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
e₂₃ : a₂ ~ a₃
⊢ a₁ ∈ l₃
[PROOFSTEP]
exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l₃ → a ∈ l₁
[PROOFSTEP]
intro a₃ m₃
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
⊢ a₃ ∈ l₁
[PROOFSTEP]
rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₃₂ : a₃ ~ a₂
⊢ a₃ ∈ l₁
[PROOFSTEP]
rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right.intro.intro.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₃₂ : a₃ ~ a₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁
[PROOFSTEP]
exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩
[GOAL]
case D0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (l' : Lists α), l' ∈ Lists'.toList Lists'.nil → trans l'
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a →
      (∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l') →
        ∀ (l' : Lists α), l' ∈ Lists'.toList (Lists'.cons a l) → trans l'
[PROOFSTEP]
intro a l IH₁ IH
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ (l' : Lists α), l' ∈ Lists'.toList (Lists'.cons a l) → trans l'
[PROOFSTEP]
simp only [Lists'.toList, Sigma.eta, List.find?, List.mem_cons, forall_eq_or_imp]
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ (∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃) ∧
    ∀ (a : Lists α), a ∈ Lists'.toList l → ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
constructor
[GOAL]
case D1.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
intros l₂ l₃ h₁ h₂
[GOAL]
case D1.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
l₂ l₃ : Lists α
h₁ : a ~ l₂
h₂ : l₂ ~ l₃
⊢ a ~ l₃
[PROOFSTEP]
exact IH₁ h₁ h₂
[GOAL]
case D1.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l → ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
intros a h₁ l₂ l₃ h₂ h₃
[GOAL]
case D1.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a✝ : Lists α
l : Lists' α true
IH₁ : trans a✝
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
a : Lists α
h₁ : a ∈ Lists'.toList l
l₂ l₃ : Lists α
h₂ : a ~ l₂
h₃ : l₂ ~ l₃
⊢ a ~ l₃
[PROOFSTEP]
exact IH _ h₁ h₂ h₃
[GOAL]
α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l
[PROOFSTEP]
cases l
[GOAL]
case atom
α : Type u_1
a✝ : α
⊢ 0 < sizeOf (Lists'.atom a✝)
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
case nil
α : Type u_1
⊢ 0 < sizeOf Lists'.nil
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
case cons'
α : Type u_1
b✝ : Bool
a✝¹ : Lists' α b✝
a✝ : Lists' α true
⊢ 0 < sizeOf (Lists'.cons' a✝¹ a✝)
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf { fst := b, snd := a } < sizeOf (Lists'.cons' a l)
[PROOFSTEP]
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
[GOAL]
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
[PROOFSTEP]
apply sizeof_pos
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α false
⊢ { fst := false, snd := l₁ } ~ { fst := false, snd := l₂ } ↔ l₁ = l₂
[PROOFSTEP]
cases l₁
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } ~ { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
apply equiv_atom.trans
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ atom a✝ = { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
simp [atom]
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
constructor
[GOAL]
case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ } → Lists'.atom a✝ = l₂
[PROOFSTEP]
rintro ⟨rfl⟩
[GOAL]
case atom.mp.refl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ Lists'.atom a✝ = Lists'.atom a✝
[PROOFSTEP]
rfl
[GOAL]
case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ }
[PROOFSTEP]
rintro ⟨rfl⟩
[GOAL]
case atom.mpr.refl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := Lists'.atom a✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α false
l₂ : Lists' α true
⊢ ¬{ fst := false, snd := l₁ } ~ { fst := true, snd := l₂ }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α true
l₂ : Lists' α false
⊢ ¬{ fst := true, snd := l₁ } ~ { fst := false, snd := l₂ }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
haveI : Decidable (l₁ ⊆ l₂) :=
  have :
    SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ < SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) :=
    by decreasing_tactic
  Subset.decidable l₁ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf { fst := true, snd := l₁ } + sizeOf { fst := true, snd := l₂ }
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
haveI : Decidable (l₂ ⊆ l₁) :=
  have :
    SizeOf.sizeOf l₂ + SizeOf.sizeOf l₁ < SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) :=
    by decreasing_tactic
  Subset.decidable l₂ l₁
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ sizeOf l₂ + sizeOf l₁ < sizeOf { fst := true, snd := l₁ } + sizeOf { fst := true, snd := l₂ }
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this✝ : Decidable (l₁ ⊆ l₂)
this : Decidable (l₂ ⊆ l₁)
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
exact decidable_of_iff' _ Equiv.antisymm_iff
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
haveI :=
  have : sizeOf (⟨b, a⟩ : Lists α) < 1 + 1 + sizeOf a + sizeOf l₁ := by simp [sizeof_pos]
  mem.decidable ⟨b, a⟩ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf { fst := b, snd := a } < 1 + 1 + sizeOf a + sizeOf l₁
[PROOFSTEP]
simp [sizeof_pos]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable ({ fst := b, snd := a } ∈ l₂)
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
haveI :=
  have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ < SizeOf.sizeOf (Lists'.cons' a l₁) + SizeOf.sizeOf l₂ := by
    decreasing_tactic
  Subset.decidable l₁ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable ({ fst := b, snd := a } ∈ l₂)
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf (Lists'.cons' a l₁) + sizeOf l₂
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this✝ : Decidable ({ fst := b, snd := a } ∈ l₂)
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
exact decidable_of_iff' _ (@Lists'.cons_subset _ ⟨_, _⟩ _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
⊢ ¬a ∈ Lists'.nil
[PROOFSTEP]
rintro ⟨_, ⟨⟩, _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
haveI :=
  have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
  Equiv.decidable a ⟨_, b⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ sizeOf { fst := b✝, snd := b } < 1 + 1 + sizeOf b + sizeOf l₂
[PROOFSTEP]
simp [sizeof_pos]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : Decidable (a ~ { fst := b✝, snd := b })
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
haveI :=
  have : SizeOf.sizeOf a + SizeOf.sizeOf l₂ < SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
    decreasing_tactic
  mem.decidable a l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : Decidable (a ~ { fst := b✝, snd := b })
⊢ sizeOf a + sizeOf l₂ < sizeOf a + sizeOf (Lists'.cons' b l₂)
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
refine' decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ a ∈ Lists'.cons' b l₂ ↔ a ~ { fst := b✝, snd := b } ∨ a ∈ l₂
[PROOFSTEP]
rw [← Lists'.mem_cons]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ a ∈ Lists'.cons' b l₂ ↔ a ∈ Lists'.cons { fst := b✝, snd := b } l₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Finsets α)
[PROOFSTEP]
unfold Finsets
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Quotient Lists.instSetoidLists)
[PROOFSTEP]
exact (Quotient.decidableEq (d := fun _ _ => Lists.Equiv.decidable _ _))
