mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: 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)
⊢ ∀ (x y : P.M), R x y → x = y

Tactic:
by

Goal state after:
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⟩
⊢ f = fun i ↦ ⟨(f i).fst, (f i).snd⟩

Tactic:
by

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ (f x).dest = ⟨a, f ∘ f'⟩

Tactic:
by

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩

Tactic:
by

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g

Tactic:
by

Goal state after:
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 α
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ g <$$> f i

Tactic:
by

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

Goal state before:
pp: ⊢ Repr PrimeMultiset

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
⊢ Nat.Prime p

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
⊢ p.Prime

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
⊢ Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
by

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

Goal state before:
pp: p : ℕ+
s : Multiset ℕ
hs : ∀ (p : ℕ), p ∈ s → Nat.Prime p
⊢ p ∈ (ofNatMultiset s hs).toPNatMultiset ↔ ↑p ∈ s

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p

Tactic:
by

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset = v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

Tactic:
by

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

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

Tactic:
dsimp [prod]

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod
Module: Mathlib.Data.PNat.Factors

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (l.node' x r).dual.eraseMax ↑(findMax' x l.dual) ∧ (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
← dual_eraseMin,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (l.node' x r).eraseMin.dual ↑(findMax' x l.dual) ∧ (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
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

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

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
by

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

Goal state before:
pp: l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatList l h).prod = l.prod

Tactic:
by

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

Goal state before:
pp: ⊢ prod 0 = 1

Tactic:
by

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

Goal state before:
pp: u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (node size✝ l x r).eraseMin.Valid

Tactic:
by

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

Goal state before:
pp: d : ℕ
u : PrimeMultiset
⊢ (d • u).prod = u.prod ^ d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.eraseMax.Valid

Tactic:
by

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

Goal state before:
pp: n : ℕ+
⊢ ↑n.factorMultiset.prod = ↑n

Tactic:
by

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

Goal state before:
pp: p n : ℕ+
⊢ p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n

Tactic:
by

Goal state after:
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 α
⊢ (g ::: P.wMap g) <$$> P.objAppend1 a f' f = P.objAppend1 a (g ⊚ f') fun x ↦ P.wMap g (f x)

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p

Tactic:
by

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

Goal state before:
pp: v : PrimeMultiset
⊢ v.prod.factorMultiset = v

Tactic:
by

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

Goal state before:
pp: ⊢ factorMultiset 1 = 0

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ rll.size = 0 ∧ rlr.size = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩

Tactic:
by

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

Goal state before:
pp: n m : ℕ+
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : ↑P (α ::: P.W α)
⊢ P.wDest' (P.wMk' x) = x

Tactic:
by

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

Goal state before:
pp: n : ℕ+
m : ℕ
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
by

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

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b x, p ⟨a, b⟩) ↔ ∃ h, p ⟨n', h⟩

Tactic:
by

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

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
by

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

Goal state before:
pp: p : Nat.Primes
⊢ (↑p).factorMultiset = PrimeMultiset.ofPrime p

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n < PNat.find h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ PNat.find h = 1 ↔ p 1

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ 1 < PNat.find h ↔ ¬p 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m : ℕ+
v : PrimeMultiset
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
by

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1

Tactic:
by

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

Goal state before:
pp: u v : PrimeMultiset
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ #(Ioc a b) = ↑b - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ+
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
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)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H : ?m.112
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
by

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

Goal state before:
pp: m n : ℕ+
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset

Tactic:
by

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

Goal state before:
pp: m : ℕ+
p : Nat.Primes
k : ℕ
⊢ ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset

Tactic:
by

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

Goal state before:
pp: u v : PrimeMultiset
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
by

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

Goal state before:
pp: u v : PrimeMultiset
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ lll.size = 0 ∧ llr.size = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
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)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H : ?m.298
⊢ Valid' o₁
      ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2)
      o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
          (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2).size =
      ls + rs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) l
bal : BalancedSz l.size r.size
⊢ Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
h₁ : 3 * a < b + c + 1
h₂ : b ≤ 3 * c
⊢ 2 * (a + b) ≤ 9 * c + 5

Tactic:
by

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

Goal state before:
pp: u : XgcdType
⊢ u.v = succ₂ u.vp

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
⊢ ∀ (a b c : Σₗ' (i : ι), α i), a ≤ b → b ≤ c → a ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

Goal state before:
pp: u : XgcdType
⊢ u.IsSpecial ↔ u.IsSpecial'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : ?m.119
H₁ : ?m.123
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
by

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

Goal state before:
pp: u : XgcdType
⊢ u.flip.IsReduced ↔ u.IsReduced

Tactic:
by

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

Goal state before:
pp: u : XgcdType
⊢ u.flip.IsSpecial ↔ u.IsSpecial

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b → b ≤ a → a = b

Tactic:
by

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 : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
⊢ delta ≤ rl.size + rr.size

Tactic:
by

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

Goal state before:
pp: case fst
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).1 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).1

Tactic:
simp only

Goal state after:
case fst
u : XgcdType
⊢ ↑u.z * ↑u.b + u.y * ↑u.a = u.y * ↑u.a + ↑u.z * ↑u.b
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∨ b ≤ a

Tactic:
by

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

Goal state before:
pp: case snd
u : XgcdType
⊢ (↑u.z * ↑u.b + u.y * ↑u.a, u.x * ↑u.b + ↑u.w * ↑u.a).2 = (u.y * ↑u.a + ↑u.z * ↑u.b, ↑u.w * ↑u.a + u.x * ↑u.b).2

Tactic:
simp only

Goal state after:
case snd
u : XgcdType
⊢ u.x * ↑u.b + ↑u.w * ↑u.a = ↑u.w * ↑u.a + u.x * ↑u.b
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : ?m.119
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
by

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 : α
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

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

Goal state before:
pp: u : XgcdType
⊢ u.flip.v = u.v.swap

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
by

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

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

Goal state before:
pp: u : XgcdType
hr : u.r = 0
⊢ u.q = u.qp + 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ (start a b).IsSpecial

Tactic:
by

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

Goal state before:
pp: a b : ℕ+
⊢ (start a b).v = (↑a, ↑b)

Tactic:
by

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

Goal state before:
pp: u : XgcdType
⊢ u.finish.IsReduced

Tactic:
by

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

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by

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

Goal state before:
pp: u : XgcdType
hr : u.r = 0
⊢ u.finish.v = u.v

Tactic:
by

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

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
⊢ sizeOf u.step < sizeOf u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ls + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
by

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

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.step.IsSpecial

Tactic:
by

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 : ℕ
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
⊢ delta ≤ ll.size + lr.size

Tactic:
by

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by

Goal state after: