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

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ ((fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y) =
    ((fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y)

Tactic:
congr <;> ext i ⟨x, _⟩

Goal state after:
case h₁.e_a.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α i ⟨x, property✝⟩)).1

case h₁.e_b.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α i ⟨x, property✝⟩)).2
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

Tactic:
apply h₁

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ 1 ≤ ↑prec

Tactic:
apply Int.ofNat_le_ofNat_of_le

Goal state after:
C : FloatCfg
⊢ 1 ≤ prec
Module: Mathlib.Data.Finmap

Goal state before:
pp: case refine_2.mk
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
x✝ : Multiset (Sigma β)
l : List (Sigma β)
⊢ Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l) →
    (Quotient.liftOn (Quot.mk (⇑(isSetoid (Sigma β))) l)
        (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } }) ⋯).Dom

Tactic:
exact id

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (s.keys.sigma fun i ↦ (lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }

Tactic:
ext x
  have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _
  simpa [lookup_eq_some_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all) <;> simp

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → ¬a ∈ (kerase a tl).keys
nd : (hd :: tl).NodupKeys
⊢ ¬a ∈ (kerase a (hd :: tl)).keys

Tactic:
simp only [nodupKeys_cons] at nd
    by_cases h : a = hd.1
    · subst h
      simp [nd.1]
    · simp [h, ih nd.2]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ sizeOf xs.dedupKeys ≤ sizeOf xs

Tactic:
by
  induction xs with
  | nil => simp [dedupKeys]
  | cons x xs h =>
    simp only [dedupKeys_cons, kinsert_def, Sigma.eta]
    exact sizeOf_cons_le_sizeOf_cons x (le_trans (sizeOf_kerase x.fst xs.dedupKeys) h)

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup

Tactic:
convert! List.support_sum_eq a this

Goal state after:
case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup = List.foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ a
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext
  simpa only [mem_neLocus] using! hF.ne_iff

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
intro _ _ h_not_in ih

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : fib (↑n✝ + 1) * fib (↑n✝ - 1) - fib ↑n✝ ^ 2 = (-1) ^ n✝
⊢ fib (↑(n✝ + 1) + 1) * fib (↑(n✝ + 1) - 1) - fib ↑(n✝ + 1) ^ 2 = (-1) ^ (n✝ + 1)

Tactic:
| succ _ _ =>

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

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n

Tactic:
exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n)
    (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

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

Goal state before:
pp: case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
intro ⟨rfl, hz, hb⟩
    constructor
    · rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
      simp
    · rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b ↑n).lnot = bit (!b) (↑n).lnot

Tactic:
by simp [lnot]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b -[n+1]).lnot = bit (!b) -[n+1].lnot

Tactic:
by simp [lnot]

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

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

Tactic:
simp [Ioc_filter_modEq_eq, Ioc_filter_dvd_eq, hr]

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

Goal state before:
pp: a b r v : ℕ
⊢ map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}) = {x ∈ Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

Tactic:
ext x
  simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]
  constructor
  · simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
  · intro h; lift x to ℕ using (by lia); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tail✝ = ofFn fun i ↦ f (↑i) (tail✝.get i)
f : ℕ → α → β
⊢ mapIdx f (head✝ :: tail✝) = ofFn fun i ↦ f (↑i) ((head✝ :: tail✝).get i)

Tactic:
simp [IH]

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

Goal state before:
pp: case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
· rw [max_eq_left hln, filter_le_of_le_bot hln]

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

Goal state before:
pp: case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

pp: case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections

Tactic:
· induction L generalizing f
    · cases mem_singleton.1 h
      exact Forall₂.nil
    simp only [sections, mem_flatMap, mem_map] at h
    rcases h with ⟨_, _, _, _, rfl⟩
    simp only [*, forall₂_cons, true_and]

Goal state after:
case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case zero
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

pp: case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l

Tactic:
case zero => simp

Goal state after:
case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ (splitBy.loop r l b (a :: g) []).flatten = g.reverse ++ a :: b :: l

Tactic:
simp [IH]

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

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten = g.reverse ++ a :: b :: l

Tactic:
simp [IH]

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ w[i % p]? = w[i]?

Tactic:
have minus : i - p < w.length - p := by lia

Goal state after:
case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₁
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inl val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inl val✝) j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₂
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inr val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inr val✝) j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₁
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inl val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inl val✝)

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₂
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inr val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inr val✝)

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i✝ : m
j✝ : n
⊢ (A₁.fromCols A₂ * B₁.fromRows B₂) i✝ j✝ = (A₁ * B₁ + A₂ * B₂) i✝ j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inl val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inl val✝)

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inr val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inr val✝)

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₁
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val✝) j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₂
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val✝) j✝

Tactic:
simp [mul_apply]

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p ∧ p ∣ a ∧ ¬a = 0

Tactic:
simpa using support_ceilDiv_subset hp

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ f n ≤ nth p n

Tactic:
by
  induction n with
  | zero =>
    rw [Nat.nth_zero]
    refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
    rcases hsurj hb with ⟨k, hk, rfl⟩
    exact hmono hn hk (Nat.zero_le _)
  | succ n ih =>
    rw [nth_eq_sInf]
    refine le_csInf ?_ ?_
    · use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn
    rintro b ⟨hb, h⟩
    rcases hsurj hb with ⟨m, hm, rfl⟩
    apply hmono hn hm
    rw [Nat.succ_le_iff]
    apply hmono.reflect_lt <;> grind

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1

Tactic:
have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
by rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]

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

Goal state before:
pp: case mpr.intro
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
w✝ : P.B a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Tactic:
subst x

Goal state after:
case mpr.intro
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
w✝ : P.B a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w✝)
Module: Mathlib.Data.Num.ZNum

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

Tactic:
by
    intro a b
    transfer_rw
    apply le_antisymm

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

Goal state before:
pp: l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1

Tactic:
exact id

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

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

Tactic:
subst x

Goal state after:
case mpr.intro
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
w✝ : P.B a i
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i (f i w✝)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) nil o₂
H1 : ¬l.size + nil.size ≤ 1
H2 : delta * l.size < nil.size
H3 : 2 * nil.size ≤ 9 * l.size + 5 ∨ nil.size ≤ 3
⊢ Valid' o₁ (l.rotateL x nil) o₂

pp: case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size < (Ordnode.node rs rl rx rr).size
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
· cases H2

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size < (Ordnode.node rs rl rx rr).size
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : ZNum
⊢ (↑a.abs).gcd ↑b.abs = (↑a).gcd ↑b

Tactic:
simp only [abs_to_nat]; rfl

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node4L x m y r).Sized

Tactic:
cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]

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

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ (l.node4L x nil y r).size = l.size + nil.size + r.size + 2

Tactic:
simp [node4L, node3L, node']

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ l.size + 1 + r.size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
exact hr.rotateL_size

Goal state after:
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' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance x r) o₂

Tactic:
rw [balance_eq_balance' hl.3 hr.3 hl.2 hr.2]; exact hl.balance' hr H

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
x : α
⊢ (M.corec g x).dest = P.map (M.corec g) (g x)

Tactic:
corec_def,

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
x : α
⊢ (M.mk (P.map (M.corec g) (g x))).dest = P.map (M.corec g) (g x)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| (g ::: fun x ↦ g <$$> x) <$$> dest' P ⋯ ⟨a, f⟩.snd

Tactic:
M.dest',

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| (g ::: fun x ↦ g <$$> x) <$$>
    ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
      splitFun (pathDestLeft P ⋯ ⟨a, f⟩.snd) fun x ↦
        ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: p : ℕ+
l : List ℕ
hl : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ p ∈ (ofNatList l hl).toPNatMultiset ↔ ↑p ∈ l

Tactic:
simp [ofNatList]

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

Goal state before:
pp: l : List ℕ+
hl : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatList l hl).toPNatMultiset = ↑l

Tactic:
simp [ofPNatList]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩

Tactic:
rw [wDest', wRec_eq]

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

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
rw [← factorMultiset_le_iff']

Goal state after:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hn
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
rw [← factorMultiset_le_iff']

Goal state after:
case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset