mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ f X

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X

Tactic:
· apply f.monotone i_ih

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X

Tactic:
· apply hX

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
by
  simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]

Goal state after:
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : ∀ (y : Fin (n + 1)), f y ∈ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin n
ihk : f k.castSucc < x
⊢ f k.succ < x

Tactic:
exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 1)

Tactic:
exact congrArg (α ≃ Fin ·) <| card_eq_one α

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u_1
inst✝¹ : FinEnum α
β : α → Type u_2
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β

Tactic:
by simpa [Pi.enum] using ⟨fun a _ => f a, mem_pi_toList _ _, rfl⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
l₀ l₁ : List (Sigma β)
nd₀ : l₀.Nodup
nd₁ : l₁.Nodup
h : ∀ (x : Sigma β), x ∈ l₀ ↔ x ∈ l₁
⊢ l₀ ~ l₁

Tactic:
grind [perm_ext_iff_of_nodup]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
hd : Sigma β
l₁✝ l₂✝ : List (Sigma β)
a✝ : l₁✝ ~ l₂✝
ih : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
l : List (Sigma β)
⊢ (hd :: l₁✝).kunion l ~ (hd :: l₂✝).kunion l

Tactic:
| cons hd _ ih =>

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))

Tactic:
refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ univ.sigma g ⊂ univ.sigma (update g i (insert x (g i)))
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
by
  simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
    and_iff_right_iff_imp] using Ne.ne_or_ne _

Goal state after:
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
i : ι k
m : M
⊢ (single i m).embSigma = single ⟨k, i⟩ m

Tactic:
classical
  grind

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (↑(m * n)).bodd = ((↑m).bodd && (↑n).bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ (-↑(m * n.succ)).bodd = ((↑m).bodd && -[n+1].bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ (-↑(m.succ * n)).bodd = (-[m+1].bodd && (↑n).bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ (↑(m.succ * n.succ)).bodd = (-[m+1].bodd && -[n+1].bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
exact h_cprankMax_sum

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#({x ∈ Ioc a b | r ∣ x})) = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0

Tactic:
rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst✝ : RightCommutative v
⊢ foldr (flip v) b l = foldl v b l

Tactic:
induction l generalizing b <;> simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l ++ rtakeWhile p l = l

Tactic:
simp only [rdropWhile, rtakeWhile]
  rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]

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

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true

Tactic:
by
    rw [decide_eq_true_eq]
    exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
← List.getElem_map List.length

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = 0

Tactic:
toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)

Goal state after:
case inl
q : ℚ
hq : q ≤ 0
⊢ 0 = 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]

Tactic:
← Int.natCast_modEq_iff

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p) * (n / p).choose (k / p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (fib a + (map fib l).sum).greatestFib = a

Tactic:
simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne',
      not_false_eq_true, le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]

Goal state after:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ a ≤ (map fib l).sum + (fib a + 1) ∧
    ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ n.choose k ≡ ∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Tactic:
← Int.natCast_modEq_iff

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (p * a).choose (p * b) ≡ a.choose b [MOD p]

Tactic:
← Int.natCast_modEq_iff

Goal state after:
a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p * a).choose (p * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]

Tactic:
← Int.natCast_modEq_iff

Goal state after:
k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₂ : p ∣ (Icc 1 (n - 1)).gcd n.choose
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
⊢ p = n.minFac

Tactic:
Finset.dvd_gcd_iff,

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), p ∣ n.choose b
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : q ∣ (Icc 1 (n - 1)).gcd n.choose
⊢ IsPrimePow n

Tactic:
Finset.dvd_gcd_iff,

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), q ∣ n.choose b
⊢ IsPrimePow n
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id ll with _ | lls
        · exact nil
        --should not happen
        rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact nil
        --should not happen
        exact
          if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (lrs + rs + 1) lr x r)
          else
            node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
              (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
t : ℕ
ht : f t = nth p (n + 1)
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty

Tactic:
exact ⟨t, ht ▸ (nth_mem _ h), fun _ hk ↦ ht ▸ nth_lt_nth' hk h⟩

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
by
  constructor
  · rintro ⟨y, hy⟩
    rcases h : y with ⟨a, f⟩
    refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩
    rw [← hy, h, map_eq_map, PFunctor.map_eq]
    congr
  rintro ⟨a, f, xeq, pf⟩
  use ⟨a, fun i => ⟨f i, pf i⟩⟩
  rw [xeq]; rfl

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

Goal state before:
pp: m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m <;> constructor

Goal state after:
case zero.mp
p : PosNum
⊢ pos p = zero → ZNum.pos p = zero.toZNum

case zero.mpr
p : PosNum
⊢ ZNum.pos p = zero.toZNum → pos p = zero

case pos.mp
p a✝ : PosNum
⊢ pos p = pos a✝ → ZNum.pos p = (pos a✝).toZNum

case pos.mpr
p a✝ : PosNum
⊢ ZNum.pos p = (pos a✝).toZNum → pos p = pos a✝
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
by
  cases r <;> simp [rotateL, rotateR]; split_ifs <;>
    simp [dual_node3L, dual_node4L, node3R]

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

Goal state before:
pp: case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d

Tactic:
revert IH

Goal state after:
case bit1
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Tactic:
revert IH

Goal state after:
case bit0
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % ↑d.abs) = ↑↑n % ↑d

Tactic:
abs_to_nat

Goal state after:
n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % (↑d).natAbs) = ↑↑n % ↑d
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', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceL x r) o₂

Tactic:
rw [balanceL_eq_balance' hl.3 hr.3 hl.2 hr.2 H]
  refine hl.balance' hr ?_
  rcases H with (⟨l', e, H⟩ | ⟨r', e, H⟩)
  · exact ⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩
  · exact ⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩

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

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

Tactic:
exact ⟨H.left, rfl⟩

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:
rw [coe_prod, to_ofNatMultiset]

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

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

Tactic:
apply factorMultiset_le_iff.mpr

Goal state after:
case a.left
m n : ℕ+
⊢ m.gcd n ∣ m
Module: Mathlib.Data.PNat.Factors

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

Tactic:
apply factorMultiset_le_iff.mpr

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

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

Tactic:
apply factorMultiset_le_iff.mpr

Goal state after:
case a.left
m n : ℕ+
⊢ m ∣ m.lcm n
Module: Mathlib.Data.PNat.Factors

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

Tactic:
apply factorMultiset_le_iff.mpr

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

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

Tactic:
dsimp only [size_node]; split_ifs
          · simp [node3R, node']; abel
          · simp [node4R, node', sl.2.2.1]; abel

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
⊢ Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size

Tactic:
induction l generalizing o₁ o₂ r with

Goal state after:
case node
α : 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
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
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:
· intro l0; rw [l0] at H
    rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
    · exact balancedSz_zero.1 H.symm
    exact le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)

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

Tactic:
rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]

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

Goal state before:
pp: case node.lt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ 0 < 0 → 0 - 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
intro h_pos_t_l_size

Goal state after:
case node.lt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : 0 < 0
⊢ 0 - 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (erase x t_l).size t_l.size
t_l_size : ℕ
⊢ 0 < t_l_size + 1 → t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
intro h_pos_t_l_size

Goal state after:
case node.lt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (erase x t_l).size t_l.size
t_l_size : ℕ
h_pos_t_l_size : 0 < t_l_size + 1
⊢ t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1