mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ k * X ^ (p * k') * ↑((n % p).choose k) * ↑((n / p).choose k')

Tactic:
← pow_add,

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ (k + p * k') * ↑((n % p).choose k) * ↑((n / p).choose k')
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (n + 1).zeckendorf.IsZeckendorfRep

Tactic:
rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
    refine (isZeckendorfRep_zeckendorf _).cons (fun a ha ↦ ?_)
    obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
    · simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
      subst ha
      exact le_greatestFib.2 le_add_self
    rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha
    subst a
    exact add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
      (greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ n.minFac ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
obtain ⟨k, _, _, hn₁⟩ := (isPrimePow_nat_iff_bounded_log_minFac _).mp h

Goal state after:
n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
⊢ n.minFac ∣ (Icc 1 (n - 1)).gcd n.choose
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Tactic:
nth_lt_nth hf,

Goal state after:
case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : n < k + 1
ha : p (nth p n)
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Ordmap.Ordnode

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

pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact ι x
    · rcases id rr with _ | rrs
      · rcases rl with _ | ⟨_, _, rlx⟩
        · exact node 2 nil x r
        · exact node 3 (ι x) rlx ι rx
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit1 = ↑(pos p) + ↑(pos p) + 1

Tactic:
by rw [ZNum.bit1, cast_pos, cast_pos]; rfl

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

Goal state before:
pp: p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ n' ≥ n

Tactic:
by simpa using hp

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑b.pred'.toZNumNeg = ↑1 - ↑b

Tactic:
Num.cast_toZNumNeg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ -↑b.pred' = ↑1 - ↑b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a ≤ a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a + b + c = a + (b + c)

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), -a + a = 0

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a + b = b + a

Tactic:
transfer

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

Goal state before:
pp: ⊢ ∀ (a b : ZNum), a * b = b * a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
a b c : ZNum
⊢ a * b * c = a * (b * c)

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), 1 * a = a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a * 1 = a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), 0 * a = 0

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a * 0 = 0

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a * (b + c) = a * b + a * c

Tactic:
transfer

Goal state after:
α : Type u_1
a✝ b✝ c✝ : ZNum
⊢ ↑a✝ * (↑b✝ + ↑c✝) = ↑a✝ * ↑b✝ + ↑a✝ * ↑c✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), (a + b) * c = a * c + b * c

Tactic:
transfer

Goal state after:
α : Type u_1
a✝ b✝ c✝ : ZNum
⊢ ↑c✝ * (↑a✝ + ↑b✝) = ↑a✝ * ↑c✝ + ↑b✝ * ↑c✝
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.succ.zero
α : 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 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
mm : n✝ + 1 + 0 ≤ 1
⊢ BalancedSz 1 (n✝ + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (0 + 1 + 1)

pp: case pos.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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝¹ n✝ : ℕ
mm : n✝¹ + 1 + (n✝ + 1) ≤ 1
⊢ BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)

Tactic:
· rcases mm with (_ | ⟨⟨⟩⟩); decide

Goal state after:
case pos.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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝¹ n✝ : ℕ
mm : n✝¹ + 1 + (n✝ + 1) ≤ 1
⊢ BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ a₁ = a₂

Tactic:
refine
      PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
        ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ∀ (x y : P.last.M),
    (∃ x_1 y_1, R x_1 y_1 ∧ x_1.fst = x ∧ y_1.fst = y) →
      ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : r.Sized
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
by
  cases r <;> simp [Ordnode.rotateL]
  simp only [hm.1]
  split_ifs <;> simp [node3L_size, node4L_size hm.2.1] <;> abel

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

Goal state before:
pp: case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

Tactic:
apply Relation.EqvGen.is_equivalence

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

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1

Tactic:
rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
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⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i ↦ ⟨(f i).fst, (f i).snd⟩) = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩

Tactic:
rw [wMk_eq, wMk_eq]

