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

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ splitBy r (a :: (l ++ m)) = (a :: l) :: splitBy r m

Tactic:
splitBy,

Goal state after:
case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ splitBy.loop r (l ++ m) a [] [] = (a :: l) :: splitBy r m
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: p n : ℕ
hp : Prime p
hn : n < p
⊢ ¬p ∣ n !

Tactic:
hp.dvd_factorial,

Goal state after:
p n : ℕ
hp : Prime p
hn : n < p
⊢ ¬p ≤ n
Module: Mathlib.Data.Nat.Choose.Dvd

Goal state before:
pp: p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ∣ a !) ∨ p ∣ b !
⊢ p ∣ (a + b).choose a

Tactic:
hp.dvd_factorial,

Goal state after:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ∣ b !
⊢ p ∣ (a + b).choose a
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ∀ i ∈ t.val, s i ≠ 0

Tactic:
by simpa using hs

Goal state after:
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)
⊢ ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x

Tactic:
intro ⟨x₁, x₂⟩ hx

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ (k % p, k / p) = (x₁, x₂)
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
a : ℕ
h✝ : a = 0
⊢ 0 = a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun p k ↦ p ^ k) = a

Tactic:
simp [*]

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

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : a = 0
⊢ 0 = a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a

Tactic:
simp [*]

Goal state after:
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)) [ZMOD ↑p]

Tactic:
by
  have decompose : ((X : (ZMod p)[X]) + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p) := by
    simpa using add_pow_eq_mul_pow_add_pow_div_char (X : (ZMod p)[X]) 1 p _
  simp only [← ZMod.intCast_eq_intCast_iff,
    ← coeff_X_add_one_pow _ n k, ← eq_intCast (Int.castRingHom (ZMod p)), ← coeff_map,
    Polynomial.map_pow, Polynomial.map_add, Polynomial.map_one, map_X, decompose]
  simp only [add_pow, one_pow, mul_one, ← pow_mul, sum_mul_sum]
  conv_lhs =>
    enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]
  have h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      k = x.1 + p * x.2 ↔ (k % p, k / p) = x := by
    intro ⟨x₁, x₂⟩ hx
    rw [Prod.mk.injEq]
    constructor <;> intro h
    · simp only [mem_product, mem_range] at hx
      have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
      rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
      exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩
    · rw [← h.left, ← h.right, mod_add_div]
  simp only [finsetSum_coeff, coeff_mul_natCast, coeff_X_pow, ite_mul, zero_mul, ← cast_mul]
  rw [← sum_product', sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl), sum_ite_eq]
  split_ifs with h
  · simp
  · rw [mem_product, mem_range, mem_range, not_and_or, Nat.lt_succ_iff, not_le, not_lt] at h
    cases h <;> simp [choose_eq_zero_of_lt (by tauto)]

Goal state after:
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₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
⊢ p = n.minFac

Tactic:
have := eq_pow_multiplicity_of_choose_modEq_zero_nat h.pos hp₂

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), n.choose b ≡ 0 [MOD p]
this : n = p ^ multiplicity p n
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n

pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
· simp only [or_iff_not_imp_right, not_exists, not_le]
    exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩

Goal state after:
case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
simp [*]

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

Goal state before:
pp: case mp
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)

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

Tactic:
· 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

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)) → Liftp p x
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✝ : ℕ
⊢ n✝ + 1 + 1 ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (n✝ + 1 + 1) ∧ BalancedSz (0 + 0 + 1) (0 + (n✝ + 1 + 1) + 1)

Tactic:
intro r0

Goal state after:
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
⊢ BalancedSz 0 0 ∧ BalancedSz 0 (n✝ + 1 + 1) ∧ BalancedSz (0 + 0 + 1) (0 + (n✝ + 1 + 1) + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1

Tactic:
rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
⊢ LiftR r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
constructor
  · rintro ⟨u, xeq, yeq⟩
    rcases h : u with ⟨a, f⟩
    use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
    constructor
    · rw [← xeq, h]
      rfl
    constructor
    · rw [← yeq, h]
      rfl
    intro i j
    exact (f i j).property
  rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
  exact ⟨⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩, xeq.symm, yeq.symm⟩

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

Goal state before:
pp: case mp.succ.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
y : F.M
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree ((M.mk ⟨a✝, f✝⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) y

Tactic:
induction y using PFunctor.M.casesOn'

Goal state after:
case mp.succ.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree ((M.mk ⟨a✝¹, f✝¹⟩).approx (n✝ + 1)) ((M.mk ⟨a✝, f✝⟩).approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝¹, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree' n✝ (x' i) (y' i)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : ¬a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
simp [*]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
⊢ x.fst = (M.mk x).dest.fst

Tactic:
rw [dest_mk]

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

Goal state before:
pp: case zero.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
y z : F.M
hy : Agree' 0 z y
a✝ : F.A
f✝ : F.B a✝ → F.M
hx : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : iselect [] (M.mk ⟨a✝, f✝⟩) = iselect [] y
⊢ (M.mk ⟨a✝, f✝⟩).approx (0 + 1) = y.approx (0 + 1)

Tactic:
induction y using PFunctor.M.casesOn'

Goal state after:
case zero.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
hx : Agree' 0 z (M.mk ⟨a✝¹, f✝¹⟩)
a✝ : F.A
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : iselect [] (M.mk ⟨a✝¹, f✝¹⟩) = iselect [] (M.mk ⟨a✝, f✝⟩)
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
y z : F.M
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : z = M.mk ⟨a✝⁸, x✝¹⟩
a✝⁵ : F.A
x✝ y✝ : F.B a✝⁵ → F.M
a✝⁴ : ∀ (i : F.B a✝⁵), Agree' n (x✝ i) (y✝ i)
a✝³ : z = M.mk ⟨a✝⁵, x✝⟩
a✝² : y = M.mk ⟨a✝⁵, y✝⟩
a✝¹ : F.A
f✝ : F.B a✝¹ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝¹, f✝⟩) = iselect ps y
a✝ : M.mk ⟨a✝¹, f✝⟩ = M.mk ⟨a✝⁸, y✝¹⟩
⊢ (M.mk ⟨a✝¹, f✝⟩).approx (n + 1 + 1) = y.approx (n + 1 + 1)

Tactic:
induction y using PFunctor.M.casesOn'

Goal state after:
case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
z : F.M
a✝⁹ : F.A
x✝¹ y✝¹ : F.B a✝⁹ → F.M
a✝⁸ : ∀ (i : F.B a✝⁹), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁷ : z = M.mk ⟨a✝⁹, x✝¹⟩
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : z = M.mk ⟨a✝⁶, x✝⟩
a✝³ : F.A
f✝¹ : F.B a✝³ → F.M
a✝² : M.mk ⟨a✝³, f✝¹⟩ = M.mk ⟨a✝⁹, y✝¹⟩
a✝¹ : F.A
f✝ : F.B a✝¹ → F.M
a✝ : M.mk ⟨a✝¹, f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝³, f✝¹⟩) = iselect ps (M.mk ⟨a✝¹, f✝⟩)
⊢ (M.mk ⟨a✝³, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝¹, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

pp: case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y

Tactic:
· rw [← agree_iff_agree', i_ih]
      apply y.consistent

Goal state after:
case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
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.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balanceL x r) o₂

Tactic:
by
  rw [balanceL_eq_balance hl.2 hr.2 H₁ H₂, balance_eq_balance' hl.3 hr.3 hl.2 hr.2]
  refine hl.balance'_aux hr (Or.inl ?_) H₃
  rcases Nat.eq_zero_or_pos (size r) with r0 | r0
  · rw [r0]; exact Nat.zero_le _
  rcases Nat.eq_zero_or_pos (size l) with l0 | l0
  · rw [l0]; exact le_trans (Nat.mul_le_mul_left _ (H₁ l0)) (by decide)
  replace H₂ : _ ≤ 3 * _ := H₂ l0 r0; lia

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩

Tactic:
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
    ext1 x
    cases f x
    rfl

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 <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
Module: Mathlib.Data.PNat.Factors

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

Tactic:
change (u ⊓ v).prod = PNat.gcd n m

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = n.gcd m
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.balanceL x r = l.balance x r

Tactic:
balanceL_eq_balance sl sr

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

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
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g (abs ((P F).map (recF g) ((P F).map fixToW ⟨a, f⟩))) = g (rec g <$> x)

Tactic:
PFunctor.map_map,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g (abs ((P F).map (recF g ∘ fixToW) ⟨a, f⟩)) = g (rec g <$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
rintro ⟨x⟩ ⟨y⟩ rxy
  apply Quot.sound
  let r' x y := r (Quot.mk _ x) (Quot.mk _ y)
  have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) =
        Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) :=
      h _ _ r'ab
    have h₁ : ∀ u v : q.P.M, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      simp only [r']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁) <| by
        rintro ⟨c⟩ ⟨d⟩ rcd
        exact Quot.sound rcd
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, ← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map,
      abs_map, h₀]
    rw [← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map, abs_map]
  exact ⟨r', this, rxy⟩

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

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
exact Or.inl <| sign_of_neg hn

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

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none c

Tactic:
obtain - | c := c

Goal state after:
case none.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none none

case none.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
c : α × WSeq α
hc : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) c

Tactic:
obtain - | c := c

Goal state after:
case some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) none

case some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
c : α × WSeq α
hc : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) (some c)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.destruct.Terminates ↔ t.destruct.Terminates

Tactic:
rw [← head_terminates_iff, ← head_terminates_iff]

Goal state after:
case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.head.Terminates ↔ t.head.Terminates