mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ match
    omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (nil, s).1.destruct with
      | none =>
        match (nil, s).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).2)),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
]

Goal state after:
α : Type u
s✝ s : Seq α
⊢ match
    omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (nil, s).1.destruct with
      | none =>
        match (nil, s).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).2)),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + (m' + 1))

Tactic:
]

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + (m' + 1))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match some (x✝, s✝) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    some (x✝, s✝) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
]

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match some (x✝, s✝) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    some (x✝, s✝) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (some (x✝, s✝.append nil)) (some (x✝, s✝))

Tactic:
]

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (some (x✝, s✝.append nil)) (some (x✝, s✝))
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.b -
      pB *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.a =
    (ppA * pB - ppB * pA) * -gp.a

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.b -
      pB *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.a =
    (ppA * pB - ppB * pA) * -gp.a
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
⊢ g.nums n * g.dens n - g.dens n * g.nums n = (∏ x ∈ Finset.range n, -(g.partNums.get? x).getD 0) * -none.getD 0

Tactic:
]

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
⊢ g.nums n * g.dens n - g.dens n * g.nums n = (∏ x ∈ Finset.range n, -(g.partNums.get? x).getD 0) * -none.getD 0
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
⊢ -((↑s).partNums.get? i).getD 0 = -1

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
⊢ -((↑s).partNums.get? i).getD 0 = -1
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s).s.get? i = some gp
⊢ -1 = -1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
⊢ (-1) ^ (n + 1) = (-1) ^ (n + 1)

Tactic:
]

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

Goal state before:
pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m_1 n, s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1

Tactic:
]

Goal state after:
case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m_1 n, s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Tactic:
]

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct

Tactic:
]

Goal state after:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> pure s).destruct (pure s).destruct

Tactic:
]

Goal state after:
case pure
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> pure s).destruct (pure s).destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct s.think.destruct

Tactic:
]

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct s.think.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ (empty α <|> s) = (empty α <|> s)

Tactic:
]

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

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct

Tactic:
]

Goal state after:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (pure s <|> (empty α).think).destruct (pure s).destruct

Tactic:
]

Goal state after:
case pure
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (pure s <|> (empty α).think).destruct (pure s).destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct s.think.destruct

Tactic:
]

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct s.think.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂

Tactic:
]

Goal state after:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> empty α) = (s <|> empty α)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C z * X ^ (n + 1) = C z * X ^ (n + 1)

Tactic:
]

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

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
]

Goal state after:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Tactic:
]

Goal state after:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 ↦ x1 = x2) a b
⊢ b ∈ c₂

Tactic:
]

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 ↦ x1 = x2) a b
⊢ b ∈ c₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
l l' : List α
⊢ ↑(l ++ l') = (↑l).append ↑l'

Tactic:
induction l <;> simp [*]

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

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ b ∈ c₁

Tactic:
]

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ b ∈ c₁
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
⊢ {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} ⊆
    ↑(Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
⊢ {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} ⊆
    ↑(Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b