mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
· apply IH
      · simpa using hgs'
      · rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩
      · simpa

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this✝ : i % p < p
this : p ≤ n
⊢ i % p < n + w.length

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
i : ℕ
i_lt : i < w.length - q - k
⊢ i < w.length - q

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
i : ℕ
i_lt : i < w.length - q - k
⊢ i < w.length - (k + q)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
i : ℕ
i_lt : i < w.length - q - k
⊢ i + (k + q) = q + (i + k)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
⊢ p = p - q + q

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ 0 < p - q

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
this : p.gcd q ≤ p - q
⊢ q ≤ w.length - q

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ p - q + q ≤ w.length - q + (p - q).gcd q

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ {b} ≤ M

Tactic:
have : b ∈ a ::ₘ M := by simp [h0]

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
this : b ∈ a ::ₘ M
⊢ {b} ≤ M
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌈↑x⌉ = ⌈↑x⌉

Tactic:
by
  rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
  constructor
  · exact_mod_cast NNRat.cast_strictMono <| Nat.ceil_lt_add_one zero_le
  · rw [Int.cast_natCast, NNRat.cast_le_natCast]
    exact Nat.le_ceil _

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ n < p

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ 0 < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n - m + (m - n) = 0
⊢ n = m

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n - m + (m - n) = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ n - m + (m - n) = m - n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ n - m + (m - n) = n - m

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n - m + (m - n) + n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n + (n - m + (m - n))

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ n - m + (m - n) + m

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ m + (n - m + (m - n))

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ n - 0 + (0 - n) = n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ 0 - n + (n - 0) = n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m - n)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: k n m : ℕ
⊢ k + n - (k + m) + (k + m - (k + n)) = n - m + (m - n)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m k l : ℕ
h : n + m = k + l
⊢ n - k + (k - n) = l - m + (m - l)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m k : ℕ
⊢ n - k + (k - n) ≤ n - m + (m - n) + (m - k + (k - m))

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
⊢ i.succ - j.succ + (j.succ - i.succ) = i - j + (j - i)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
h : i ≠ j
⊢ 0 < i - j + (j - i)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ n ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 < n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
this : multiplicity p n + 1 ≤ multiplicity p n
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
by
  rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_getElem, Fin.getElem_fin]

Goal state after:
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_1
n : PosNum
this : 0 < ↑n
⊢ 2 ≤ ↑n + ↑n + 1

Tactic:
lia

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

Goal state before:
pp: case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
· exact ι x

Goal state after:
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
· exact ι x

Goal state after:
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ b < 3 * a + 1

Tactic:
lia

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

Goal state before:
pp: b c d : ℕ
mr₂ : b + c + 1 ≤ 3 * d
⊢ c ≤ 3 * d

Tactic:
lia

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

Goal state before:
pp: b c d : ℕ
mr₁ : 2 * d ≤ b + c + 1
mm₁ : b ≤ 3 * c
⊢ d ≤ 3 * c

Tactic:
lia

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

Goal state before:
pp: a b c d : ℕ
lr₁ : 3 * a ≤ b + c + 1 + d
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ a + b + 1 ≤ 3 * (c + d + 1)

Tactic:
lia

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

Goal state before:
pp: a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₁ : 2 * d ≤ b + c + 1
mm₂ : c ≤ 3 * b
⊢ c + d + 1 ≤ 3 * (a + b + 1)

Tactic:
lia

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

Goal state before:
pp: case node.inl.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
n✝ : ℕ
r0 : n✝ + 1 + 1 ≤ 1
⊢ (0 + 0 ≤ 1 ∨ 0 ≤ 3 * 0 ∧ 0 ≤ 3 * 0) ∧
    (0 + (n✝ + 1 + 1) ≤ 1 ∨ 0 ≤ 3 * (n✝ + 1 + 1) ∧ n✝ + 1 + 1 ≤ 3 * 0) ∧
      (0 + 0 + 1 + (0 + (n✝ + 1 + 1) + 1) ≤ 1 ∨
        0 + 0 + 1 ≤ 3 * (0 + (n✝ + 1 + 1) + 1) ∧ 0 + (n✝ + 1 + 1) + 1 ≤ 3 * (0 + 0 + 1))

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
⊢ r.size = 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
⊢ l.size = 1

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ ↑(zero * 0) = ↑zero * ↑0

Tactic:
exact (mul_zero _).symm

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
a✝ : PosNum
⊢ ↑(pos a✝ * 0) = ↑(pos a✝) * ↑0

Tactic:
exact (mul_zero _).symm

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
a✝ : PosNum
⊢ ↑(neg a✝ * 0) = ↑(neg a✝) * ↑0

Tactic:
exact (mul_zero _).symm

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 < 2 * ↑d

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
H2 : 3 * a ≤ b + c
hb₂ : c ≤ 3 * b
⊢ a ≤ 3 * b

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
H2 : 3 * a ≤ b + c
h : b < 2 * c
⊢ a + b < 3 * c

Tactic:
lia

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

Goal state before:
pp: a b : ℕ
H3 : 2 * b ≤ 9 * a + 3
⊢ 3 * b ≤ 16 * a + 9

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
l0 : l.size = 0
⊢ rl.size + rr.size ≤ 2

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
l0 : 1 ≤ l.size
⊢ rl.size + rr.size ≤ 2 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
⊢ ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
this : r.size ≤ 3 * (l.size + 1)
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ 1 + 1 ≤ 3 * (l.size + 1)

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
by
  rw [balance']; split_ifs <;> simp [all_node', all_rotateL, all_rotateR]

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

Goal state before:
pp: case inr.inr
α : 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₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
H₂ : r.size ≤ 3 * l.size
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
lia

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

Goal state before:
pp: case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

pp: case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
· have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left

Goal state after:
case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
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₂ (r.dual.node' x l.dual).eraseMax ↑(findMax' x l.dual) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.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_node',

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).dual.eraseMax ↑(findMax' x l.dual) ∧
    (l.node' x r).dual.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
Module: Mathlib.Data.PNat.Factors

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

Tactic:
have := prod_ofPNatMultiset (l : Multiset ℕ+) h
  rw [Multiset.prod_coe] at this
  exact this

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

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

Goal state before:
pp: case inl
α : 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
H : rl.size + rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
lia

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₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ t.size = 0 → rr.size ≤ 1

Tactic:
· rw [e, add_right_comm]; rintro ⟨⟩

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

Goal state before:
pp: case inr
α : 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 ≤ 3 * rl.size
a✝¹ : 1 ≤ t.size
a✝ : 1 ≤ rr.size
⊢ rr.size ≤ 3 * (ll.size + lr.size + 1 + rl.size)

Tactic:
lia

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

Goal state before:
pp: case pos
α : 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 α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))

Tactic:
simp [node3R, node', sl.1]

Goal state after:
case pos
α : 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 α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : lrs < ratio * lls
⊢ lls + (lrs + rs + 1) = lls + lrs + 1 + rs
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H2.inr.inl.intro
α : 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
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ 3 * l.size

Tactic:
lia

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

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

Tactic:
· refine Valid'.glue_aux hl hr sep (Or.inr ⟨not_lt.1 h_1, not_lt.1 h⟩)

Goal state after: