awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
⊢ l₁ ⊆ l₂_1

Tactic:
obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁

Premises used: Iff.mp, Lists.Equiv.antisymm_iff
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
⊢ l₂_1 ⊆ l₁

Tactic:
obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁

Premises used: Iff.mp, Lists.Equiv.antisymm_iff
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
⊢ l₂_1 ⊆ l₂_2

Tactic:
obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂

Premises used: Iff.mp, Lists.Equiv.antisymm_iff
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
⊢ l₂_2 ⊆ l₂_1

Tactic:
obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂

Premises used: Iff.mp, Lists.Equiv.antisymm_iff
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
C1 : l₁ ⊆ l₂_2 ∧ l₂_2 ⊆ l₁
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2

Tactic:
apply Equiv.antisymm_iff.2

Premises used: Iff.mpr, Lists.Equiv.antisymm_iff
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
C1 : l₁ ⊆ l₂_2
C1₁ : l₂_2 ⊆ l₁
⊢ l₁ ⊆ l₂_2 ∧ l₂_2 ⊆ l₁

Tactic:
constructor
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
C1 : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂_2
⊢ l₁ ⊆ l₂_2

Tactic:
apply Lists'.subset_def.2

Premises used: Iff.mpr, Lists'.subset_def
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
C1 : ∀ (a : Lists α), a ∈ l₂_2.toList → a ∈ l₁
⊢ l₂_2 ⊆ l₁

Tactic:
apply Lists'.subset_def.2

Premises used: Iff.mpr, Lists'.subset_def
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
C1 : ∀ (a₂ : Lists α) (m₂ : a₂ ∈ l₂_1.toList) (e₁₂ : a₁ ~ a₂), a₁ ∈ l₂_2
⊢ a₁ ∈ l₂_2

Tactic:
rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩

Premises used: Lists'.mem_of_subset'
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₁₂ : a₁ ~ a₂
C1 : ∀ (a₃ : Lists α) (m₃ : a₃ ∈ l₂_2.toList) (e₂₃ : a₂ ~ a₃), a₁ ∈ l₂_2
⊢ a₁ ∈ l₂_2

Tactic:
rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩

Premises used: Lists'.mem_of_subset'
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₁₂ : a₁ ~ a₂
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
e₂₃ : a₂ ~ a₃
⊢ a₁ ∈ l₂_2

Tactic:
⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩

Premises used: And.intro, Exists.intro
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₁₂ : a₁ ~ a₂
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
e₂₃ : a₂ ~ a₃
⊢ a₁ ∈ l₂_2

Tactic:
exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
C1 : ∀ (a₂ : Lists α) (m₂ : a₂ ∈ l₂_1.toList) (e₃₂ : a₃ ~ a₂), a₃ ∈ l₁
⊢ a₃ ∈ l₁

Tactic:
rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩

Premises used: Lists'.mem_of_subset'
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₃₂ : a₃ ~ a₂
C1 : ∀ (a₁ : Lists α) (m₁ : a₁ ∈ l₁.toList) (e₂₁ : a₂ ~ a₁), a₃ ∈ l₁
⊢ a₃ ∈ l₁

Tactic:
rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩

Premises used: Lists'.mem_of_subset'
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₃₂ : a₃ ~ a₂
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁

Tactic:
⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩

Premises used: Lists.Equiv.symm, And.intro, Exists.intro
-- 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
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
a₃ : Lists α
m₃ : a₃ ∈ l₂_2.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂_1.toList
e₃₂ : a₃ ~ a₂
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁

Tactic:
exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩
-- 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 : Lists α
l : Lists' α true
IH₁ : trans a
IH₂ : ∀ (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
simpa using ⟨IH₁, IH₂⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
l : Lists' α b
atom : ∀ (a : α), 0 < sizeOf (Lists'.atom a)
nil : 0 < sizeOf.{u_1 + 1} (α := Lists' α true) Lists'.nil
cons' : ∀ {b : Bool} (a : Lists' α b) (a_1 : Lists' α true), 0 < sizeOf (a.cons' a_1)
⊢ 0 < sizeOf l

Tactic:
cases l
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
a : α
⊢ 0 < sizeOf (Lists'.atom a)

Tactic:
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec,
    true_or, add_pos_iff, zero_lt_one]

Premises used: Lists'.nil.sizeOf_spec, true_or, zero_lt_one, Lists'.cons'.sizeOf_spec, Lists'.atom.sizeOf_spec, add_pos_iff
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
⊢ 0 < sizeOf.{u_1 + 1} (α := Lists' α true) Lists'.nil

Tactic:
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec,
    true_or, add_pos_iff, zero_lt_one]

Premises used: Lists'.nil.sizeOf_spec, true_or, zero_lt_one, Lists'.cons'.sizeOf_spec, Lists'.atom.sizeOf_spec, add_pos_iff
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
a : Lists' α b
a_1 : Lists' α true
⊢ 0 < sizeOf (a.cons' a_1)

Tactic:
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec,
    true_or, add_pos_iff, zero_lt_one]

Premises used: Lists'.nil.sizeOf_spec, true_or, zero_lt_one, Lists'.cons'.sizeOf_spec, Lists'.atom.sizeOf_spec, add_pos_iff
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
simp : 0 < sizeOf l
⊢ sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a) < sizeOf (a.cons' l)

Tactic:
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]

Premises used: lt_add_iff_pos_right, Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l

Tactic:
apply sizeof_pos

Premises used: Lists.sizeof_pos
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α false
atom :
  ∀ (a : α),
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) ~
        Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
      Lists'.atom a = l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔ l₁ = l₂

Tactic:
cases l₁
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : Lists' α false
a : α
atom : Lists.atom a = Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔ Lists'.atom a = l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) ~
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂

Tactic:
apply equiv_atom.trans

Premises used: Iff.trans, Lists.equiv_atom
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : Lists' α false
a : α
atom :
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ →
    Lists'.atom a = l₂
atom₁ :
  Lists'.atom a = l₂ →
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false l₂ ↔
    Lists'.atom a = l₂

Tactic:
constructor
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Lists'.atom a = Lists'.atom a

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a) =
    Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
decreasing_tactic decreasing_tactic₁ decreasing_tactic₂ decreasing_tactic₃ decreasing_tactic₄ decreasing_tactic₅ :
  sizeOf l₁ + sizeOf l₂ < 2 + sizeOf l₁ + (2 + sizeOf l₂)
⊢ sizeOf l₁ + sizeOf l₂ <
    sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁) +
      sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)

Tactic:
decreasing_tactic
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
haveI :
  (this : Decidable (l₁ ⊆ l₂)) →
    Decidable
      (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
⊢ Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)

Tactic:
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₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
decreasing_tactic decreasing_tactic₁ decreasing_tactic₂ decreasing_tactic₃ decreasing_tactic₄ decreasing_tactic₅ :
  sizeOf l₂ + sizeOf l₁ < 2 + sizeOf l₁ + (2 + sizeOf l₂)
⊢ sizeOf l₂ + sizeOf l₁ <
    sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁) +
      sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)

Tactic:
decreasing_tactic
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
haveI :
  (this : Decidable (l₂ ⊆ l₁)) →
    Decidable
      (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
⊢ Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)

Tactic:
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₁
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : Lists' α true
this_1 : Decidable (l₁ ⊆ l₂)
this : Decidable (l₂ ⊆ l₁)
⊢ Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)

Tactic:
exact decidable_of_iff' _ Equiv.antisymm_iff

Premises used: decidable_of_iff', Lists.Equiv.antisymm_iff
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a) < HAdd.hAdd (α := ℕ) 1 1 + sizeOf a + sizeOf l₁

Tactic:
simp [sizeof_pos]

Premises used: Lists.sizeof_pos
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
haveI : (this : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)) → Decidable (a.cons' l₁ ⊆ l₂)
⊢ Decidable (a.cons' l₁ ⊆ l₂)

Tactic:
haveI :=
        have : sizeOf (⟨b, a⟩ : Lists α) < 1 + 1 + sizeOf a + sizeOf l₁ := by simp [sizeof_pos]
        mem.decidable ⟨b, a⟩ l₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf (a.cons' l₁) + sizeOf l₂

Tactic:
decreasing_tactic
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)
haveI : (this : Decidable (l₁ ⊆ l₂)) → Decidable (a.cons' l₁ ⊆ l₂)
⊢ Decidable (a.cons' l₁ ⊆ l₂)

Tactic:
haveI :=
        have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf (Lists'.cons' a l₁) + SizeOf.sizeOf l₂ := by
          decreasing_tactic
        Subset.decidable l₁ l₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this_1 : Decidable (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a ∈ l₂)
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable (a.cons' l₁ ⊆ l₂)

Tactic:
exact decidable_of_iff' _ (@Lists'.cons_subset _ ⟨_, _⟩ _ _)

Premises used: Lists'.cons_subset, decidable_of_iff'
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
⊢ sizeOf (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b) < HAdd.hAdd (α := ℕ) 1 1 + sizeOf b + sizeOf l₂

Tactic:
simp [sizeof_pos]

Premises used: Lists.sizeof_pos
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
haveI : (this : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)) → Decidable (a ∈ b.cons' l₂)
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
haveI :=
        have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
        Equiv.decidable a ⟨_, b⟩
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
⊢ sizeOf a + sizeOf l₂ < sizeOf a + sizeOf (b.cons' l₂)

Tactic:
decreasing_tactic
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
haveI : (this : Decidable (a ∈ l₂)) → Decidable (a ∈ b.cons' l₂)
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
haveI :=
        have :
          SizeOf.sizeOf a + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
          decreasing_tactic
        mem.decidable a l₂
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this_1 : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
this : Decidable (a ∈ l₂)
refine : a ∈ b.cons' l₂ ↔ a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b ∨ a ∈ l₂
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
refine decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) ?_

Premises used: Membership.mem, decidable_of_iff', Or, Sigma.mk, Lists.Equiv
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this_1 : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
this : Decidable (a ∈ l₂)
rw : a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b) l₂
⊢ a ∈ b.cons' l₂ ↔ a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b ∨ a ∈ l₂

Tactic:
rw [← Lists'.mem_cons]

Premises used: Lists'.mem_cons
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
inst : DecidableEq α
a : Lists α
b_1 : Bool
b : Lists' α b_1
l₂ : Lists' α true
this_1 : Decidable (a ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 b) l₂

Tactic:
rfl
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l : Lists' α true
⊢ ∀ {a a' : Lists α}, a ~ a' → (a ∈ l ↔ a' ∈ l)

Tactic:
suffices ∀ {a a'}, a ~ a' → a ∈ l → a' ∈ l from fun e => ⟨this e, this e.symm⟩
  fun e₁ ⟨_, m₃, e₂⟩ => ⟨_, m₃, e₁.symm.trans e₂⟩

Premises used: Membership.mem, Lists.Equiv.trans, Lists.Equiv.symm, And.intro, Iff.intro, Exists.intro, _private.0.Lists'.mem_equiv_left.match_1
-- Module: Mathlib.SetTheory.Lists
Goal:
α : Type u_1
l₁ l₂ l₃ : Lists' α true
h₁ : l₁ ⊆ l₂
h₂ : l₂ ⊆ l₃
⊢ l₁ ⊆ l₃

Tactic:
subset_def.2 fun _ m₁ => mem_of_subset h₂ <| mem_of_subset' h₁ m₁

Premises used: Iff.mpr, Lists'.subset_def, Lists'.mem_of_subset, Lists'.mem_of_subset'