mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π' ≫ (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f =
    (lightProfiniteToLightCondSet ⋙ free R).map π' ≫
      hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr) ≫ p

Tactic:
← Functor.comp_map,

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π' ≫ (lightProfiniteToLightCondSet ⋙ free R).map (y' ▷ ℕ∪{∞}) ≫ f =
    (lightProfiniteToLightCondSet ⋙ free R).map π' ≫
      hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr) ≫ p
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : AList β
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂ ∪ s₃).entries ↔ y ∈ dlookup x (s₁ ∪ (s₂ ∪ s₃)).entries

Tactic:
by simp [not_or, or_assoc, and_or_left, and_assoc]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val.NodupKeys

Tactic:
refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ∀ x ∈ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val,
    ∀ y ∈ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, x.fst = y.fst → x = y
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
· subst h
      simp only [lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons_cons _

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
rw [kunion_cons]

Goal state after:
case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast ⋯ a = fun t ↦ a (cast ⋯ t)

Tactic:
by
  subst eq; rfl

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

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

Tactic:
by
    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero, Bool.not_not]

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

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

pp: case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false 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 false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

pp: case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false 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 false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

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 false false <;> simp +decide [h]

Goal state after:
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false 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 false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false 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 false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

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))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ ↑m <<< ↑n = ↑(m <<< n)

Tactic:
unfold_projs

Goal state after:
m n : ℕ
⊢ (match ↑m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    ↑(m.shiftLeft n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m <<< ↑n = m * ↑(2 ^ n)

Tactic:
unfold_projs

Goal state after:
m : ℤ
n : ℕ
⊢ (match m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    m.mul ↑(Nat.pow 2 n)
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
inst✝ : LeftCommutative f
⊢ foldl (flip f) b l = foldr f b l

Tactic:
induction l generalizing b <;> simp [*, flip, foldr_cons_eq_foldr_apply, -foldr_cons]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rtakeWhile p [] = []

Tactic:
by simp [rtakeWhile]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
⊢ map₂Right f as bs = (map₂Right' f as bs).fst

Tactic:
by
  simp only [map₂Right, map₂Right', map₂Left_eq_map₂Left']

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : n ∈ {n | n ≤ l.length}
m : ℕ
⊢ m ∈ {n | n ≤ l.length} → (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) m → n = m

Tactic:
hm

Goal state after:
α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : n ∈ {n | n ≤ l.length}
m : ℕ
hm : m ∈ {n | n ≤ l.length}
⊢ (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) m → n = m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ (v ++ w)[j]? = v[j]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
getElem?_append_left

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ v[j]? = v[j]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ (v ++ w)[j + u.length + p - u.length]? = v[j + p]?

Tactic:
getElem?_append_left

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ v[j + u.length + p - u.length]? = v[j + p]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ j + u.length + p - u.length < v.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m

Tactic:
rw [splitBy_eq_iff]

Goal state after:
case inr.inr
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten ∧
    ¬[] ∈ splitBy r l ++ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1) ∧
        IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(uIcc (toDFinsupp s) (toDFinsupp t)) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)

Tactic:
DFinsupp.card_uIcc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∏ i ∈ (toDFinsupp s).support ∪ (toDFinsupp t).support, #(uIcc ((toDFinsupp s) i) ((toDFinsupp t) i)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
⊢ ∃ M', N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
by
  classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iic n.factorization).attach

Tactic:
rw [Finset.map_eq_image]
  change _ = (Finset.Iic n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)
  rw [← Finset.image_image, Finset.attach_image_val]
  exact divisors_eq_image_Iic_factorization_prod_pow hn

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

Goal state before:
pp: case mpr
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)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
← h.left,

Goal state after:
case mpr
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)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (k % p, x₂).1 + p * (k % p, x₂).2
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n

Tactic:
hm

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ p ^ multiplicity p n * m
Module: Mathlib.Data.Num.ZNum

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

Tactic:
change Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)

Goal state after:
n : ℕ
⊢ (↑(n + 1)).toZNumNeg = -↑(n + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d

Tactic:
rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
          abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
      rfl

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

Goal state before:
pp: case mpr.succ.step.f.f
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)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))

Tactic:
simp only [approx_mk]

Goal state after:
case mpr.succ.step.f.f
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)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro x_a fun j ↦ (x_f j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : ↑F F.M
i : F.Idx
⊢ (if H' : i.fst = (M.mk x).head then (M.mk x).children (cast ⋯ i.snd) else default) =
    if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default

Tactic:
congr with h

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

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
h₂ : M.mk ⟨a✝¹, f✝¹⟩ = M.mk ⟨a, f₂⟩
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 (M.mk ⟨a✝, f✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝, f✝⟩).approx (n + 1 + 1)

Tactic:
simp only [approx_mk]

Goal state after:
case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
h₂ : M.mk ⟨a✝¹, f✝¹⟩ = M.mk ⟨a, f₂⟩
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 (M.mk ⟨a✝, f✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
⊢ (CofixA.intro a✝¹ fun j ↦ (f✝¹ j).approx (n + 1)) = CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
· simp [node4L, node', size, hm.1]; abel

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:
exact hl.balance' hr H

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

Goal state before:
pp: n : ℕ+
⊢ ↑n.factorMultiset.prod = ↑n

Tactic:
dsimp [factorMultiset]
    rw [PrimeMultiset.prod_ofNatList]
    exact Nat.prod_primeFactorsList n.ne_zero

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

Goal state before:
pp: p n : ℕ+
⊢ p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n

Tactic:
by
  simp [factorMultiset, dvd_iff, PNat.Prime]

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

Goal state before:
pp: a b : ℕ+
⊢ (start a b).IsSpecial

Tactic:
by
  dsimp [start, IsSpecial]

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

Goal state before:
pp: case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : ((↑w + x) * ↑d, (y + ↑z) * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
← ha',

Goal state after:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, (y + ↑z) * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk.mk
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 a✝ : (P F).M α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr a✝) → Quot.mk Mcongr x = Quot.mk Mcongr a✝

Tactic:
rename M (P F) α => y

Goal state after:
case mk.mk
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 α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr y) → Quot.mk Mcongr x = Quot.mk Mcongr y
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ closure (range fun x ↦ x ^ n) = nonneg ℚ

Tactic:
convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm
  · have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩
    simp [subset_antisymm_iff, range_subset_iff, this]
  · ext
    simp [NNRat.addSubmonoid_closure_range_pow hn₀, NNRat.exists]

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none

Tactic:
by simp [h, enumerate]

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none

Tactic:
by simp [h, enumerate]

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

Goal state before:
pp: case some
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val✝ : α
hs : sel s = some val✝
⊢ enumerate sel s m = none

Tactic:
· cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm

Goal state after: