awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x : ↥T
m n : ℕ
⊢ take m x = take n x ↔ min m (↑x : List A).length = min n (↑x : List A).length

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x y x_1 : List A
a : A
h : Membership.mem (γ := Set (List A)) ((fun (x_2 : List A) ↦ x ++ x_2) ⁻¹' (↑T : Set (List A))) (x_1 ++ [a])
rwa rwa₁ rwa₂ rwa₃ : x ++ (x_1 ++ [a]) ∈ T
⊢ (fun (x_2 : List A) ↦ x ++ x_2) x_1 ++ [a] ∈ T

Tactic:
rwa [List.append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ subAt T x ↔ x ++ y ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
⊢ subAt T [] = T

Tactic:
rfl

Premises used: Set.Mem, setOf, List.append, Set.preimage, Descriptive.Tree.subAt, rfl
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∀ (x_1 : List A), x_1 ∈ subAt (subAt T x) y ↔ x_1 ∈ subAt T (x ++ y)
⊢ subAt (subAt T x) y = subAt T (x ++ y)

Tactic:
ext
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y x_1 : List A
⊢ x_1 ∈ subAt (subAt T x) y ↔ x_1 ∈ subAt T (x ++ y)

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x : List A
h : S ≤ T
⊢ subAt S x ≤ subAt T x

Tactic:
Set.preimage_mono h

Premises used: setOf, Set.preimage_mono, Set.preimage
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x_1 y : List A
n : ℕ
x : ↥T
⊢ List.drop n (↑x : List A) ∈ subAt T (↑(take n x) : List A)

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : y.length ≤ x.length
⊢ y ∈ pullSub T x ↔ y <+: x ∧ [] ∈ T

Tactic:
simp [pullSub, List.take_of_length_le hl, List.drop_eq_nil_iff.mpr hl]

Premises used: Iff.mpr, List.take_of_length_le, Descriptive.Tree.pullSub, List.drop_eq_nil_iff
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
right : y = x ++ List.drop x.length y
⊢ ∃ z ∈ T, y = x ++ z

Tactic:
use y.drop x.length, h2

Premises used: List.drop, List.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
right : List.take x.length y ++ List.drop x.length y = x ++ List.drop x.length y
⊢ y = x ++ List.drop x.length y

Tactic:
nth_rw 1 [← List.take_append_drop x.length y]

Premises used: List.take_append_drop, List.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ List.take x.length y ++ List.drop x.length y = x ++ List.drop x.length y

Tactic:
simpa [-List.take_append_drop, List.prefix_iff_eq_take, hl] using h1

Premises used: List.prefix_iff_eq_take, List.take_append_drop
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
⊢ (∃ z ∈ T, y = x ++ z) → y ∈ pullSub T x

Tactic:
simp +contextual [pullSub]

Premises used: Descriptive.Tree.pullSub
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ x ++ y ∈ pullSub T x ↔ y ∈ T

Tactic:
simp [mem_pullSub_long]

Premises used: Descriptive.Tree.mem_pullSub_long
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x : List A
⊢ x ∈ pullSub T x ↔ [] ∈ T

Tactic:
simpa using mem_pullSub_append (y := [])

Premises used: Descriptive.Tree.mem_pullSub_append
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
y₁ : ∀ (h : y ∈ pullSub (subAt T x) x), y ∈ (↑T : Set (List A))
⊢ y ∈ (↑(pullSub (subAt T x) x) : Set (List A)) → y ∈ (↑T : Set (List A))

Tactic:
(h : y ∈ pullSub _ x)
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
inl : ∀ (h' : y.length ≤ x.length), y ∈ (↑T : Set (List A))
inr : ∀ (h' : x.length ≤ y.length), y ∈ (↑T : Set (List A))
⊢ y ∈ (↑T : Set (List A))

Tactic:
rcases le_total y.length x.length with h' | h'

Premises used: le_total, List.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
⊢ y <+: x ∧ [] ∈ subAt T x

Tactic:
rw [mem_pullSub_short h'] at h

Premises used: Descriptive.Tree.mem_pullSub_short
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
h₁ : y <+: x ∧ [] ∈ subAt T x
⊢ y.length ≤ x.length

Tactic:
rw [mem_pullSub_short h'] at h

Premises used: Descriptive.Tree.mem_pullSub_short
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ x ∈ T

Tactic:
simpa using h.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ y ∈ (↑T : Set (List A))

Tactic:
exact mem_of_prefix h.1 (by simpa using h.2)

Premises used: Descriptive.Tree.mem_of_prefix, And.left
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : x.length ≤ y.length
⊢ ∃ z ∈ subAt T x, y = x ++ z

Tactic:
rw [mem_pullSub_long h'] at h

Premises used: Descriptive.Tree.mem_pullSub_long
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : x.length ≤ y.length
h₁ : ∃ z ∈ subAt T x, y = x ++ z
⊢ x.length ≤ y.length

Tactic:
rw [mem_pullSub_long h'] at h

Premises used: Descriptive.Tree.mem_pullSub_long
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∃ z ∈ subAt T x, y = x ++ z
h' : x.length ≤ y.length
inr : ∀ (w : List A) (h : w ∈ subAt T x) (h' : x.length ≤ (x ++ w).length), x ++ w ∈ (↑T : Set (List A))
⊢ y ∈ (↑T : Set (List A))

Tactic:
obtain ⟨_, h, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x w : List A
h : w ∈ subAt T x
h' : x.length ≤ (x ++ w).length
⊢ x ++ w ∈ (↑T : Set (List A))

Tactic:
h

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x w : List A
h : w ∈ subAt T x
h' : x.length ≤ (x ++ w).length
⊢ x ++ w ∈ (↑T : Set (List A))

Tactic:
exact h
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x : List A
h : ∀ (y : List A), y ∈ subAt (pullSub T x) x ↔ y ∈ T
⊢ subAt (pullSub T x) x = T

Tactic:
ext y
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ subAt (pullSub T x) x ↔ y ∈ T

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
h : S ≤ T
x : List A
⊢ pullSub S x ≤ pullSub T x

Tactic:
fun _ ⟨h1, h2⟩ ↦ ⟨h1, h h2⟩

Premises used: Membership.mem, Set.Subset, Descriptive.Tree.pullSub, And.intro, _private.0.Descriptive.Tree.pullSub_mono.match_1, Subtype.val
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x : List A
h : pullSub S x ≤ T
rw : subAt (pullSub S x) x ≤ subAt T x
⊢ S ≤ subAt T x

Tactic:
rw [← subAt_pullSub S x]

Premises used: Descriptive.Tree.subAt_pullSub
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x : List A
h : pullSub S x ≤ T
⊢ subAt (pullSub S x) x ≤ subAt T x

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S T : ↥(tree A)
x : List A
h : S ≤ subAt T x
⊢ pullSub S x ≤ pullSub (subAt T x) x

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
⊢ pullSub T [] = T

Tactic:
simp [pullSub]

Premises used: Descriptive.Tree.pullSub
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∀ (z : List A), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
⊢ pullSub (pullSub T y) x = pullSub T (x ++ y)

Tactic:
ext z
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
h : ∀ (hl : x.length ≤ z.length), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
h₁ : ∀ (hl : z.length ≤ x.length), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
rcases le_total x.length z.length with hl | hl

Premises used: le_total, List.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
pos : ∀ (hp : x <+: z), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
neg : ∀ (hp : ¬x <+: z), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
by_cases hp : x <+: z
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : x <+: z
pos : ∀ (z : List A) (hl : x.length ≤ (x ++ z).length), x ++ z ∈ pullSub (pullSub T y) x ↔ x ++ z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
obtain ⟨z, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ (x ++ z).length
⊢ x ++ z ∈ pullSub (pullSub T y) x ↔ x ++ z ∈ pullSub T (x ++ y)

Tactic:
simp [pullSub, List.take_add]

Premises used: List.take_add, Descriptive.Tree.pullSub
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
neg : z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)
neg₁ : z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right : List.drop (x ++ y).length z ∈ T
⊢ List.take x.length z <+: x

Tactic:
simpa [List.take_take] using h.take x.length

Premises used: List.IsPrefix.take, List.take_take, List.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right : List.drop (x ++ y).length z ∈ T
⊢ List.take x.length z <+: x

Tactic:
replace h := by simpa [List.take_take] using h.take x.length
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
neg : ∀ (h : List.take x.length z <+: x), List.drop x.length z ∈ pullSub T y → z ∈ pullSub T (x ++ y)
neg₁ : List.drop (x ++ y).length z ∈ T → ∀ (h : List.take x.length z <+: x), z ∈ pullSub (pullSub T y) x
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
constructor <;> intro ⟨h, _⟩ <;>
        [skip; replace h := by simpa [List.take_take] using h.take x.length]
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right : List.drop x.length z ∈ pullSub T y
⊢ (List.take x.length z).length = x.length

Tactic:
simpa
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right : List.drop x.length z ∈ pullSub T y
⊢ z ∈ pullSub T (x ++ y)

Tactic:
cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm

Premises used: List.IsPrefix.eq_of_length, Iff.mpr, List.prefix_iff_eq_take, Eq.symm
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
right : List.drop (x ++ y).length z ∈ T
h : List.take x.length z <+: x
⊢ (List.take x.length z).length = x.length

Tactic:
simpa
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
right : List.drop (x ++ y).length z ∈ T
h : List.take x.length z <+: x
⊢ z ∈ pullSub (pullSub T y) x

Tactic:
cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm

Premises used: List.IsPrefix.eq_of_length, Iff.mpr, List.prefix_iff_eq_take, Eq.symm
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ List.length.{u_1} (α := A) [] ≤ y.length

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
simp : z.length ≤ x.length + y.length
⊢ z.length ≤ (x ++ y).length

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ x.length + y.length

Tactic:
lia
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
h : z <+: x ∧ [] <+: y ∧ [] ∈ T ↔ z <+: x ++ y ∧ [] ∈ T
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
rw [mem_pullSub_short hl, mem_pullSub_short (by simp), mem_pullSub_short (by simp; lia)]

Premises used: Descriptive.Tree.mem_pullSub_short
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z <+: x ∧ [] <+: y ∧ [] ∈ T ↔ z <+: x ++ y ∧ [] ∈ T

Tactic:
simpa using fun _ ↦ (z.isPrefix_append_of_length hl).symm

Premises used: List.isPrefix_append_of_length, Iff.symm
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l : Lists' α true
⊢ (cons a l).toList = a :: l.toList

Tactic:
rfl

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

Tactic:
induction l
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (Lists α)) (toList (ofList [])) []

Tactic:
simp [*]
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
head : Lists α
tail : List (Lists α)
tail_ih : (ofList tail).toList = tail
⊢ (ofList (head :: tail)).toList = head :: tail

Tactic:
simp [*]
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
a : α
h : true = false
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : false = x) ↦ Lists' α x) (atom a) ⋯;
  ofList l'.toList = l'

Tactic:
cases h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
h : true = true
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) nil ⋯;
  ofList l'.toList = l'

Tactic:
simp
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b_1 b_2 : Bool
b : Lists' α b_2
a : Lists' α true
a_ih :
  ∀ (h : true = b_2),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b_2 = x) ↦ Lists' α x) b ⋯;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) a ⋯;
    ofList l'.toList = l'
h : true = true
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) (b.cons' a) ⋯;
  ofList l'.toList = l'

Tactic:
simpa [cons] using IH rfl

Premises used: Lists'.cons, rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
atom :
  ∀ (a : α) (h : true = false),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : false = x) ↦ Lists' α x) (Lists'.atom a) ⋯;
    ofList l'.toList = l'
nil :
  ∀ (h : true = true),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) Lists'.nil ⋯;
    ofList l'.toList = l'
cons' :
  ∀ {b : Bool} (b_1 : Lists' α b) (a : Lists' α true),
    (∀ (h : true = b),
        let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) b_1 ⋯;
        ofList l'.toList = l') →
      ∀
        (IH :
          ∀ (h : true = true),
            let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) a ⋯;
            ofList l'.toList = l')
        (h : true = true),
        let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) (b_1.cons' a) ⋯;
        ofList l'.toList = l'
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) l ⋯;
  ofList l'.toList = l'

Tactic:
induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl

Premises used: Lists'.atom, Lists'.cons', Lists'.cons, Lists'.nil
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
motive : Lists' α true → Sort u_2
ofList : (l : List (Lists α)) → motive (Lists'.ofList l)
l : Lists' α true
⊢ motive (Lists'.ofList l.toList) = motive l

Tactic:
simp
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
a : Lists α
l : Lists' α b
⊢ a ∈ l ↔ ∃ (a' : Lists α), a' ∈ l.toList ∧ a ~ a'

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l

Tactic:
simp [mem_def, or_and_right, exists_or]

Premises used: exists_or, Lists'.mem_def, or_and_right
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩

Premises used: Lists'.Subset.cons, _private.0.Lists'.cons_subset.match_1, HasSubset.Subset, Lists'.cons, Iff.intro
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
refine : ∀ (h : cons a l₁ ⊆ l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
generalize : ∀ (l₁' : Lists' α true) (h' : cons a l₁ = l₁') (h : l₁' ⊆ l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
generalize h' : Lists'.cons a l₁ = l₁' at h

Premises used: Lists'.cons
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : Lists'.cons a l₁ = l₁'
h : l₁' ⊆ l₂
nil : ∀ (h' : Lists'.cons a l₁ = Lists'.nil), a ∈ l₂ ∧ l₁ ⊆ l₂
cons :
  ∀ {a' a'_1 : Lists α} {l : Lists' α true} (e : a' ~ a'_1) (h' : Lists'.cons a l₁ = Lists'.cons a' l)
    (m : a'_1 ∈ l₂.toList) (s : l.Subset l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
obtain - | @⟨a', _, _, _, e, m, s⟩ := h
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = Lists'.nil
nil :
  ∀ (fst : Bool) (snd : Lists' α fst) (h' : cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = Lists'.nil),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
fst : Bool
snd : Lists' α fst
h' : cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = nil
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases h'
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'_1 : Lists α
l : Lists' α true
e : a' ~ a'_1
h' : Lists'.cons a l₁ = Lists'.cons a' l
m : a'_1 ∈ l₂.toList
s : l.Subset l₂
cons :
  ∀ (fst : Bool) (snd : Lists' α fst)
    (h' : Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = Lists'.cons a' l),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' a'_1 : Lists α
l : Lists' α true
e : a' ~ a'_1
m : a'_1 ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
h' : Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = Lists'.cons a' l
cons :
  ∀ (fst_1 : Bool) (snd_1 : Lists' α fst_1) (e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'_1)
    (h' :
      Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
        Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a'
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
l : Lists' α true
m : a' ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
fst_1 : Bool
snd_1 : Lists' α fst_1
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'
h' :
  cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
    cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'

Tactic:
cases h'
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
l : Lists' α true
m : a' ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
fst_1 : Bool
snd_1 : Lists' α fst_1
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'
h' :
  cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
    cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l
e₁ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'
⊢ l₁.Subset l₂

Tactic:
cases h'
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
m : a' ∈ l₂.toList
fst : Bool
snd : Lists' α fst
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'
s : l₁.Subset l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
⟨⟨_, m, e⟩, s⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
m : a' ∈ l₂.toList
fst : Bool
snd : Lists' α fst
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'
s : l₁.Subset l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
exact ⟨⟨_, m, e⟩, s⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂

Tactic:
Subset.nil

Premises used: Lists'.Subset.nil, Lists'.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂

Tactic:
exact Subset.nil

Premises used: Lists'.Subset.nil
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head :: tail ⊆ l₂
⊢ ofList (head :: tail) ⊆ ofList l₂

Tactic:
Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))

Premises used: Lists'.Subset.cons, Lists.Equiv.refl, List.subset_of_cons_subset, Lists'.ofList
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head :: tail ⊆ l₂
cons : head ∈ (ofList l₂).toList
⊢ ofList (head :: tail) ⊆ ofList l₂

Tactic:
refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))

Premises used: Lists'.Subset.cons, Lists.Equiv.refl, List.subset_of_cons_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head :: tail ⊆ l₂
⊢ head ∈ l₂ ∧ tail ⊆ l₂

Tactic:
simp only [List.cons_subset] at h

Premises used: List.cons_subset
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head ∈ l₂ ∧ tail ⊆ l₂
⊢ head ∈ (ofList l₂).toList

Tactic:
simp [h]