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

Goal state before:
pp: u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)

Tactic:
]

Goal state after:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)
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
this : delta * Nat.succ 0 ≤ ll.size + lr.size
⊢ delta ≤ ll.size + lr.size

Tactic:
]

Goal state after:
α : 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
this : delta * Nat.succ 0 ≤ ll.size + lr.size
⊢ delta ≤ ll.size + lr.size
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * u.r = u.y * (u.r + ↑u.b * u.q) + ↑u.z * ↑u.b

Tactic:
]

Goal state after:
case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * u.r = u.y * (u.r + ↑u.b * u.q) + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * u.r = ↑u.w * (u.r + ↑u.b * u.q) + u.x * ↑u.b

Tactic:
]

Goal state after:
case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * u.r = ↑u.w * (u.r + ↑u.b * u.q) + u.x * ↑u.b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.nil
α : 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
⊢ (node ls nil lx lr).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil

Tactic:
]

Goal state after:
case pos.nil
α : 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
⊢ (node ls nil lx lr).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Tactic:
]

Goal state after:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip

Tactic:
]

Goal state after:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.finish.IsReduced

Tactic:
]

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.finish.IsReduced
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.reduce.IsReduced

Tactic:
]

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.IsReduced
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
]

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ u.finish.IsSpecial
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial

Tactic:
]

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.v = x✝.v

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ ∏ i, #(Icc (a i) (b i)) - 1 = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ ∏ i, #(Icc (a i) (b i)) - 2 = ∏ i, #(Icc (a i) (b i)) - 2

Tactic:
]

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.v = x✝.v

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ ∏ i, #(Iic (b i)) - 1 = ∏ i, #(Iic (b i)) - 1

Tactic:
]

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

Goal state before:
pp: a b : ℕ+
⊢ (a.xgcd b).wp + 1 + (a.xgcd b).x = (a.xgcd b).wp + 1 + (a.xgcd b).x

Tactic:
]

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

Goal state before:
pp: a b : ℕ+
⊢ (a.xgcd b).y + ((a.xgcd b).zp + 1) = (a.xgcd b).y + ((a.xgcd b).zp + 1)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ ∏ i, #(Ici (a i)) - 1 = ∏ i, #(Ici (a i)) - 1

Tactic:
]

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ TypeVec.id <$$> x = x

Tactic:
rw [← abs_repr x, ← abs_map]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)
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 α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
]

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ ↑(f i j)⟩
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, ⋯⟩⟩) = abs ⟨a, f⟩

Tactic:
]

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.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ (x * y).succ = x * y + 1

Tactic:
]

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

Goal state before:
pp: case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
]

Goal state after:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> u = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
← abs_repr u,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> abs (repr u) = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
]

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> u = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
← abs_repr u,

Goal state after:
case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> abs (repr u) = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
]

Goal state after:
case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size = 0 ∧ rr.size = 0
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
]

Goal state after:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size = 0 ∧ rr.size = 0
⊢ rl.size = 0 ∧ rr.size = 0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)

Tactic:
]

Goal state after:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
]

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ x * y + 1 + ↑z * x = x * y + x * ↑z + 1

Tactic:
]

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ x * y + 1 + ↑z * x = x * y + x * ↑z + 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
]

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * y + (x * y + 1) = y * ↑w + y * x + 1

Tactic:
]

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * y + (x * y + 1) = y * ↑w + y * x + 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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 ⟹ α
haf : abs ⟨a, f⟩ = x
⊢ ∃ a_1 f_1, x = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ

Tactic:
]

Goal state after:
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 ⟹ α
haf : abs ⟨a, f⟩ = x
⊢ ∃ a_1 f_1, x = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ m ≤ n + 1

Tactic:
]

Goal state after:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ m ≤ n + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
]

Goal state after:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
]

Goal state after:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)

Tactic:
]

Goal state after:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ x * ↑b' + 1 = x * ↑b' + 1

Tactic:
]

Goal state after:
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
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.balance x r = l.balance x r

pp: case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.size = 0 → r.size ≤ 1

pp: case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size

Tactic:
]

Goal state after:
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.size = 0 → r.size ≤ 1

case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size