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

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt32.ofFin UInt32.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : UInt32
⊢ UInt32.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt32.ofFin UInt32.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (UInt32.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt64.ofFin UInt64.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : UInt64
⊢ UInt64.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt64.ofFin UInt64.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (UInt64.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Int8
⊢ (Int8.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int8.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (BitVec.toFin ∘ Int8.toBitVec) ((Int8.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Int16
⊢ (Int16.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int16.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (BitVec.toFin ∘ Int16.toBitVec) ((Int16.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Int32
⊢ (Int32.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int32.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (BitVec.toFin ∘ Int32.toBitVec) ((Int32.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Int64
⊢ (Int64.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int64.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (BitVec.toFin ∘ Int64.toBitVec) ((Int64.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ LeftInverse BitVec.ofFin BitVec.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
n : ℕ
x : BitVec n
⊢ { toFin := x.toFin } = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ RightInverse BitVec.ofFin BitVec.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
n : ℕ
x : Fin (2 ^ n)
⊢ { toFin := x }.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
⊢ ∀ (x : (hp : p) → α hp), x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))

Tactic:
intro x

Goal state after:
α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Vector α n)

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Vector α n)
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Sym α n)

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Sym α n)
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Perm α) = (Nat.card α)!
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs = ys)

Tactic:
rw [AList.ext_iff]; infer_instance

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (kextract a s.entries).snd.NodupKeys

Tactic:
by
    rw [kextract_eq_dlookup_kerase]; exact s.nodupKeys.kerase _

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
⊢ ∀ (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ erase a ⟦s⟧ = ⟦AList.erase a s⟧

Tactic:
by
  simp [erase]

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case neg
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
have : IsIso π' := ⟨ConcreteCategory.ofHom ⟨(h.elim ·), continuous_of_const <| by aesop⟩,
      by ext x; exact h.elim (π' x), by ext x; all_goals exact h.elim x⟩

Goal state after:
case neg
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
this : IsIso π'
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ ∀ (x : α), lookup x s₁ = lookup x s₂

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some ⟨a, b⟩ else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some ⟨a, b⟩ else none) → a_1 = b_1 ∧ c = d

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x : Sigma β
⊢ ∀ {b_1 : Sigma β},
    x.fst ≠ b_1.fst →
      ∀ (c : Sigma β),
        (c ∈ if a = x.fst then some ⟨a, b⟩ else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some ⟨a, b⟩ else none) → x = b_1 ∧ c = d
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
· subst e
      exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup a (kerase a' l) = dlookup a l

Tactic:
by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    obtain ⟨ah, bh⟩ := hd
    by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah
    · subst h₁ h₂
      cases Ne.irrefl h
    · subst h₁
      simp [h₂]
    · subst h₂
      simp [h]
    · simp [h₁, h₂, ih]

Goal state after:
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
⊢ (some (⋯ ▸ b), l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
· subst a'
      simp [kerase]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inl
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ p f

Tactic:
convert! h0 using 1
    simpa [funext_iff] using he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
h₁ : s = t
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f s = pimage g t

Tactic:
by
  aesop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ⟨i, x⟩ ∉ univ.sigma g

Tactic:
simp [hx']

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₁.support

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₂.support

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
        (∀ x ∈ insert a s, CPRankMax n (f x)) → CPRankMax ((insert a s).card * n) (∑ x ∈ insert a s, f x)

Tactic:
intro x

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
⊢ ∀ (s : Finset β),
    x ∉ s →
      ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
        (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Tactic:
rw [sq, sq]

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Tactic:
rw [sq, sq]

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Tactic:
rw [sq, sq]

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd2 : p ^ (l + 1) ∣ n.natAbs
⊢ ↑(p ^ (l + 1)) ∣ ↑n.natAbs

Tactic:
apply Int.natCast_dvd_natCast.2 hsd2

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

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ (fun x ↦ x ^^^ a) = id ↔ a = 0

Tactic:
rw [xor_right_eq, xor_left_eq_id_iff]

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

Goal state before:
pp: case ofNat.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 false true <;> simp [h]

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

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

Tactic:
by
  ext x
  simp only [mem_map, mem_filter, mem_Ico, 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 omega); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
a : α
b : β
⊢ foldl v (v b a) [] = v (foldl v b []) a

Tactic:
simp [*, hv.right_comm]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, foldl v (v b a) tail✝ = v (foldl v b tail✝) a
a : α
b : β
⊢ foldl v (v b a) (head✝ :: tail✝) = v (foldl v b (head✝ :: tail✝)) a

Tactic:
simp [*, hv.right_comm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []

Tactic:
cases l

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → β → γ
⊢ zipWith f [] [] = []

case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : β
tail✝ : List β
⊢ zipWith f [] (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []

Tactic:
cases l

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → β → γ
⊢ zipWith f [] [] = []

case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) [] = []
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
← append_consecutive (Nat.le_succ n) h,

Goal state after:
n m : ℕ
h : n < m
⊢ Ico n n.succ ++ Ico n.succ m = n :: Ico (n + 1) m
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
⊢ modifyLast f ([] ++ [a]) = [] ++ [f a]

Tactic:
simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome

Tactic:
intro x

Goal state after:
α : Type u_1
l : List α
x : α
⊢ ∀ (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (x :: (l ++ [b])).reverse = x :: (l ++ [b]) → (x :: (l ++ [b])).Palindrome
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Goal state after:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Goal state after:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q w = take q (drop q w ++ z)

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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q (drop q w ++ z)

Tactic:
· rw [hz]

Goal state after:
α : 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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q (drop q w ++ z)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.gt
α : 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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w.HasPeriod (p.gcd q)

Tactic:
convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)

Goal state after:
α : 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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w = take q (drop q w) ++ drop q w

case inr.inr.gt
α : 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
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp s) (toDFinsupp t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)

Tactic:
Finset.card_map,

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

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

Tactic:
Finset.card_map,

Goal state after:
α : 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)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
| ∑ i ∈ range (n % p + 1), ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))

Tactic:
2,

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
| fun i ↦ ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k : ℕ
| ∑ j ∈ range (n / p + 1), X ^ k * ↑((n % p).choose k) * (X ^ (p * j) * ↑((n / p).choose j))

Tactic:
2,

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k : ℕ
| fun j ↦ X ^ k * ↑((n % p).choose k) * (X ^ (p * j) * ↑((n / p).choose j))