mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))

Tactic:
by_cases h : f true true <;> simp +decide [h]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
by
  rw [← bitwise_diff, bitwise_bit]

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

Goal state before:
pp: case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

Tactic:
by_cases h : f true true

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
v : ℤ
⊢ ↑(#({x ∈ Ico a b | x ≡ v [ZMOD r]})) = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

Tactic:
by
  simp [Ico_filter_modEq_eq, Ico_filter_dvd_eq, hr]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(#({x ∈ Ico 0 b | x ≡ v [MOD r]})) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
Ico_filter_modEq_card _ _ hr,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉) 0 = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ (↑1 - 1) * ↑r < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ ↑1 * ↑r

Tactic:
Int.cast_one,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ (1 - 1) * ↑r < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ 1 * ↑r
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑1

pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0

Tactic:
· rw [← cast_sub h.le, Int.ceil_eq_iff, div_le_iff₀ hr', lt_div_iff₀ hr', cast_one, Int.cast_one,
      sub_self, zero_mul, cast_pos, tsub_pos_iff_lt, one_mul, cast_le, tsub_le_iff_right]
    exact ⟨h, ((mod_lt _ hr).trans_le (by simp)).le⟩

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? (fun x ↦ !p x) l = (dropWhile p l).head?

Tactic:
convert! l.find?_eq_head?_dropWhile_not ?_
  simp

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
by
  match l, h with
  | a::l, h => apply isChain_of_mem_splitByLoop _ _ h <;> simp

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r (head✝ :: tail✝))

Tactic:
apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ ∀ (m : List α), m ∈ [].head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [head✝]).head hb) = false
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ ∀ (y : α), y ∈ Y → y < z

Tactic:
simpa using hYZ

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

Goal state before:
pp: n : ℕ
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

case neg
n : ℕ
hn : ¬n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k ≠ n

Tactic:
suffices k.factorization = f from (this ▸ hlt.ne <| congrArg _ ·)

Goal state after:
case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k.factorization = f
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:
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.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n ≤ f n

Tactic:
· rcases hn with ⟨hf, hn⟩
    rw [nth, dif_pos hf, List.getD_eq_default _ _ (by simp [hn])]
    exact Nat.zero_le _

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

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

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

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

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 node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

Goal state after:
case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

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

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

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

case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑n.pred' + 1

Tactic:
← Num.succ'_to_nat,

Goal state after:
n : PosNum
⊢ ↑n = ↑n.pred'.succ'
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ofInt' -[n+1] = ↑-[n+1]

Tactic:
change Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)
    rw [← neg_inj, neg_neg, Nat.cast_succ, Num.add_one, Num.zneg_toZNumNeg, Num.toZNum_succ,
      Nat.cast_succ, ZNum.add_one]
    rfl

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

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
⊢ ↑(d.divModAux q r).2 + ↑d * ↑(d.divModAux q r).1 = ↑n ∧ ↑(d.divModAux q r).2 < ↑d

Tactic:
unfold divModAux
  have : ∀ {r₂}, Num.ofZNum' (Num.sub' r (Num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d := by
    intro r₂
    apply Num.mem_ofZNum'.trans
    rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
    simp
  rcases e : Num.ofZNum' (Num.sub' r (Num.pos d)) with - | r₂
  · rw [Num.cast_bit0, two_mul]
    refine ⟨h₁, lt_of_not_ge fun h => ?_⟩
    obtain ⟨r₂, e'⟩ := Nat.le.dest h
    rw [← Num.to_of_nat r₂, add_comm] at e'
    cases e.symm.trans (this.2 e'.symm)
  · have := this.1 e
    simp only [Num.cast_bit1]
    constructor
    · rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
    · rwa [this, two_mul, add_lt_add_iff_right] at h₂

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

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

Tactic:
intro IH

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

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

Tactic:
intro IH

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

Goal state before:
pp: case pos
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_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ((M.mk ⟨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 only [dif_pos, casesOn_mk']

Goal state after:
case pos
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_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ (isubtree ps_tail (x_f (cast ⋯ i))).head = default.head
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : PrimeMultiset
⊢ v.prod.factorMultiset = v

Tactic:
by
  apply PrimeMultiset.coeNat_injective
  rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
  rcases v with ⟨l⟩
  dsimp [PrimeMultiset.toNatMultiset]
  let l' := l.map ((↑) : Nat.Primes → ℕ)
  have (p : ℕ) (hp : p ∈ l') : p.Prime := by
    simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp
    obtain ⟨hp', -⟩ := hp
    exact hp'
  exact Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
simp only [← lt_add_one_iff, find_lt_iff]

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

Goal state before:
pp: case pos
α : 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
⊢ Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
    ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs

Tactic:
splitMax_eq

Goal state after:
case pos
α : 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
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs

case pos.s
α : 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
⊢ ℕ
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.right
m n : ℕ+
⊢ n ∣ m.lcm n

Tactic:
exact dvd_lcm_right m n

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

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

Tactic:
obtain ⟨H1, H2⟩ := raised_iff.1 H; rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

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

Goal state before:
pp: a b : ℕ+
⊢ a.gcdD b = a.gcd b

Tactic:
by
  rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
  apply dvd_antisymm
  · apply dvd_gcd
    · exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
    · exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm
  · have h₇ : (gcd a b : ℕ) ∣ gcdZ a b * a := (Nat.gcd_dvd_left a b).trans (dvd_mul_left _ _)
    have h₈ : (gcd a b : ℕ) ∣ gcdX a b * b := (Nat.gcd_dvd_right a b).trans (dvd_mul_left _ _)
    rw [h₅] at h₇
    rw [dvd_iff]
    exact (Nat.dvd_add_iff_right h₈).mpr h₇

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' x))

Tactic:
induction x using q.P.wCases

Goal state after:
case ih
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a✝ : (P F).A
f'✝ : (P F).drop.B a✝ ⟹ α
f✝ : (P F).last.B a✝ → (P F).W α
⊢ recF g ((P F).wMk a✝ f'✝ f✝) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a✝ f'✝ f✝)))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' x))

Tactic:
by
  induction x using q.P.wCases
  case ih a f' f =>
    rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
x y : (P F).W α
⊢ WEquiv x y → recF u x = recF u y

Tactic:
induction x using q.P.wCases

Goal state after:
case ih
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
y : (P F).W α
a✝ : (P F).A
f'✝ : (P F).drop.B a✝ ⟹ α
f✝ : (P F).last.B a✝ → (P F).W α
⊢ WEquiv ((P F).wMk a✝ f'✝ f✝) y → recF u ((P F).wMk a✝ f'✝ f✝) = recF u y
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
⊢ abs ((P F).wDest' x) = abs ((P F).wDest' y) → WEquiv x y

Tactic:
induction x using q.P.wCases

Goal state after:
case ih
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
y : (P F).W α
a✝ : (P F).A
f'✝ : (P F).drop.B a✝ ⟹ α
f✝ : (P F).last.B a✝ → (P F).W α
⊢ abs ((P F).wDest' ((P F).wMk a✝ f'✝ f✝)) = abs ((P F).wDest' y) → WEquiv ((P F).wMk a✝ f'✝ f✝) y
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map,
      h₀]

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

Goal state before:
pp: case abs
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ recF u (WType.mk a f) = recF u (WType.mk a' f')

Tactic:
simp only [recF_eq', abs_map, h]

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

Goal state before:
pp: case abs
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ recF u (WType.mk a f) = recF u (WType.mk a' f')

Tactic:
| abs a f a' f' h =>

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

Goal state before:
pp: case abs
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h : QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩
⊢ Wequiv (WType.mk a' f') (WType.mk a f)

Tactic:
| abs a f a' f' h =>

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))

Tactic:
· ext
    simp [NNRat.addSubmonoid_closure_range_pow hn₀, NNRat.exists]

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ ∀ (n : ℕ), Finite ↑∅

Tactic:
simp [Finite.to_subtype]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
⊢ F l (Sum.inl val✝) →
    F (c :: l)
      (match Sum.inl val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
intro IH

Goal state after:
case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
IH : F l (Sum.inl val✝)
⊢ F (c :: l)
    (match Sum.inl val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
⊢ F l (Sum.inr val✝) →
    F (c :: l)
      (match Sum.inr val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
intro IH

Goal state after:
case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l)
    (match Sum.inr val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)