Goal state after:
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⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ g <$$> ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn f' fun i ↦ (f i).snd⟩ =
    ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn (g ⊚ f') fun i ↦ g ⊚ (f i).snd⟩
Module: Mathlib.Data.PNat.Find

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

Tactic:
simp [h1]

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

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

Tactic:
← Nat.card_uIcc,

Goal state after:
a b : ℕ+
⊢ #(uIcc a b) = #(uIcc ↑a ↑b)
Module: Mathlib.Data.PNat.Factors

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

Tactic:
← PrimeMultiset.prod_dvd_iff,

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

Goal state before:
pp: case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Tactic:
· exact inf_le_right

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

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

Tactic:
← PrimeMultiset.prod_dvd_iff,

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

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

Tactic:
let m := v.prod

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod
Module: Mathlib.Data.PNat.Factors

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

Tactic:
let m := v.prod

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : 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 :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).eraseMin.size + 1 = ls + rs

Tactic:
add_assoc,

Goal state after:
case refine_3
α : 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 :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ (Ordnode.node ls ll lx lr).size + ((rl.node' rx rr).eraseMin.size + 1) = ls + rs
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 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)) =
    if lls + lrs + 1 ≤ 1 then ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).node' x nil
    else ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).rotateR x nil

Tactic:
symm; rw [if_neg, rotateR]
        · dsimp only [size_node]; split_ifs
          · simp [node3R, node']; abel
          · simp [node4R, node', sl.2.2.1]; abel
        · exact not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))

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

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

Tactic:
by
  dsimp [IsSpecial, flip]
  rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H : ?m.362
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
refine ⟨h.left.balanceR vr H, ?_⟩
        rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
        exact (e.add_left _).add_right _

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_2
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀✝ : (P F).A
f'₀✝ : (P F).drop.B a₀✝ ⟹ α
f₀✝ : (P F).last.B a₀✝ → (P F).W α
a₁✝ : (P F).A
f'₁✝ : (P F).drop.B a₁✝ ⟹ α
f₁✝ : (P F).last.B a₁✝ → (P F).W α
h✝ : WEquiv ((P F).wMk a₀✝ f'₀✝ f₀✝) ((P F).wMk a₁✝ f'₁✝ f₁✝)
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

Tactic:
simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec.{u} n
x : G α✝
⊢ FG_abs (abs (repr (FG_repr x))) = x

Tactic:
by rw [abs_repr, FG_abs_repr]

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

Goal state before:
pp: case node.lt
α : 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_h : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_l_h

Goal state after:
case node.lt
α : 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
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : 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₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_l := t_ih_l' h_mem
      clear t_ih_l' t_ih_r'
      have t_l_h := Valid'.erase_aux x h.left
      obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
      rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz
          (Or.inl (Exists.intro t_l.size (And.intro t_l_size h.bal.1)))]
      rw [t_ih_l, h.sz.1]
      have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
      revert h_pos_t_l_size; rcases t_l.size with - | t_l_size <;> intro h_pos_t_l_size
      · cases h_pos_t_l_size
      · simp [Nat.add_right_comm]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_pos hp, one_mul]

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ Functor.Comp F₂ F₁ α → ↑((P F₂).comp (P F₁)) α

Tactic:
dsimp [Functor.Comp]
    intro y
    refine ⟨⟨(repr y).1, fun u => (repr ((repr y).2 u)).1⟩, ?_⟩
    dsimp [PFunctor.comp]
    intro x
    exact (repr ((repr y).2 x.1)).snd x.2

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α : Type u
x : G α
⊢ FG_abs (abs (repr (FG_repr x))) = x

Tactic:
by rw [abs_repr, FG_abs_repr]

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

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → p u

Tactic:
rintro ⟨a, f, xeq, h'⟩

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
⊢ p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = f '' univ

Tactic:
ext u; rw [mem_supp]; constructor
  · intro h'
    apply h' _ _ rfl
  intro h' a' f' e
  rw [← h _ _ _ _ e.symm]; apply h'

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s : WSeq α
⊢ LiftRel R s s

Tactic:
by
    refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
    rw [← h]
    apply Computation.LiftRel.refl _ |>.refl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ ∀ {a : WSeq α} {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct

Tactic:
intro a b ab

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
⊢ Computation.LiftRel (LiftRelO R S) a.destruct b.destruct