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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b

Tactic:
;

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝

Tactic:
;

Goal state after:
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
;

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝
Module: Mathlib.Data.List.Sigma

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

Tactic:
;

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

Goal state before:
pp: α : 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₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
;

Goal state after:
α : 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₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)

Tactic:
;

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
a✝³ b✝ : Sigma β
a✝² : a✝³.fst ≠ b✝.fst
a✝¹ : decide (a = a✝³.fst) = true
a✝ : decide (a = b✝.fst) = true
⊢ False

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
a✝³ b✝ : Sigma β
a✝² : a✝³.fst ≠ b✝.fst
a✝¹ : decide (a = a✝³.fst) = true
a✝ : decide (a = b✝.fst) = true
⊢ False
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (⋯ ▸ b), l) else ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd)) =
    (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (⋯ ▸ b), l) else ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd)) =
    (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors = image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach)

Tactic:
rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ image ((fun p ↦ p.1 * p.2) ∘ Subtype.val) (m.divisors ×ˢ n.divisors).attach =
    image (⇑{ toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ }) (m.divisors ×ˢ n.divisors).attach

Tactic:
;

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ image ((fun p ↦ p.1 * p.2) ∘ Subtype.val) (m.divisors ×ˢ n.divisors).attach =
    image (⇑{ toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ }) (m.divisors ×ˢ n.divisors).attach
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case swap
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
s₁ s₂ : Sigma β
l✝ : List (Sigma β)
l : List (Sigma β)
⊢ (s₂ :: s₁ :: l✝).kunion l ~ (s₁ :: s₂ :: l✝).kunion l

Tactic:
simp [kerase_comm, Perm.swap]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
this : DecidableEq α
⊢ Finset α

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
this : DecidableEq α
⊢ Finset α
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum

Tactic:
;

Goal state after:
case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
inst✝¹ : Zero γ
inst✝ : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ ∀ (x : α), ¬f x • g x = 0 → ¬g x = 0

Tactic:
;

Goal state after:
α : Type u₁
β : Type u₂
γ : Type u₃
inst✝¹ : Zero γ
inst✝ : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ ∀ (x : α), ¬f x • g x = 0 → ¬g x = 0
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
a✝ : α
⊢ ((r • f) • m) a✝ = (r • f • m) a✝

Tactic:
;

Goal state after:
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
a✝ : α
⊢ ((r • f) • m) a✝ = (r • f • m) a✝
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is

Tactic:
;

Goal state after:
ds₁ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is
Module: Mathlib.Data.Holor

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

Tactic:
;

Goal state after:
α : Type
ds₁ : List ℕ
a : Holor α ds₁
⊢ cast ⋯ a = fun t ↦ a (cast ⋯ t)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)

Tactic:
;

Goal state after:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)

Tactic:
;

Goal state after:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t

Tactic:
;

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
;

Goal state after:
n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b

Tactic:
;

Goal state after:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
;

Goal state after:
b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b

Tactic:
;

Goal state after:
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m

Tactic:
;

Goal state after:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case true
n : ℤ
⊢ ofNat (1 / 2) = 0

Tactic:
rw [Nat.div_eq_of_lt] <;> simp

Goal state after:
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
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs

Tactic:
;

Goal state after:
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
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs
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 := ⋯
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ ↑(p ^ (k + 1)) ∣ ↑m.natAbs

Tactic:
;

Goal state after:
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 := ⋯
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ ↑(p ^ (k + 1)) ∣ ↑m.natAbs
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:
;

Goal state after:
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
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: 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)

Tactic:
;

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.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a ≤ x_1 ∧ x_1 < b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a ≤ x_1 ∧ x_1 < b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a ≤ ↑y ∧ ↑y < ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a ≤ ↑y ∧ ↑y < ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x

Tactic:
;

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: 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)

Tactic:
;

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.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v x : ℕ
h : (↑a ≤ ↑x ∧ ↑x < ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x

Tactic:
;

Goal state after:
case mpr
a b r v x : ℕ
h : (↑a ≤ ↑x ∧ ↑x < ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a < ↑y ∧ ↑y ≤ ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Tactic:
;

Goal state after:
case mp
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a < ↑y ∧ ↑y ≤ ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Tactic:
;

Goal state after:
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
h : (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x

Tactic:
;

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
h : (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x

Tactic:
;

Goal state after:
case mpr
a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case a
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ 0 ≤ b

Tactic:
;

Goal state after:
case a
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ 0 ≤ b
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
b : β
⊢ foldr (flip v) b [] = foldl v b []

Tactic:
simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

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

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

Tactic:
simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

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

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])

Tactic:
;

Goal state after:
case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
⊢ (sz.splitLengths l).length = sz.length

Tactic:
by
  induction sz generalizing l <;> simp [splitLengths, *]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length

Tactic:
;

Goal state after:
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w

Tactic:
;

Goal state after:
α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
;

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
;

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this : i % p < p
⊢ i % p < n + w.length

Tactic:
;

Goal state after:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this : i % p < p
⊢ i % p < n + w.length
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this✝ : i % p < p
this : p ≤ n
⊢ i % p < n + w.length

Tactic:
;

Goal state after:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this✝ : i % p < p
this : p ≤ n
⊢ i % p < n + w.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ ([].reverse ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m

Tactic:
;

Goal state after:
case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ ([].reverse ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m
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
⊢ (p - q).gcd q ≤ p - q

Tactic:
;

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
⊢ (p - q).gcd q ≤ p - q