mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ - -n = n

Tactic:
cases n

Goal state after:
case zero
⊢ - -zero = zero

case pos
a✝ : PosNum
⊢ - -pos a✝ = pos a✝

case neg
a✝ : PosNum
⊢ - -neg a✝ = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.bit1 = (-n).bitm1

Tactic:
cases n

Goal state after:
case zero
⊢ -zero.bit1 = (-zero).bitm1

case pos
a✝ : PosNum
⊢ -(pos a✝).bit1 = (-pos a✝).bitm1

case neg
a✝ : PosNum
⊢ -(neg a✝).bit1 = (-neg a✝).bitm1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.bitm1 = (-n).bit1

Tactic:
cases n

Goal state after:
case zero
⊢ -zero.bitm1 = (-zero).bit1

case pos
a✝ : PosNum
⊢ -(pos a✝).bitm1 = (-pos a✝).bit1

case neg
a✝ : PosNum
⊢ -(neg a✝).bitm1 = (-neg a✝).bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.succ = (-n).pred

Tactic:
cases n

Goal state after:
case zero
⊢ -zero.succ = (-zero).pred

case pos
a✝ : PosNum
⊢ -(pos a✝).succ = (-pos a✝).pred

case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ (↑↑p).natAbs = (-↑p).natAbs

Tactic:
rw [p.to_nat_to_int, Int.natAbs_neg]

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

Goal state before:
pp: n : ZNum
⊢ n + 0 = n

Tactic:
cases n

Goal state after:
case zero
⊢ zero + 0 = zero

case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

case neg
a✝ : PosNum
⊢ neg a✝ + 0 = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ 0 + n = n

Tactic:
cases n

Goal state after:
case zero
⊢ 0 + zero = zero

case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

case neg
a✝ : PosNum
⊢ 0 + neg a✝ = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ (Num.ofNat' 0).toZNum = -(Num.ofNat' 0).toZNum

Tactic:
rw [Num.ofNat'_zero]

Goal state after:
⊢ Num.toZNum 0 = -Num.toZNum 0
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : ↑(const n A) α
⊢ get (f <$$> x) = get x

Tactic:
cases x
  rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α : TypeVec.{u} n
x : ↑(const n A) α
⊢ mk n (get x) = x

Tactic:
cases x
  dsimp [const.get, const.mk]
  congr with (_⟨⟩)

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

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ (node s l x r).size = (node s l x r).realSize

Tactic:
rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ (Num.ofNat' 0).toZNum = 0

Tactic:
rw [Num.ofNat'_zero]

Goal state after:
α : Type u_1
⊢ Num.toZNum 0 = 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False

Tactic:
obtain ⟨r₂, e'⟩ := Nat.le.dest h

Goal state after:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
r₂ : ℕ
e' :
  ↑d + r₂ =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : Num
⊢ n.div 0 = 0

Tactic:
cases n

Goal state after:
case zero
⊢ zero.div 0 = 0

case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : Num
⊢ n.mod 0 = n

Tactic:
cases n

Goal state after:
case zero
⊢ zero.mod 0 = zero

case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : Num
⊢ m ∣ n ↔ n % m = 0

Tactic:
← dvd_to_nat,

Goal state after:
m n : Num
⊢ ↑m ∣ ↑n ↔ n % m = 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ n.div 0 = 0

Tactic:
cases n

Goal state after:
case zero
⊢ zero.div 0 = 0

case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

case neg
a✝ : PosNum
⊢ (neg a✝).div 0 = 0
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inr.refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size > 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
left✝ : rl.size ≤ delta * rr.size
hb₂ : rr.size ≤ delta * rl.size
⊢ l.size ≤ delta * rl.size

Tactic:
exact Valid'.rotateL_lemma₁ H2 hb₂

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

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
exact hl.rotateR_size

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

Goal state before:
pp: m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n

Tactic:
by
  constructor
  · intro h
    rw [← prod_factorMultiset m, ← prod_factorMultiset m]
    apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
    rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]
  · intro h
    rw [← mul_div_exact h, factorMultiset_mul]
    exact le_self_add

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

Goal state before:
pp: u : PrimeMultiset
n : ℕ+
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
let h := @prod_dvd_iff u n.factorMultiset

Goal state after:
u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n.factorMultiset.prod ↔ u ≤ n.factorMultiset := prod_dvd_iff
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hba : b ≤ a
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
exact Or.inr (Lex.right _ hba)

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H : ?m.233
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
refine ⟨vl.balanceL h.right H, ?_⟩

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H :
  (∃ l', Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ r', Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case a
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 α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (wrepr ((P F).wMk a f' f)) ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩))

Tactic:
apply wEquiv.abs'

Goal state after:
case a
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 α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ abs ((P F).wDest' (wrepr ((P F).wMk a f' f))) =
    abs ((P F).wDest' ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨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
      (t_l.size + t_r.size + 1)

Tactic:
have h_glue := Valid'.glue h.left h.right h.bal.1
      obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
      constructor
      · exact h_glue_valid
      · right; rw [h_glue_sized]

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 α
⊢ (wSetoid α) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))
    (wrepr ((P F).wMk a f' f))

Tactic:
apply wEquiv.abs'

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 ((P F).wDest' ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))
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:
cases x
  rfl

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

Goal state before:
pp: case node.gt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < 0 → t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

Tactic:
intro h_pos_t_r_size

Goal state after:
case node.gt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < 0
⊢ t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
⊢ 0 < t_r_size + 1 → t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Tactic:
intro h_pos_t_r_size

Goal state after:
case node.gt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size✝ : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x 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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ (TypeVec.id ::: Sigma.fst) <$$> (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'

Tactic:
MvFunctor.map_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ ((TypeVec.id ::: Sigma.fst) ⊚ (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩)) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'
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
⊢ (prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
MvFunctor.map_map,

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
⊢ ((prod.fst ⊚ subtypeVal R) ⊚ h) <$$> 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
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
by
  let r' (x y) := x = y ∨ r x y
  intro x y rxy
  apply Cofix.bisim_aux r'
  · intro x
    left
    rfl
  · intro x y r'xy
    rcases r'xy with r'xy | r'xy
    · rw [r'xy]
    have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
    rw [← Quot.factor_mk_eq _ _ this]
    dsimp [r']
    rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]
    rw [h _ _ r'xy]
  right; exact rxy

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 ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
MvFunctor.map_map,

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
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⟩⟩ = x

Tactic:
rhs
      rw [← abs_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₁ α)
| abs (repr x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
        Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
MvFunctor.map_map,

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    (((TypeVec.id ::: Quot.mk Mcongr) ⊚
        (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯))) <$$>
      Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    (((TypeVec.id ::: Quot.mk Mcongr) ⊚
        (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯))) <$$>
      Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
MvFunctor.map_map,

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((((TypeVec.id ::: Quot.mk Mcongr) ⊚
          (TypeVec.id :::
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯))) ⊚
        (TypeVec.id ::: Quot.mk Mcongr)) <$$>
      MvQPF.abs (M.dest (P F) a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
        Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr) <$$>
      MvQPF.abs (M.dest (P F) a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
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 : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$> (TypeVec.id ::: f) <$$> g (f x))

Tactic:
MvFunctor.map_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    (((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) ⊚ (TypeVec.id ::: f)) <$$> g (f x))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        corec fun x ↦
          (TypeVec.id ::: fun x ↦ x) <$$>
            Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) <$$>
      (TypeVec.id ::: fun x ↦ x) <$$> (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest

Tactic:
MvFunctor.map_map,

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    (((TypeVec.id :::
          corec fun x ↦
            (TypeVec.id ::: fun x ↦ x) <$$>
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ⊚
        (TypeVec.id ::: fun x ↦ x)) <$$>
      (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest