mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ g <$$> ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn f' fun i ↦ (f i).snd⟩ =
    P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩

Tactic:
wMk_eq

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ g <$$> ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn f' fun i ↦ (f i).snd⟩ =
    ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn (g ⊚ f') fun i ↦ g ⊚ (f i).snd⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
this : ∀ (p : ℕ), p ∈ l' → Nat.Prime p
⊢ ↑(List.map Subtype.val l).prod.primeFactorsList = ↑(List.map Subtype.val l)

Tactic:
exact Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm

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

Goal state before:
pp: u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp

Tactic:
constructor <;> intro h <;> exact h.symm

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

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size

Tactic:
induction r generalizing o₁ o₂ with
  | nil => exact ⟨hl, rfl⟩
  | node rs rl rx rr IHrl _ => ?_

Goal state after:
case node.node
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rl o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rl) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih✝ :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rr o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rr) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
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)
⊢ LiftP p x

Tactic:
use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩

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)
⊢ (fun i ↦ Subtype.val) <$$> abs ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩ = x
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)
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩) = x

Tactic:
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.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ⊚ g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ⊚ g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)

Tactic:
id_comp,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv (g <$$> (P F).wMk a f' f₀) (g <$$> (P F).wMk a f' f₁)

Tactic:
rw [q.P.w_map_wMk, q.P.w_map_wMk]

Goal state after:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₀ i) ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₁ i)
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)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = x

Tactic:
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.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv (g <$$> (P F).wMk a₀ f'₀ f₀) (g <$$> (P F).wMk a₁ f'₁ f₁)

Tactic:
rw [q.P.w_map_wMk, q.P.w_map_wMk]

Goal state after:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₀ (g ⊚ f'₀) fun i ↦ g <$$> f₀ i) ((P F).wMk a₁ (g ⊚ f'₁) fun i ↦ g <$$> f₁ i)
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
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ (TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)

Tactic:
h₀

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
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ (TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b) =
    (TypeVec.id ::: f) <$$> (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
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⟩
⊢ g ((TypeVec.id ⊚ TypeVec.id ::: recF g ∘ fixToW) <$$> x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
id_comp,

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 ((TypeVec.id ::: recF g ∘ fixToW) <$$> x) = g ((TypeVec.id ::: rec g) <$$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (Quot.mk (⇑Wsetoid) (WType.mk a f)) = g₂ (Quot.mk (⇑Wsetoid) (WType.mk a f))

Tactic:
change g₁ ⟦⟨a, f⟩⟧ = g₂ ⟦⟨a, f⟩⟧

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ ⟦WType.mk a f⟧ = g₂ ⟦WType.mk a f⟧
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 y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩

Tactic:
id_comp,

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 y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs ⟨a, splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩
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 : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
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)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = abs ((P F).map (f ∘ Quot.mk r ∘ Quot.mk Mcongr) b.dest)

Tactic:
h₀

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
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)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest = abs ((P F).map (f ∘ Quot.mk r ∘ Quot.mk Mcongr) b.dest)
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 =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]

Goal state after:
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) <$$>
      (TypeVec.id ::: corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
        (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
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 ⊚ TypeVec.id :::
        ((Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) ∘ fun i ↦
          i.dest) <$$>
      y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
id_comp,

Goal state after:
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) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) ∘ fun i ↦
          i.dest) <$$>
      y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
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 : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ⊚ TypeVec.id ::: _root_.id) <$$> x = x

Tactic:
id_comp,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: _root_.id) <$$> x = x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ (↑0).sign = ↑(Int.sign 0)

Tactic:
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ SuppPreservation ↔ LiftpPreservation

Tactic:
by
  constructor <;> intro h
  · rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_uniform] at h'
    dsimp only [SuppPreservation, supp] at h
    rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
    simp
  · rintro α ⟨a, f⟩
    simp only [LiftpPreservation] at h
    simp only [supp, h]

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

Goal state before:
pp: case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
have := mem_unique td (ret_mem _)

Goal state after:
case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case step
α : Type u
s : WSeq α
m n m✝ : ℕ
a✝ : m.le m✝
IH : (s.get? m✝).Terminates → (s.get? m).Terminates
⊢ (s.get? m✝.succ).Terminates → (s.get? m).Terminates

Tactic:
| step _ IH =>

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) none p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
rcases p with - | b

Goal state after:
case none.none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
h : LiftRelO R (LiftRel R) none none
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) none)

case none.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
b : β × WSeq β
h : LiftRelO R (LiftRel R) none (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) (some b))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
rcases p with - | b

Goal state after:
case some.none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) none)

case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))
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)
⊢ x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
hxs

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
⊢ x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t