mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p

Tactic:
intro α

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α : TypeVec.{u} n
⊢ ∀ {β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
x : ↑(P F).wp α
⊢ Quot.mk WEquiv (g <$$> x) = g <$$> Quot.mk WEquiv x

Tactic:
conv =>
      rhs
      dsimp [MvFunctor.map]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
x : ↑(P F).wp α
⊢ Quot.mk WEquiv (g <$$> x) = Fix.map g (Quot.mk WEquiv x)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_neg hn]
    exact mul_nonneg_of_nonpos_of_nonpos (by simp) hn.le

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x : F₂ (F₁ α)
⊢ abs ⟨(repr x).fst, fun x_1 ↦ abs ⟨(repr ((repr x).snd x_1)).fst, fun y ↦ (repr ((repr x).snd x_1)).snd y⟩⟩ =
    abs (repr x)

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
⊢ abs ⟨⟨a, f⟩.fst, fun x ↦ abs ⟨(repr (⟨a, f⟩.snd x)).fst, fun y ↦ (repr (⟨a, f⟩.snd x)).snd y⟩⟩ = abs ⟨a, f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : ↑(P F) α
⊢ FG_abs (abs ((P F).map f x)) = f <$> FG_abs (abs x)

Tactic:
by rw [abs_map, FG_abs_map]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) ↔ ∀ u ∈ supp (abs ⟨a, f⟩), p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (g <$> abs ⟨a, f⟩) = g '' supp (abs ⟨a, f⟩)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
⊢ c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
T

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
S : WSeq (Computation α)
m : pure a ∈ []
⊢ ∃ a, parallel.aux2 [] = Sum.inl a

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
⊢ (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
    ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
IH

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
m : s.think ∈ []
l' : List (Computation α)
e' : parallel.aux2 [] = Sum.inr l'
⊢ s ∈ l'

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap R) s2 s1

Tactic:
by
  refine ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩
  rw [← LiftRelO.swap, Computation.LiftRel.swap]
  apply liftRel_destruct h

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
⊢ (∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')) →
    ∀ {s : WSeq α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
IH

Goal state after:
case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
⊢ ∀ {s : WSeq α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case zero
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
⊢ c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
T

Goal state after:
case zero
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case succ
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T : c✝.Terminates
n✝ : ℕ
a✝ :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n✝ → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? (n✝ + 1)
⊢ c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
T

Goal state after:
case succ
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n✝ : ℕ
a✝ :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n✝ → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? (n✝ + 1)
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ s'.think.get? n

Tactic:
simp only [get?, dropn_think, head_think]

Goal state after:
case h2
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (s'.drop n).head.think
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (Sum.inr [])

pp: case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝)
    (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) tail✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) head✝.destruct)

Tactic:
case nil =>
      intro a h
      assumption

Goal state after:
case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝)
    (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) tail✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) head✝.destruct)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case nil
α : Type u
⊢ [] ∈ (↑[]).toList

Tactic:
| nil =>

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

Goal state before:
pp: case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
⊢ (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
    ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = C'.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
IH

Goal state after:
case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C'.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
⊢ ∀ {T : WSeq (WSeq β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
T

Goal state after:
case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
⊢ LiftRel (LiftRel R) S T →
    ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨j, b⟩ ≤ ⟨i, a⟩

Tactic:
· simp [hij, le_def, hij.symm]

Goal state after:
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
⊢ (∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
IH

Goal state after:
case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true

Tactic:
Legacy.Iterator.hasNext_cons_addChar,

Goal state after:
case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true