-- Mathlib/Data/Seq/Seq.lean
theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂

Proof state:
case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝¹ s✝¹) (cons x✝ s✝) →
    BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct →
      (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail

Tactic:
intro _ this

Result:
case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
this : BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct
⊢ (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail

Proof state:
case cons.cons.intro.left
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ some x✝¹ = some x✝

Tactic:
rw [h1]

Result:
no goals

Proof state:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
this : BisimO R s.destruct s'.destruct
⊢ s.head = s'.head ∧ R s.tail s'.tail

Tactic:
revert r this

Result:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
⊢ R s s' → BisimO R s.destruct s'.destruct → s.head = s'.head ∧ R s.tail s'.tail

Proof state:
case cons.cons.intro.right
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ R s✝¹ s✝

Tactic:
exact h2

Result:
no goals

Proof state:
case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R nil (cons x✝ s✝)
this : BisimO R nil.destruct (cons x✝ s✝).destruct
⊢ nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Tactic:
rw [destruct_nil, destruct_cons] at this

Result:
case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R nil (cons x✝ s✝)
this : BisimO R none (some (x✝, s✝))
⊢ nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Proof state:
case cons.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝ s✝) nil
this : BisimO R (some (x✝, s✝)) none
⊢ (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

Tactic:
exact False.elim this

Result:
no goals

Proof state:
case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
⊢ R nil (cons x✝ s✝) →
    BisimO R nil.destruct (cons x✝ s✝).destruct → nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Tactic:
intro _ this

Result:
case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R nil (cons x✝ s✝)
this : BisimO R nil.destruct (cons x✝ s✝).destruct
⊢ nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Proof state:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ (↑s).head = (↑s').head ∧ ∃ s_1 s'_1, ↑s_1 = (↑s).tail ∧ ↑s'_1 = (↑s').tail ∧ R s_1 s'_1

Tactic:
suffices head s = head s' ∧ R (tail s) (tail s') from
  And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
    by cases s' using Subtype.recOn; rfl, r⟩) this

Result:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ s.head = s'.head ∧ R s.tail s'.tail

Proof state:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
⊢ s.head = s'.head ∧ R s.tail s'.tail

Tactic:
have := bisim r

Result:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r : R s s'
this : BisimO R s.destruct s'.destruct
⊢ s.head = s'.head ∧ R s.tail s'.tail

Proof state:
case cons.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝ s✝) nil
this : BisimO R (cons x✝ s✝).destruct nil.destruct
⊢ (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

Tactic:
rw [destruct_nil, destruct_cons] at this

Result:
case cons.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝ s✝) nil
this : BisimO R (some (x✝, s✝)) none
⊢ (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

Proof state:
case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
this : BisimO R (some (x✝¹, s✝¹)) (some (x✝, s✝))
⊢ some x✝¹ = some x✝ ∧ R s✝¹ s✝

Tactic:
obtain ⟨h1, h2⟩ := this

Result:
case cons.cons.intro
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ some x✝¹ = some x✝ ∧ R s✝¹ s✝

Proof state:
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ ↑s'.tail = (↑s').tail

Tactic:
cases s' using Subtype.recOn

Result:
case mk
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Seq α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ ↑(tail ⟨val✝, property✝⟩) = (↑⟨val✝, property✝⟩).tail

Proof state:
case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
r✝ : R nil (cons x✝ s✝)
this : BisimO R none (some (x✝, s✝))
⊢ nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Tactic:
exact False.elim this

Result:
no goals