awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
nil : ∀ (h : [] ⊆ l₂), ofList [] ⊆ ofList l₂
cons :
  ∀ (head : Lists α) (tail : List (Lists α)) (l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂)
    (h : head :: tail ⊆ l₂), ofList (head :: tail) ⊆ ofList l₂
⊢ ofList l₁ ⊆ ofList l₂

Tactic:
induction l₁ with
  | nil => exact Subset.nil
  | cons _ _ l₁_ih =>
    refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
    simp only [List.cons_subset] at h; simp [h]

Premises used: Lists'.cons, List.cons_subset, Lists'.Subset.nil, Lists'.nil
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
rw : ofList l.toList ⊆ ofList l.toList
⊢ l ⊆ l

Tactic:
rw [← Lists'.of_toList l]

Premises used: Lists'.of_toList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList

Tactic:
ofList_subset (List.Subset.refl _)

Premises used: List.Subset.refl, Lists'.ofList_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList

Tactic:
exact ofList_subset (List.Subset.refl _)

Premises used: List.Subset.refl, Lists'.ofList_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
rw : ofList l.toList ⊆ nil → ofList l.toList = nil
⊢ l ⊆ nil → l = nil

Tactic:
rw [← of_toList l]

Premises used: Lists'.of_toList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
nil :
  HasSubset.Subset.{u_1} (α := Lists' α true) (ofList []) Lists'.nil →
    Eq.{u_1 + 1} (α := Lists' α true) (ofList []) Lists'.nil
cons :
  ∀ (head : Lists α) (tail : List (Lists α)),
    (ofList tail ⊆ Lists'.nil → ofList tail = Lists'.nil) →
      ofList (head :: tail) ⊆ Lists'.nil → ofList (head :: tail) = Lists'.nil
⊢ ofList l.toList ⊆ Lists'.nil → ofList l.toList = Lists'.nil

Tactic:
induction toList l

Premises used: Lists'.toList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
h : HasSubset.Subset.{u_1} (α := Lists' α true) (ofList []) nil
⊢ Eq.{u_1 + 1} (α := Lists' α true) (ofList []) nil

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : 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

Tactic:
rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩

Premises used: Iff.mp, Lists'.cons_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
x : Lists' α true
h : Membership.mem (γ := List (Lists α)) (toList nil) a
⊢ a ∈ x

Tactic:
cases h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
b : Bool
a0 : Lists' α b
l0 l₂ : Lists' α true
s : a0.cons' l0 ⊆ l₂
h : a ∈ (a0.cons' l0).toList
cons :
  ∀ {a_1 a' : Lists α} (e : a_1 ~ a') (h : a ∈ (a_1.snd (β := fun (b : Bool) ↦ Lists' α b).cons' l0).toList)
    (m : a' ∈ l₂.toList) (s : l0.Subset l₂), a ∈ l₂
⊢ a ∈ l₂

Tactic:
obtain - | ⟨e, m, s⟩ := s
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
h : a ∈ (a_1.snd (β := fun (b : Bool) ↦ Lists' α b).cons' l0).toList
m : a' ∈ l₂.toList
s : l0.Subset l₂
⊢ a = a_1 ∨ a ∈ l0.toList

Tactic:
simp only [toList, Sigma.eta, List.mem_cons] at h

Premises used: Lists'.toList, Sigma.eta, List.mem_cons
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
m : a' ∈ l₂.toList
s : l0.Subset l₂
h : a = a_1 ∨ a ∈ l0.toList
cons : ∀ (e : a ~ a'), a ∈ l₂
cons₁ : ∀ (h : a ∈ l0.toList), a ∈ l₂
⊢ a ∈ l₂

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a' : Lists α
m : a' ∈ l₂.toList
s : l0.Subset l₂
e : a ~ a'
⊢ a ∈ l₂

Tactic:
⟨_, m, e⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a' : Lists α
m : a' ∈ l₂.toList
s : l0.Subset l₂
e : a ~ a'
⊢ a ∈ l₂

Tactic:
exact ⟨_, m, e⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
m : a' ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂

Tactic:
mem_of_subset' s h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
m : a' ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂

Tactic:
exact mem_of_subset' s h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂
ofList : ∀ (l₁ : List (Lists α)) (H : ∀ (a : Lists α), a ∈ (Lists'.ofList l₁).toList → a ∈ l₂), Lists'.ofList l₁ ⊆ l₂
⊢ l₁ ⊆ l₂

Tactic:
induction l₁ using recOfList with | _ l₁
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
H : ∀ (a : Lists α), Membership.mem (γ := List (Lists α)) (toList (ofList [])) a → a ∈ l₂
⊢ ofList [] ⊆ l₂

Tactic:
Subset.nil

Premises used: Lists'.Subset.nil, Lists'.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
H : ∀ (a : Lists α), Membership.mem (γ := List (Lists α)) (toList (ofList [])) a → a ∈ l₂
⊢ ofList [] ⊆ l₂

Tactic:
exact Subset.nil

Premises used: Lists'.Subset.nil
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (ofList t).toList → a ∈ l₂), ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ (ofList (h :: t)).toList → a ∈ l₂
⊢ ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂

Tactic:
simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *

Premises used: Lists'.toList_cons, forall_eq_or_imp, Lists'.to_ofList, List.mem_cons, Lists'.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (ofList t).toList → a ∈ l₂), ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ (ofList (h :: t)).toList → a ∈ l₂
t_ih₁ : ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂
⊢ h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂

Tactic:
simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *

Premises used: Lists'.toList_cons, forall_eq_or_imp, Lists'.to_ofList, List.mem_cons, Lists'.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂

Tactic:
cons_subset.2 ⟨H.1, t_ih H.2⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Lists'.cons_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂

Tactic:
exact cons_subset.2 ⟨H.1, t_ih H.2⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Lists'.cons_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : Lists' α true
l₁ : List (Lists α)
H : ∀ (a : Lists α), a ∈ (Lists'.ofList l₁).toList → a ∈ l₂
ofList :
  ∀ (H : ∀ (a : Lists α), Membership.mem (γ := List (Lists α)) (toList (Lists'.ofList [])) a → a ∈ l₂),
    Lists'.ofList [] ⊆ l₂
ofList₁ :
  ∀ (h : Lists α) (t : List (Lists α))
    (t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (Lists'.ofList t).toList → a ∈ l₂), Lists'.ofList t ⊆ l₂)
    (H : ∀ (a : Lists α), a ∈ (Lists'.ofList (h :: t)).toList → a ∈ l₂), Lists'.ofList (h :: t) ⊆ l₂
⊢ Lists'.ofList l₁ ⊆ l₂

Tactic:
induction l₁ with
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩

Premises used: Lists'.toList_cons, forall_eq_or_imp, Lists'.cons, Lists'.Subset.nil, Lists'.to_ofList, List.mem_cons, Lists'.ofList, Lists'.nil
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : List (Lists α)
⊢ (ofList l).IsList

Tactic:
Eq.refl _

Premises used: Eq.refl, Lists.IsList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : List (Lists α)
⊢ (ofList l).toList = l

Tactic:
simp [ofList, of']

Premises used: Lists.of', Lists.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
h : IsList (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l)
⊢ ofList (toList (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l)) =
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l

Tactic:
simp_all [ofList, of']

Premises used: Lists.of', Lists.ofList
-- Module: Mathlib.SetTheory.Lists
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.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
        (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
        | true, l => D l
        | false, x => PUnit)
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
-- Module: Mathlib.SetTheory.Lists
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)
suffices :
  {b : Bool} →
    (l : Lists' α b) →
      PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
        (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
        | true, l => D l
        | false, x => PUnit)
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
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⟩
-- Module: Mathlib.SetTheory.Lists
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
a : α
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) false, Lists'.atom a with
    | true, l => D l
    | false, x => PUnit)

Tactic:
exact ⟨C0 _, ⟨⟩⟩
-- Module: Mathlib.SetTheory.Lists
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
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true Lists'.nil))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, Lists'.nil with
    | true, l => D l
    | false, x => PUnit)

Tactic:
exact ⟨C1 _ D0, D0⟩
-- Module: Mathlib.SetTheory.Lists
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 b_1 : Bool
a : Lists' α b_1
l : Lists' α true
IH₁ :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 a))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b_1, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, l with
    | true, l => D l
    | false, x => PUnit)
cons' :
  (this : D (a.cons' l)) →
    PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
      (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
      | true, l => D l
      | false, x => PUnit)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
    | true, l => D l
    | false, x => PUnit)

Tactic:
have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
-- Module: Mathlib.SetTheory.Lists
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 b_1 : Bool
a : Lists' α b_1
l : Lists' α true
IH₁ :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 a))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b_1, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, l with
    | true, l => D l
    | false, x => PUnit)
this : D (a.cons' l)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
    | true, l => D l
    | false, x => PUnit)

Tactic:
exact ⟨C1 _ this, this⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (Lists.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
atom :
  (a : α) →
    PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)))
      (match (motive := (b : Bool) → Lists' α b → Sort u_3) false, Lists'.atom a with
      | true, l => D l
      | false, x => PUnit)
nil :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true Lists'.nil))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, Lists'.nil with
    | true, l => D l
    | false, x => PUnit)
cons' :
  {b : Bool} →
    (a : Lists' α b) →
      (l : Lists' α true) →
        (IH₁ :
            PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a))
              (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, a with
              | true, l => D l
              | false, x => PUnit)) →
          (IH :
              PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l))
                (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, l with
                | true, l => D l
                | false, x => PUnit)) →
            PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
              (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
              | true, l => D l
              | false, x => PUnit)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
    | true, l => D l
    | false, x => PUnit)

Tactic:
induction l with
  | atom => exact ⟨C0 _, ⟨⟩⟩
  | nil => exact ⟨C1 _ D0, D0⟩
  | cons' a l IH₁ IH =>
    have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
    exact ⟨C1 _ this, this⟩

Premises used: Lists.atom
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
⟨fun h => ?_, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩

Premises used: _private.0.Lists.Equiv.antisymm_iff.match_1, Lists.of', Lists.Equiv.antisymm, Iff.intro, Lists.Equiv
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
refine : ∀ (h : of' l₁ ~ of' l₂), l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
refl : l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
antisymm : ∀ (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁), l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

Tactic:
simp [Lists'.Subset.refl]

Premises used: Lists'.Subset.refl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : α
l : Lists α
h : atom a ~ l
refl : atom a = atom a
⊢ atom a = l

Tactic:
cases h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : α
⊢ atom a = atom a

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
refl : l₁ ~ l₁
antisymm :
  ∀ {l₁ l₂ : Lists' α true} (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁
⊢ l₂ ~ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ : Lists α
⊢ l₁ ~ l₁

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁

Tactic:
Equiv.antisymm h₂ h₁

Premises used: Lists.Equiv.antisymm
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁

Tactic:
exact Equiv.antisymm h₂ h₁

Premises used: Lists.Equiv.antisymm
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
refl : l₁ ~ l₁
antisymm :
  ∀ {l₁ l₂ : Lists' α true} (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁
refl₁ : l₁ ~ l₁
antisymm₁ :
  ∀ {l₁ l₂ : Lists' α true} (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁
⊢ l₂ ~ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h <;> [rfl; exact Equiv.antisymm h₂ h₁]
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
this.1

Premises used: PProd.fst
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
exact this.1

Premises used: PProd.fst
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
suffices : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
C0 : ∀ (a : α), trans (atom a)
C1 : ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)
D0 : ∀ (l' : Lists α), Membership.mem (γ := List (Lists α)) (Lists'.toList Lists'.nil) l' → trans l'
D1 :
  ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'

Tactic:
apply inductionMut

Premises used: Lists.inductionMut
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
C0 C0₁ C0₂ C0₃ : ∀ (h₂ : atom a ~ l₃), atom a ~ l₃
⊢ atom a ~ l₃

Tactic:
rwa [← equiv_atom.1 h₁] at h₂

Premises used: Iff.mp, Lists.equiv_atom
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
C1 : ∀ (h₁ : of' l₁ ~ of' l₁) (h₂ : of' l₁ ~ l₃), of' l₁ ~ l₃
C1₁ :
  ∀ {l₂ : Lists' α true} (l₂_1 : l₁.Subset l₂),
    l₂.Subset l₁ →
      ∀ (h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
        (h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ l₃), of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
obtain - | l₂ := id h₁

Premises used: id
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
h₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
exact h₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ l₃
C1 :
  ∀
    (h₂ :
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1),
    of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
C1₁ :
  ∀ {l₂ : Lists' α true} (l₃ : l₂_1.Subset l₂),
    l₂.Subset l₂_1 →
      ∀
        (h₂ :
          Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂),
        of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂
⊢ of' l₁ ~ l₃

Tactic:
obtain - | l₃ := id h₂

Premises used: id
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1

Tactic:
h₁
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1

Tactic:
exact h₁