-- Mathlib/Data/Stream/Init.lean
theorem bisim_simple (s₁ s₂ : Stream' α) :
    head s₁ = head s₂ → s₁ = tail s₁ → s₂ = tail s₂ → s₁ = s₂ := fun hh ht₁ ht₂ =>
  eq_of_bisim (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂)
    (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by
      constructor
      · exact h₁
      rw [← h₂, ← h₃]
      (repeat' constructor) <;> assumption)
    (And.intro hh (And.intro ht₁ ht₂))

Proof state:
case right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁.tail s₂.tail

Tactic:
rw [← h₂, ← h₃]

Result:
case right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂

Proof state:
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head ∧ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁.tail s₂.tail

Tactic:
constructor

Result:
case left
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head

case right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁.tail s₂.tail

Proof state:
case right.right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁ = s₁.tail ∧ s₂ = s₂.tail

Tactic:
constructor

Result:
case right.right.left
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁ = s₁.tail

case right.right.right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₂ = s₂.tail

Proof state:
case right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂

Tactic:
(repeat' constructor) <;> assumption

Result:
no goals

Proof state:
case right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂

Tactic:
repeat' constructor

Result:
case right.left
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head

case right.right.left
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁ = s₁.tail

case right.right.right
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₂ = s₂.tail

Proof state:
case left
α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head

Tactic:
exact h₁

Result:
no goals