mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise (fun a b ↦ a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))

case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}

Tactic:
· simpa [Nat.succ_le_succ_iff] using hm

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun ab s ↦
        let r := f ab.1 ab.2 s.1;
        (r.1, r.2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))

Tactic:
by
    simp only [mapAccumr₂, mapAccumr₂_eq_foldr f as]
    rfl

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
by
  rcases shortlex_def.mp h with h1 | h2
  · apply of_length_lt
    rw [List.length_append, List.length_append]
    lia
  cases s with
  | nil =>
    rw [List.nil_append, List.nil_append]
    exact h
  | cons head tail =>
    apply of_lex
    · simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1
    exact List.Lex.append_left r h2.2 (head :: tail)

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h2len : (x :: xs).length = (xa :: xb).length
h : r x xa
⊢ Acc (Shortlex r) (x :: xs)

Tactic:
simp only [List.length_cons, add_left_inj] at h2len

Goal state after:
case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ Acc (Shortlex r) (x :: xs)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
· conv at ep => change p = 1
      subst p
      simp

Goal state after:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
i✝ : F.B a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)

Tactic:
apply n_ih

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
i : F.B a✝
⊢ Agree' n✝ (f✝¹ i) (f✝ i)

Tactic:
apply n_ih

Goal state after:
case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
i : F.B a✝
⊢ Agree ((f✝¹ i).approx n✝) ((f✝ i).approx (n✝ + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Tactic:
apply n_ih

Goal state after:
case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree' n✝ (x' i) (y' i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case cons.f
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head

Tactic:
simp only [iselect, isubtree] at ps_ih ⊢

Goal state after:
case cons.f
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x✝ : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateL x r).Sized

Tactic:
cases r; · exact hl.node' hr
  rw [Ordnode.rotateL_node]; split_ifs
  · exact hl.node3L hr.2.1 hr.2.2
  · exact hl.node4L hr.2.1 hr.2.2

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.balance' x r).Sized

Tactic:
unfold Ordnode.balance'; split_ifs
  · exact hl.node' hr
  · exact hl.rotateL hr
  · exact hl.rotateR hr
  · exact hl.node' hr

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ (node size✝ l x✝ r).toList.length = (node size✝ l x✝ r).realSize

Tactic:
by
    rw [toList_node, List.length_append, List.length_cons, length_toList' l,
        length_toList' r]; rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) =
    if 0 + (0 + 1 + 1) ≤ 1 then nil.node' x (nil.node' rx (node 1 nil rrx nil))
    else nil.rotateL x (nil.node' rx (node 1 nil rrx nil))

Tactic:
rw [if_neg, rotateL_node, if_pos]

Goal state after:
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = nil.node3L x nil rx (node 1 nil rrx nil)

case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ nil.size < ratio * (node 1 nil rrx nil).size

case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ ¬0 + (0 + 1 + 1) ≤ 1
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b x, p ⟨a, b⟩) ↔ ∃ h, p ⟨n', h⟩

Tactic:
mk_coe,

Goal state after:
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a h x, p ⟨a, ⋯⟩) ↔ ∃ h, p ⟨n', h⟩
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a h x, p ⟨a, ⋯⟩) ↔ ∃ h, p ⟨n', h⟩

Tactic:
@exists_comm (_ < _) (_ = _),

Goal state after:
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b a_1, p ⟨a, ⋯⟩) ↔ ∃ h, p ⟨n', h⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : (P F).B a ⟹ α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ (fun i ↦ Subtype.val) <$$> abs ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩ = x

Tactic:
rw [← abs_map, h₀]

Goal state after:
case h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : (P F).B a ⟹ α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩) = abs ⟨a, f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x

Tactic:
rw [← abs_map, h₀]

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case mk
α : Type u_1
inst✝ : Preorder α
s_val : Ordnode α
property✝ : s_val.Valid
h : (↑⟨s_val, property✝⟩).empty = true
⊢ ⟨s_val, property✝⟩ = ∅

Tactic:
| mk s_val _ =>

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x

Tactic:
apply Fix.ind_rec

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)
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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x

Tactic:
apply Fix.ind_rec

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)
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
x : Fix F α
⊢ (mk ∘ dest) x = x

Tactic:
apply Fix.ind_rec

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → (mk ∘ dest) (mk x) = mk x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ x = y

Tactic:
by rw [← Cofix.dest_mk x, h, Cofix.dest_mk]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ prod.fst ⊚ prod.diag) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
fst_diag

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
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
⊢ ↑((P F₂).comp (P F₁)) α → Functor.Comp F₂ F₁ α

Tactic:
by
    dsimp [Functor.Comp]
    intro p
    exact abs ⟨p.1.1, fun x => abs ⟨p.1.2 x, fun y => p.2 ⟨x, y⟩⟩⟩

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
⊢ o ∈ t.head

Tactic:
rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ o ∈ t.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons a' s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
i2

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t

Tactic:
intro s t h

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝² : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : S s✝ t✝
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h✝ : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ S s t
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab

Goal state after:
case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (↑s).get? n = Computation.pure (s.get? n)

Tactic:
dsimp [get?]; rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]

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

Goal state before:
pp: case case4
c : Char
s₁ s₂ : Legacy.Iterator
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) =
    false

Tactic:
if_neg (by simpa using h₁)

Goal state after:
case case4
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ false = false
Module: Mathlib.Data.String.Basic

Goal state before:
pp: a b c : String
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
simp only [le_iff_toList_le]
    apply le_trans

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

Goal state before:
pp: α : 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 β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝² : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
x✝¹ : LiftRelO R (LiftRel R) none none
x✝ : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
this : n1 < n
ob : Option (β × WSeq β)
mb : ob ∈ T'.join.destruct
rob : LiftRelO R U a ob
⊢ ob ∈ destruct_append.aux T'.join none

Tactic:
exact mb

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

Goal state before:
pp: case right.ma
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ b ∈ T.join.destruct

Tactic:
exact mb

Goal state after: