mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (k % z).toNat < z.natAbs

pp: case mp.refine_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + ↑↑⟨(k % z).toNat, ?mp.refine_1⟩) • p = k • p

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (k % z).toNat < z.natAbs
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
h : (some a :: ↑s) 0 = none
⊢ (some a :: ↑s) (0 + 1) = none

pp: case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none

Tactic:
·

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
h : (some a :: ↑s) 0 = none
⊢ (some a :: ↑s) (0 + 1) = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none

Tactic:
·

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' → x = x' ∧ s = s'

pp: case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'

Tactic:
·

Goal state after:
case mp
α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' → x = x' ∧ s = s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'

Tactic:
·

Goal state after:
case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = none
⊢ s = nil

pp: case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : (fun a' ↦ (a', s.tail)) <$> some val✝ = none
⊢ s = nil

Tactic:
·

Goal state after:
case none
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = none
⊢ s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : (fun a' ↦ (a', s.tail)) <$> some val✝ = none
⊢ s = nil

Tactic:
·

Goal state after:
case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : (fun a' ↦ (a', s.tail)) <$> some val✝ = none
⊢ s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = some (a, s')
⊢ s = cons a s'

pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
·

Goal state after:
case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = some (a, s')
⊢ s = cons a s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
·

Goal state after:
case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
s : Seq α
⊢ s.head = none → s = nil

pp: case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none

Tactic:
·

Goal state after:
case mp
α : Type u
s : Seq α
⊢ s.head = none → s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none

Tactic:
·

Goal state after:
case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = none
⊢ motive s

pp: case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = some v
⊢ motive s

Tactic:
·

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = none
⊢ motive s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = some v
⊢ motive s

Tactic:
·

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = some v
⊢ motive s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
⊢ corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (Corec.f f (some b)).snd n = none

Tactic:
generalize some b = o

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
o : Option β
⊢ corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : (Corec.f f none).fst = none
⊢ (Corec.f f (Corec.f f none).snd).fst = none

pp: case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h : (Corec.f f (some b)).fst = none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
·

Goal state after:
case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : (Corec.f f none).fst = none
⊢ (Corec.f f (Corec.f f none).snd).fst = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
h :
  (match none with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match none with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

Tactic:
·

Goal state after:
case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
h :
  (match none with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match none with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

Tactic:
·

Goal state after:
case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

pp: case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
s : α × β
h : f b = some s
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some s with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
·

Goal state after:
case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y ↦ ∃ s s', ↑s = x ∧ ↑s' = y ∧ R s s'

pp: case a
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'

Tactic:
·

Goal state after:
case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y ↦ ∃ s s', ↑s = x ∧ ↑s' = y ∧ R s s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil.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'
⊢ R nil nil → BisimO R nil.destruct nil.destruct → nil.head = nil.head ∧ R nil.tail nil.tail

pp: 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

pp: 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 (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

pp: 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:
·

Goal state after:
case nil.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'
⊢ R nil nil → BisimO R nil.destruct nil.destruct → nil.head = nil.head ∧ R nil.tail nil.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

pp: case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Tactic:
·

Goal state after:
case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil.nil.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'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head

pp: case nil.nil.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'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail

Tactic:
·

Goal state after:
case nil.nil.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'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil.nil.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'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail

Tactic:
·

Goal state after:
case nil.nil.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'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Tactic:
·

Goal state after:
case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: 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

pp: 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 (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

pp: 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:
·

Goal state after:
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
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: 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 (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

pp: 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:
·

Goal state after:
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 (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: 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:
·

Goal state after:
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
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case a
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'

Tactic:
·

Goal state after:
case a
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inl
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
h_nil₁ : s₁ = nil
h_nil₂ : s₂ = nil
⊢ BisimO motive s₁.destruct s₂.destruct

pp: case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
w✝² : α
w✝¹ w✝ : Seq α
h₁ : s₁ = cons w✝² w✝¹
h₂ : s₂ = cons w✝² w✝
right✝ : motive w✝¹ w✝
⊢ BisimO motive s₁.destruct s₂.destruct

Tactic:
·

Goal state after:
case inl
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
h_nil₁ : s₁ = nil
h_nil₂ : s₂ = nil
⊢ BisimO motive s₁.destruct s₂.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h : Stream'.cons none c.val 0 = some a
⊢ Stream'.cons none c.val (0 + 1) = some a

pp: case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a

Tactic:
·

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h : Stream'.cons none c.val 0 = some a
⊢ Stream'.cons none c.val (0 + 1) = some a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a

Tactic:
·

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
w✝² : α
w✝¹ w✝ : Seq α
h₁ : s₁ = cons w✝² w✝¹
h₂ : s₂ = cons w✝² w✝
right✝ : motive w✝¹ w✝
⊢ BisimO motive s₁.destruct s₂.destruct

Tactic:
·

Goal state after:
case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
w✝² : α
w✝¹ w✝ : Seq α
h₁ : s₁ = cons w✝² w✝¹
h₂ : s₂ = cons w✝² w✝
right✝ : motive w✝¹ w✝
⊢ BisimO motive s₁.destruct s₂.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
·

Goal state after:
case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)

Tactic:
rw [get_succ_iterate', ih, get_succ_iterate']

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
·

Goal state after:
case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
·

Goal state after:
case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
⊢ (unfolds head tail s).tail.get n = s.tail.get n

Tactic:
unfolds_eq,

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n
s : Stream' α
⊢ (s.head :: unfolds head tail s.tail).tail.get n = s.tail.get n