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

Goal state before:
pp: case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [l0, m1.1, m1.2]

Goal state after:
case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (0 + 0 + 1) (0 + r.size + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
conv =>

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑(- -n).bitm1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ p.pred'.toZNum.succ = ZNum.pos p

Tactic:
← toZNum_succ,

Goal state after:
p : PosNum
⊢ p.pred'.succ.toZNum = ZNum.pos p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ (ofNat' 0).toZNum = (ofNat' (0 + 1)).toZNumNeg + 1

Tactic:
rw [ofNat'_succ, ofNat'_zero]

Goal state after:
⊢ toZNum 0 = (0 + 1).toZNumNeg + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : ZNum
⊢ ↑(b + 0) = ↑b + ↑0

Tactic:
cases b

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(zero + 0) = ↑zero + ↑0

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(pos a✝ + 0) = ↑(pos a✝) + ↑0

case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(neg a✝ + 0) = ↑(neg a✝) + ↑0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: b : ZNum
⊢ ↑(b * 0) = ↑b * ↑0

Tactic:
cases b

Goal state after:
case zero
⊢ ↑(zero * 0) = ↑zero * ↑0

case pos
a✝ : PosNum
⊢ ↑(pos a✝ * 0) = ↑(pos a✝) * ↑0

case neg
a✝ : PosNum
⊢ ↑(neg a✝ * 0) = ↑(neg a✝) * ↑0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ node s l x r = l.node' x r

Tactic:
by
  rw [h.1]

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual

Tactic:
cases m <;> simp [node4L, node4R, node3R, dual_node3L, add_comm]

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

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
⊢ (l.rotateL x nil).dual = nil.dual.rotateR x l.dual

Tactic:
simp [rotateL, rotateR]

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).dual = (node size✝ l✝ x✝ r✝).dual.rotateR x l.dual

Tactic:
simp [rotateL, rotateR]

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).dual =
    if l✝.size < ratio * r✝.size then r✝.dual.node3R x✝ l✝.dual x l.dual else r✝.dual.node4R x✝ l✝.dual x l.dual
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: d n : PosNum
⊢ ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2

Tactic:
by
  rw [Nat.div_mod_unique (PosNum.cast_pos _)]
  induction n with
  | one =>
    exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
  | bit1 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
    · lia
  | bit0 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux
    · simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
    · simpa using IH.2

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

Goal state before:
pp: case pos
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⟩)
h'' : a = x_a
⊢ ((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

Tactic:
subst x_a
      simp only [dif_pos, casesOn_mk']
      rw [ps_ih]
      intro h'
      apply h
      constructor <;> try rfl
      apply h'

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
← size_dual,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ (l.rotateR x r).dual.size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
by
  rw [balance']; split_ifs with h h_1 h_2
  · exact hl.node' hr (Or.inl h)
  · exact hl.rotateL hr h h_1 H₁
  · exact hl.rotateR hr h h_2 H₂
  · exact hl.node' hr (Or.inr ⟨not_lt.1 h_2, not_lt.1 h_1⟩)

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

Goal state before:
pp: case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₁, f₁⟩)
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
obtain rfl : a₀ = a₁ := bisim.head h₁

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₀, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₀, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₂ (l.balanceR x r).dual o₁

Tactic:
dual_balanceR

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| dest P ⟨a, g ⊚ f⟩ = (g ::: fun x ↦ g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
conv =>

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
    splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
      ((fun x ↦ g <$$> x) ∘ fun x ↦ ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ = (g ::: fun x ↦ g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
conv =>
    rhs
    rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ =
    ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
      splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
        ((fun x ↦ g <$$> x) ∘ fun x ↦ ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (l.balanceR x r).dual o₁

Tactic:
dual_balanceR

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case succ
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ (n • u).prod * u.prod = u.prod ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ u.prod ^ n * u.prod = u.prod ^ (n + 1)
Module: Mathlib.Data.QPF.Multivariate.Basic

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

pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), p ↑(f i j)

Tactic:
· rw [← hy, ← abs_repr y, h, ← abs_map]; rfl

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

Goal state before:
pp: case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
rw [← yeq, ← abs_repr u, h, ← abs_map]

Goal state after:
case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ h'' a' '' univ

Tactic:
have hh : u ∈ supp x a' := by rw [← hfi]; apply h'

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ
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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x) = (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) y)

Tactic:
have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) x) = (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) y)
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 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)

Tactic:
conv =>

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)
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
β : Type u
g : β → F (α ::: β)
x : β
| (corec g x).dest = (TypeVec.id ::: corec g) <$$> g x

Tactic:
conv =>

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
| Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr (corecF g 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
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
⊢ (TypeVec.id ::: Quot.mk r) <$$> (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r) <$$> (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)

Tactic:
exact h _ _ r'ab

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

Goal state before:
pp: case right
α : 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
h_balanceable :
  (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ 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)

Tactic:
rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]

Goal state after:
case right
α : 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
h_balanceable :
  (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised ((erase x t_l).size + t_r.size + 1) (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
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
conv =>

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
| recF g ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr x))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.right.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
rw [← yeq, ← abs_repr u, h, ← abs_map]

Goal state after:
case h.right.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((P F).map (fun t ↦ (↑t).2) ⟨a, f⟩) = abs ⟨a, fun i ↦ (↑(f i)).2⟩
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 ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
conv =>

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 α
| abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
| rec g (mk x) = g (rec g <$> x)

Tactic:
conv =>

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
| recF g (PFunctor.W.mk ((P F).map fixToW (repr x)))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : F (Fix F)
| (mk ∘ dest) <$> x = x

Tactic:
conv =>

Goal state after:
F : Type u → Type u
q : QPF F
x : F (Fix F)
| id <$> x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
⊢ Quot.mk Mcongr <$> abs x.dest = Quot.mk Mcongr <$> abs y.dest

Tactic:
have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩

Goal state after:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ Quot.mk Mcongr <$> abs x.dest = Quot.mk Mcongr <$> abs y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

Goal state after:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
conv =>

Goal state after:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| (corec g x).dest = corec g <$> g x

Tactic:
conv =>

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| Quot.lift (fun x ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g 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 : F (α ::: Fix F α)
| ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x

Tactic:
conv =>

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
| TypeVec.id <$$> 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
g : α ⟹ β
x : ↑(P F).wp α
| Quot.mk WEquiv (g <$$> x) = g <$$> Quot.mk WEquiv x

Tactic:
conv =>

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
x : ↑(P F).wp α
| Fix.map g (Quot.mk WEquiv 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✝ x y : Cofix F α
h : x = mk y.dest
| (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
conv =>

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
| (TypeVec.id ::: corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$> (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest