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

Goal state before:
pp: case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

pp: case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4R x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4R x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
⊢ All P (l.rotateL x nil) ↔ All P l ∧ P x ∧ All P nil

pp: case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.rotateL x (node size✝ l✝ x✝ r✝)) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
⊢ All P (l.rotateL x nil) ↔ All P l ∧ P x ∧ All P nil

case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.rotateL x (node size✝ l✝ x✝ r✝)) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : l✝.size < ratio * r✝.size
⊢ All P (l.node3L x l✝ x✝ r✝) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

pp: case neg
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : ¬l✝.size < ratio * r✝.size
⊢ All P (l.node4L x l✝ x✝ r✝) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : l✝.size < ratio * r✝.size
⊢ All P (l.node3L x l✝ x✝ r✝) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

case neg
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : ¬l✝.size < ratio * r✝.size
⊢ All P (l.node4L x l✝ x✝ r✝) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝ : l.size + r.size ≤ 1
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

pp: case neg
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝ : l.size + r.size ≤ 1
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

case neg
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r
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.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balanceL x r) o₂

Tactic:
rw [balanceL_eq_balance hl.2 hr.2 H₁ H₂, balance_eq_balance' hl.3 hr.3 hl.2 hr.2]

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.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balance' x r) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
x : α
⊢ Any (Eq x) nil ↔ x ∈ nil.toList

pp: case node
α : Type u_1
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
l_ih✝ : Any (Eq x) l✝ ↔ x ∈ l✝.toList
r_ih✝ : Any (Eq x) r✝ ↔ x ∈ r✝.toList
⊢ Any (Eq x) (node size✝ l✝ x✝ r✝) ↔ x ∈ (node size✝ l✝ x✝ r✝).toList

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
x : α
⊢ Any (Eq x) nil ↔ x ∈ nil.toList

case node
α : Type u_1
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
l_ih✝ : Any (Eq x) l✝ ↔ x ∈ l✝.toList
r_ih✝ : Any (Eq x) r✝ ↔ x ∈ r✝.toList
⊢ Any (Eq x) (node size✝ l✝ x✝ r✝) ↔ x ∈ (node size✝ l✝ x✝ r✝).toList
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
⊢ nil.merge nil = nil

pp: case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).merge nil = node size✝ l✝ x✝ r✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ nil.merge nil = nil

case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).merge nil = node size✝ l✝ x✝ r✝
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a a' : P.A} {f : P.B a → P.M} {f' : P.B a' → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩) → a = a'

pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a : P.A} {f f' : P.B a → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → ∀ (i : P.B a), R (f i) (f' i)

Tactic:
<;>

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a a' : P.A} {f : P.B a → P.M} {f' : P.B a' → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩) → a = a'

case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a : P.A} {f f' : P.B a → P.M}, R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → ∀ (i : P.B a), R (f i) (f' i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
⊢ a = a'

pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
⊢ R (f i) (f' i)

Tactic:
<;>

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
⊢ a = a'

case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
⊢ R (f i) (f' i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rr : Ordnode α
hr : (nil.node' rx rr).Balanced
sr : (node rs nil rx rr).Sized
⊢ nil.balance x (nil.node' rx rr) = nil.balance' x (nil.node' rx rr)

pp: case nil.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx rr) = nil.balance' x ((node rls rll rlx rlr).node' rx rr)

Tactic:
<;>

Goal state after:
case nil.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rr : Ordnode α
hr : (nil.node' rx rr).Balanced
sr : (node rs nil rx rr).Sized
⊢ nil.balance x (nil.node' rx rr) = nil.balance' x (nil.node' rx rr)

case nil.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx rr) = nil.balance' x ((node rls rll rlx rlr).node' rx rr)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
<;>

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
hr : (nil.node' rx nil).Balanced
sr : (node rs nil rx nil).Sized
⊢ nil.balance x (nil.node' rx nil) = nil.balance' x (nil.node' rx nil)

pp: case nil.node.nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ nil.balance x (nil.node' rx (node rrs rrl rrx rrr)) = nil.balance' x (nil.node' rx (node rrs rrl rrx rrr))

pp: case nil.node.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx nil) = nil.balance' x ((node rls rll rlx rlr).node' rx nil)

pp: case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
    nil.balance' x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))

Tactic:
<;>

Goal state after:
case nil.node.nil.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
hr : (nil.node' rx nil).Balanced
sr : (node rs nil rx nil).Sized
⊢ nil.balance x (nil.node' rx nil) = nil.balance' x (nil.node' rx nil)

case nil.node.nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ nil.balance x (nil.node' rx (node rrs rrl rrx rrr)) = nil.balance' x (nil.node' rx (node rrs rrl rrx rrr))

case nil.node.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx nil) = nil.balance' x ((node rls rll rlx rlr).node' rx nil)

case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
    nil.balance' x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.root a f i c✝) = h i (WPath.root a f i c✝)

pp: case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.child a f i j✝ c✝) = h i (WPath.child a f i j✝ c✝)

Tactic:
<;>

Goal state after:
case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.root a f i c✝) = h i (WPath.root a f i c✝)

case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.child a f i j✝ c✝) = h i (WPath.child a f i j✝ c✝)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.root a f i c✝) = P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.root a f i c✝)

pp: case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.child a f i j✝ c✝) =
    P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.child a f i j✝ c✝)

Tactic:
<;>

Goal state after:
case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.root a f i c✝) = P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.root a f i c✝)

case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.child a f i j✝ c✝) =
    P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.child a f i j✝ c✝)
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ ↑(ofNatMultiset v h).prod = v.prod

Tactic:
by rw [coe_prod, to_ofNatMultiset]

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

Goal state before:
pp: p : ℕ+
l : List ℕ
hl : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ p ∈ (ofNatList l hl).toPNatMultiset ↔ ↑p ∈ l

Tactic:
by
  simp [ofNatList]

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

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
← PrimeMultiset.prod_add

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then nil.node' x ((node rls rll rlx rlr).node' rx nil)
    else nil.rotateL x ((node rls rll rlx rlr).node' rx nil)

Tactic:
have : size rll = 0 ∧ size rlr = 0 := by
          have := balancedSz_zero.1 hr.1
          rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
        cases sr.2.1.2.1.size_eq_zero.1 this.1
        cases sr.2.1.2.2.size_eq_zero.1 this.2
        obtain rfl : rls = 1 := sr.2.1.1
        rw [if_neg, rotateL_node, if_neg]; · rfl
        all_goals (try dsimp only [size]); decide

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

Goal state before:
pp: case a.left
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset

pp: case a.right
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ n.factorMultiset

Tactic:
<;>

Goal state after:
case a.left
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset

case a.right
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m

pp: case a.hn
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n

Tactic:
<;>

Goal state after:
case a.hm
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m

case a.hn
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

pp: case a.hn
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
<;>

Goal state after:
case a.hm
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

case a.hn
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.left
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset

pp: case a.right
m n : ℕ+
⊢ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
<;>

Goal state after:
case a.left
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset

case a.right
m n : ℕ+
⊢ n.factorMultiset ≤ (m.lcm n).factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx lr).Balanced
sl : (node ls nil lx lr).Sized
⊢ (nil.node' lx lr).balance x nil = (nil.node' lx lr).balance' x nil

pp: case node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
⊢ ((node lls lll llx llr).node' lx lr).balance x nil = ((node lls lll llx llr).node' lx lr).balance' x nil

Tactic:
<;>

Goal state after:
case node.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx lr).Balanced
sl : (node ls nil lx lr).Sized
⊢ (nil.node' lx lr).balance x nil = (nil.node' lx lr).balance' x nil

case node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
⊢ ((node lls lll llx llr).node' lx lr).balance x nil = ((node lls lll llx llr).node' lx lr).balance' x nil