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

Goal state before:
pp: case cons.succ.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
· simp [Ne.symm hx.left] at h

Goal state after:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [] ∨ m ∈ [(a :: g).reverse]
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
mem_singleton

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [] ∨ m = (a :: g).reverse
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ [g.reverse ++ [a]] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
mem_singleton

Goal state after:
case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
· rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
      obtain rfl | hm := h
      · apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩
      · grind

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

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

Tactic:
exact this.lt_of_le (gcd_le_left q p_pos)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    snd ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

Tactic:
simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
      simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]
      rw [← Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, cast_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
  exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

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

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

Tactic:
by simp [hN, add_comm (_ + _)]

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: q : ℚ≥0
⊢ (↑q).num / ↑(↑q).den = ↑q.num / ↑q.den

Tactic:
den_coe,

Goal state after:
q : ℚ≥0
⊢ (↑q).num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
convert! Rat.den_mul_den_eq_den_mul_gcd q₁ q₂
  norm_cast

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
⊢ dig.alternatingSum = 0

Tactic:
have := dig.alternatingSum_reverse

Goal state after:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
this : dig.reverse.alternatingSum = (-1) ^ (dig.length + 1) • dig.alternatingSum
⊢ dig.alternatingSum = 0
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
hdvd : k ∣ n
hk : k ≠ 0
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
exact ⟨_, factorization_le_iff_dvd hk hn |>.mpr hdvd, prod_factorization_pow_eq_self hk⟩

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

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
· have hdvd := dvd_of_mem_divisors h
    have hk := ne_zero_of_dvd_ne_zero hn hdvd
    exact ⟨_, factorization_le_iff_dvd hk hn |>.mpr hdvd, prod_factorization_pow_eq_self hk⟩

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬((k % p, k / p).1 ∈ range (n % p + 1) ∧ (k % p, k / p).2 ∈ range (n / p + 1))
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
mem_range,

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬((k % p, k / p).1 < n % p + 1 ∧ (k % p, k / p).2 ∈ range (n / p + 1))
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬((k % p, k / p).1 < n % p + 1 ∧ (k % p, k / p).2 ∈ range (n / p + 1))
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
mem_range,

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬((k % p, k / p).1 < n % p + 1 ∧ (k % p, k / p).2 < n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
· exact n.lt_fib_greatestFib_add_one

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: α : Type u_1
b : BinaryTree α
⊢ b.toOrdNode.size = b.numNodes

Tactic:
by
  induction b with simp [BinaryTree.toOrdNode, *]

Goal state after:
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⟩
    · exact node (rs + 1) nil x r
    · refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
      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 (rs + lrs + 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: case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

Tactic:
exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩

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 α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ x = ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
rw [← hy, h, map_eq_map, PFunctor.map_eq]

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ⟨a, Subtype.val ∘ f⟩ = ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.Num.ZNum

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

Tactic:
rw [ZNum.bit1, cast_neg, cast_neg]
    rcases e : pred' p with - | a <;>
      have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
    · conv at ep => change p = 1
      subst p
      simp
    · dsimp only [Num.succ'] at ep
      subst p
      have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (-↑a : ℤ) 1]
      simpa using this

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

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : P.B ?mpr.w), p (f_1 i)

case mpr.w
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ P.A
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : P.B ?mpr.w), p (f_1 i)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)

case mpr.h.w
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ P.B ?mpr.w → α
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h.h.left
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h.h.left
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
first | constructor | assumption

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

Goal state before:
pp: case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
first | constructor | assumption

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

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x → ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) → LiftP p x

Tactic:
· rintro ⟨y, hy⟩
    rcases h : y with ⟨a, f⟩
    refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
    rw [← hy, h, map_eq]
    rfl

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) → LiftP p x
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (f_1 i j)

case mpr.w
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ P.A
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (f_1 i j)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)

case mpr.h.w
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ P.B ?mpr.w ⟹ α
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)

Tactic:
first | constructor | assumption

Goal state after:
case mpr.h.h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
first | constructor | assumption

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

Goal state before:
pp: case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
first | constructor | assumption

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

Goal state before:
pp: case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
have := this.1 e

Goal state after:
case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg.inr.refine_6
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ mr.size + r.size + 1 ≤ delta * (l.size + ml.size + 1)

Tactic:
· exact Valid'.node4L_lemma₅ lr₂ mr₁ mm₂

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

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

Tactic:
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]

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

Goal state before:
pp: m : ℕ+
p : Nat.Primes
k : ℕ
⊢ ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset

Tactic:
Multiset.le_count_iff_replicate_le,

Goal state after:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ ↑p ^ k ∣ m ↔ Multiset.replicate k p ≤ m.factorMultiset
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : 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
⊢ (∃ 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'

Tactic:
refine Or.inr ⟨_, Or.inr e, ?_⟩

Goal state after:
case neg
α : 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
⊢ BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ u.step.v.2 = u.v.swap.2

Tactic:
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
    rw [← ha, hr]
    ring

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

Goal state before:
pp: case mpr.inl
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: case inl
k m : ℕ
⊢ Raised (k + m) (k + m)

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: case neg
α : 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
⊢ 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:
have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1

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