mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j

Tactic:
;

Goal state after:
case neg.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ removeNth 0 f x✝ = tail f x✝

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ removeNth 0 f x✝ = tail f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝

Tactic:
;

Goal state after:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l

Tactic:
cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_cons_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩

Tactic:
;

Goal state after:
case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i

Tactic:
;

Goal state after:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = fun i_1 ↦
      (fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = fun i_1 ↦
      (fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

pp: case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
;

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ motive s hs

Tactic:
refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
    (fun _ => empty) ?_ .rfl
  intro a s has _ hCs haS
  rw [insert_subset_iff] at haS
  exact insert haS.1 haS.2 has (hCs haS.2)

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

Goal state before:
pp: case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
;

Goal state after:
case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x ↦ α) (last n)) x✝¹ x✝ = (snocEquiv fun x ↦ α) x✝¹ x✝

Tactic:
;

Goal state after:
n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x ↦ α) (last n)) x✝¹ x✝ = (snocEquiv fun x ↦ α) x✝¹ x✝
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)

Tactic:
;

Goal state after:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
rw [← card_fintypeInsertOfNotMem s h]; congr!

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ a ∈ s, a ∈ t
⊢ False

Tactic:
;

Goal state after:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ a ∈ s, a ∈ t
⊢ False
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Tactic:
;

Goal state after:
α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
;

Goal state after:
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z

Tactic:
exact max_lt_iff

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

Goal state before:
pp: case refl
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a

Tactic:
;

Goal state after:
case refl
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ [a, b]

Tactic:
;

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ [a, b]
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l

Tactic:
(apply hab.subset; simp)

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

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Tactic:
;

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
(apply hab.subset; simp)

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

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
(apply hab.subset; simp)

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case inl
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

pp: case inr
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ R (l.get a) (l.get b)

Tactic:
;

Goal state after:
case inl
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

case inr
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ R (l.get a) (l.get b)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case rel
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

pp: case cons
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

Tactic:
;

Goal state after:
case rel
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

case cons
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a c : α
l₁ l₂ : List α
⊢ IsChain R (a :: l₁ ++ c :: l₂) ↔ IsChain R (a :: l₁ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
isChain_split (l₂ := l₂)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : M
⊢ (a ::ₘ {b}).prod = a * b

Tactic:
prod_cons,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : M
⊢ a * {b}.prod = a * b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length

Tactic:
;

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
by rw [List.rotate', length_rotate' (l ++ [a]) n]; simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
prod_cons,

Goal state after:
case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m * L.prod)
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + (0 + 1)

Tactic:
;

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + (0 + 1)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Tactic:
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l

Tactic:
;

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l

Tactic:
;

Goal state after:
α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ (c :: d :: l).getLast ⋯ = b

Tactic:
rwa [getLast_cons_cons]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
l : List α
h✝ : IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
;

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
l : List α
h✝ : IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l

Tactic:
;

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (range l.sum)

Tactic:
;

Goal state after:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (range l.sum)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ s.prod * (a :: t).prod

Tactic:
prod_cons,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ s.prod * (a * t.prod)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hl⟩ → Acc (List.lex_chains r) y

Tactic:
;

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hl⟩ → Acc (List.lex_chains r) y
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⋯
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y

Tactic:
;

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⋯
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro.intro.nil.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
hm : List.IsChain (flip r) []
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hm⟩ → Acc (List.lex_chains r) y

Tactic:
;

Goal state after:
case cons.intro.intro.nil.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
hm : List.IsChain (flip r) []
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hm⟩ → Acc (List.lex_chains r) y
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ (0 • m).prod = m.prod ^ 0

Tactic:
rw [zero_nsmul, pow_zero]
    rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
a✝ : List M
h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a✝⟧ → a' = 1
⊢ prod ⟦a✝⟧ = a ^ count a ⟦a✝⟧

Tactic:
;

Goal state after:
case h
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
a✝ : List M
h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a✝⟧ → a' = 1
⊢ prod ⟦a✝⟧ = a ^ count a ⟦a✝⟧
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h
M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : List M
h : ∀ (x : M), x ∈ ⟦a✝⟧ → x = 1
⊢ prod ⟦a✝⟧ = 1

Tactic:
;

Goal state after:
case h
M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : List M
h : ∀ (x : M), x ∈ ⟦a✝⟧ → x = 1
⊢ prod ⟦a✝⟧ = 1
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
a✝ : List M
hs : Quot.mk (⇑(List.isSetoid M)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid M)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid M)) a✝))

Tactic:
;

Goal state after:
case h
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
a✝ : List M
hs : Quot.mk (⇑(List.isSetoid M)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid M)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid M)) a✝))
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False