mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs

Tactic:
rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ ll.size + lr.size + 1 + rl.size + rr.size + 1 = ll.size + lr.size + 1 + (rl.size + rr.size + 1)
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

Tactic:
exact ⟨⟨i, c⟩, right _ ha, left _ _ h⟩

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
⊢ let d := a.gcdD b;
  let w := a.gcdW b;
  let x := a.gcdX b;
  let y := a.gcdY b;
  let z := a.gcdZ b;
  let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
intro d

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
⊢ let w := a.gcdW b;
  let x := a.gcdX b;
  let y := a.gcdY b;
  let z := a.gcdZ b;
  let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ ↑w * ↑z = x * y + 1

Tactic:
rw [← mul_coe, hdet, succPNat_coe]

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

Goal state before:
pp: case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Tactic:
replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
      simp [balanceL, balance, H2]; split_ifs <;> simp [add_comm]

Goal state after:
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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))

Tactic:
q.P.wDest'_wMk,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ((TypeVec.id ::: recF g) <$$> ⟨a, splitFun f' f⟩))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
cases cmpLE x y <;> simp [insert'_eq_insertWith]

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

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
rw [h.sz.1]

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      (t_l.size + t_r.size + 1)
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF ((P F).wMk' ∘ repr) ((P F).wMk a f' f) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
recF_eq',

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> (P F).wDest' ((P F).wMk a f' f))) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
rw [h.sz.1]

Goal state after:
case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      (t_l.size + t_r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.gt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
rw [h.sz.1]

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.gt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      (t_l.size + t_r.size + 1)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p

Tactic:
by rintro α β f ⟨x, g⟩; simp only [Pi.abs, (· <$$> ·), ← abs_map]; rfl

Goal state after:
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
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : (P F).M α
⊢ ∀ (a : (P F).M α),
    r (Quot.mk Mcongr c) (Quot.mk Mcongr a) →
      Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a)

Tactic:
intro d

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c d : (P F).M α
⊢ r (Quot.mk Mcongr c) (Quot.mk Mcongr d) →
    Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr d)
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 (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ recF g ((P F).wMk' ⟨a, (TypeVec.id ::: fixToW) ⊚ f⟩) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
recF_eq',

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk' ⟨a, (TypeVec.id ::: fixToW) ⊚ f⟩))) =
    g ((TypeVec.id ::: rec g) <$$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
g : F α → α
x : (P F).W
⊢ recF g x = g (abs ((P F).map (recF g) x.dest))

Tactic:
by
  cases x
  rfl

Goal state after:
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩

Tactic:
congr 2

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f
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₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ abs ⟨a, (TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩

Tactic:
congr 2

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ((TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧) =
    (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ ∃ a_1 f_1, abs ⟨a, fun x ↦ ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)

Tactic:
refine ⟨_, _, rfl, ?_⟩

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ ∀ (i : (P F).B a), p ⟦f i⟧
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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ∃ a_1 f_1,
    abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧
      ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)

Tactic:
refine ⟨_, _, rfl, ?_⟩

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.PredLast p ((P F).appendContents f' (fun x ↦ ⟦f x⟧) i j)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) (some (fst✝, snd✝)) (some (fst✝, snd✝))

Tactic:
simp only [LiftRelO, and_true]

Goal state after:
case some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
fst✝ : α
snd✝ : WSeq α
⊢ R fst✝ fst✝
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t u✝ : WSeq α
h1 : LiftRel R s✝ t
h2 : LiftRel R t u✝
s u : WSeq α
h : (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s u
⊢ Computation.LiftRel (LiftRelO R fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct

Tactic:
rcases h with ⟨t, h1, h2⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
s u t : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ Computation.LiftRel (LiftRelO R fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
b : β
t' : WSeq β
td : some (b, t') ∈ (t.drop n).destruct
ab : R a b
right✝ : LiftRel R s' t'
⊢ ∃ b ∈ t, R a b

Tactic:
exact ⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ⟨⋯.choose, ⋯⟩ = t

Tactic:
rw [← Subtype.coe_inj]

Goal state after:
case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ↑⟨⋯.choose, ⋯⟩ = ↑t
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (Sum.inr (c' :: val✝))

Tactic:
· intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩

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
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }

Tactic:
congr 2

Goal state after:
case case1.e_s₁.e_i
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
⊢ s₁.i + c + Pos.Raw.get s₁.s s₁.i = s₁.i + Pos.Raw.get s₁.s s₁.i + c

case case1.e_s₂.e_i
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
⊢ s₂.i + c + Pos.Raw.get s₂.s s₂.i = s₂.i + Pos.Raw.get s₂.s s₂.i + c
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
⊢ decide
      ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
        { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr) =
    decide (s₁.curr < s₂.curr)

pp: case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
· simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList]

Goal state after:
case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
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:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ pure (node (f v)) <*> pure (map f l) <*> pure (map f r) = pure (node (f v) (map f l) (map f r))

Tactic:
pure_seq,

Goal state after:
case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node (f v) <$> pure (map f l) <*> pure (map f r) = pure (node (f v) (map f l) (map f r))