-- Mathlib/SetTheory/Lists.lean
theorem Equiv.trans : ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Proof state:
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l'

Tactic:
apply inductionMut

Result:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : α), trans (atom a)

case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (l : Lists' α true), (∀ l' ∈ l.toList, trans l') → trans (of' l)

case D0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ l' ∈ Lists'.nil.toList, trans l'

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' ∈ l.toList, trans l') → ∀ l' ∈ (Lists'.cons a l).toList, trans l'

Proof state:
α : Type u_1
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
let trans := fun l₁ : Lists α => ∀ ⦃l₂ l₃⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Result:
α : 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₃

Proof state:
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' ∈ l.toList, trans l'
⊢ ∀ l' ∈ (Lists'.cons a l).toList, trans l'

Tactic:
simpa using ⟨IH₁, IH₂⟩

Result:
no goals

Proof state:
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' ∈ l₁.toList, trans l'
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
exact h₁

Result:
no goals

Proof state:
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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₃ : Lists α
m₃ : a₃ ∈ l₂✝.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.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⟩

Result:
no goals

Proof state:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : α), trans (atom a)

Tactic:
intro a l₂ l₃ h₁ h₂

Result:
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₃

Proof state:
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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₃ : Lists α
m₃ : a₃ ∈ l₂✝.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.toList
e₃₂ : a₃ ~ a₂
⊢ a₃ ∈ l₁

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

Result:
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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₃ : Lists α
m₃ : a₃ ∈ l₂✝.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.toList
e₃₂ : a₃ ~ a₂
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁

Proof state:
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' ∈ l₁.toList, trans l'
l₃ : Lists α
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ l₃
⊢ of' l₁ ~ l₃

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

Result:
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' ∈ l₁.toList, trans l'
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Proof state:
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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ a ∈ l₁.toList, a ∈ l₂✝

Tactic:
intro a₁ m₁

Result:
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' ∈ l₁.toList, trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
⊢ a₁ ∈ l₂✝

Proof state:
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
exact this.1

Result:
no goals

Proof state:
case D0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ l' ∈ Lists'.nil.toList, trans l'

Tactic:
rintro _ ⟨⟩

Result:
no goals