mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset

Tactic:
intro h

Goal state after:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.left
m n : ℕ+
⊢ m.gcd n ∣ m

pp: case a.right
m n : ℕ+
⊢ m.gcd n ∣ n

Tactic:
· exact gcd_dvd_left m n

Goal state after:
case a.right
m n : ℕ+
⊢ m.gcd n ∣ n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)

pp: case neg
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : ¬lrs < ratio * lls
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)

Tactic:
· simp [node3R, node']; abel

Goal state after:
case neg
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : ¬lrs < ratio * lls
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

Tactic:
intro h

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y

Tactic:
intro h

Goal state after:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
⊢ u.bp = u.ap → u.ap = u.bp

Tactic:
intro h

Goal state after:
case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mpr
u : XgcdType
⊢ u.ap = u.bp → u.bp = u.ap

Tactic:
intro h

Goal state after:
case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
hlt₁.antisymm hlt₂

Goal state after:
case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₂✝⟩ = ⟨a₁, b₂✝⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ ¬delta ≤ 1

Tactic:
by decide

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

Goal state before:
pp: case pos.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      nil

Tactic:
exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
rd : delta ≤ (node rls rll rlx rlr).size + nil.size
⊢ ¬delta ≤ 1

Tactic:
by decide

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

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
rw [this, ← ha, u.qp_eq hr]

Goal state after:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * (↑u.b * (u.qp + 1)) + u.x * ↑u.b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ lr.size
⊢ ¬delta ≤ 1

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
ld : delta ≤ (node lls lll llx llr).size + nil.size
⊢ ¬delta ≤ 1

Tactic:
by decide

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.v.swap = x✝.v

Tactic:
step_v u h,

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.v.swap.swap = x✝.v
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> x = g <$$> f <$$> x

Tactic:
rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]
  rfl

Goal state after:
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 α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) →
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
intro h

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
⊢ ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
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 α
⊢ (∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u) →
    ∃ a f,
      abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

Tactic:
intro 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 f,
    abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ 0 < delta

Tactic:
by decide

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

Goal state before:
pp: case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ a.gcdX b * ↑b + ↑(a.gcdD b)
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ a.gcd b ∣ a.gcdD b

Tactic:
dvd_iff

Goal state after:
case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ a.gcdX b * ↑b + ↑(a.gcdD b)
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ ↑(a.gcd b) ∣ ↑(a.gcdD b)
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
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H : ?m.362
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
by
        refine ⟨h.left.balanceR vr H, ?_⟩
        rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
        exact (e.add_left _).add_right _

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 α
⊢ recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
rw [recF, MvPFunctor.wRec_eq]

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' fun i ↦ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation → IsUniform

Tactic:
intro h

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
⊢ IsUniform
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insert' x t).Valid

Tactic:
rw [insert'_eq_insertWith]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid
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
u : F (α ::: β) → β
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 α
⊢ WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁) → recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

Tactic:
intro h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
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 : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ f x✝¹ '' univ ↔ x✝ ∈ supp ⟨a, f⟩ x✝¹

pp: case mpr.h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ IsUniform

Tactic:
MvPFunctor.supp_eq

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ f x✝¹ '' univ ↔ x✝ ∈ f x✝¹ '' univ

case mpr.h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ IsUniform
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation → LiftPPreservation

Tactic:
intro h

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation → SuppPreservation

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation

Tactic:
constructor <;> intro h
  · rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_isUniform] at h'
    dsimp only [SuppPreservation, supp] at h
    simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
      image_univ, mem_range, exists_imp]
    constructor <;> intros <;> subst_vars <;> solve_by_elim
  · rintro α ⟨a, f⟩
    simp only [LiftPPreservation] at h
    ext
    simp only [supp, h, mem_ofPred_eq]

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
x y : (P F).W α
⊢ WEquiv x y → WEquiv y x

Tactic:
intro h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv y 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 y : (P F).W α
⊢ WEquiv x y → WEquiv (g <$$> x) (g <$$> y)

Tactic:
intro h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ u, abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)

Tactic:
constructor
  · rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use ⟨a, fun i => (f i).val⟩
    dsimp
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]
      rfl
    intro i
    apply (f i).property
  rintro ⟨⟨a, f⟩, h₀, h₁⟩; dsimp at *
  use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
  rw [← abs_map, ← h₀]; rfl

Goal state after:
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

Goal state after:
case mk
F : Type u → Type v
q : QPF F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk a✝ f✝))))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
⊢ Wequiv x y → recF u x = recF u y

Tactic:
intro h

Goal state after:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
⊢ recF u x = recF u y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y

Tactic:
cases x

Goal state after:
case mk
F : Type u → Type v
q : QPF F
y : (P F).W
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝)) = QPF.abs y.dest
⊢ Wequiv (WType.mk a✝ f✝) y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
⊢ Wequiv x y → Wequiv y x

Tactic:
intro h

Goal state after:
F : Type u → Type v
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x
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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ (t_l.glue t_r).size = (node size✝ t_l t_x t_r).size - 1

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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
· rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]; rfl

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₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
intro h

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x →
    mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x

Tactic:
intro h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) → ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

Tactic:
intro h

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
⊢ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ) → ∀ ⦃p : α → Prop⦄, Liftp p x → p u

Tactic:
intro h

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
⊢ ∀ ⦃p : α → Prop⦄, Liftp p x → p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
intro h

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → IsUniform

Tactic:
intro h

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ IsUniform