mathlib-initiative/mathlib-tactics huggingface dataset:
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) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Tactic:
]

Goal state after:
α : 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) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯
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
⊢ op a (fold op b (s.erase a)) = op a (fold op b (s.erase a))

Tactic:
]

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (range fun x ↦ u ↑x)

Tactic:
]

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (range fun x ↦ u ↑x)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map g s.val) = Multiset.fold op b (Multiset.map g s.val)

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op b c = op b c

Tactic:
]

Goal state after:
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
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card α - 1 = Fintype.card α - 1

Tactic:
]

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

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ Infinite α

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ j.succAbove (i.succAbove k) = j.succAbove (i.succAbove k)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ InjOn f s

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ InjOn f s
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGE ↔ Antitone f

Tactic:
by
  simp only [sortedGE_iff_antitone_get, Antitone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
⊢ b = b

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun j ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)

Tactic:
]

Goal state after:
case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun j ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ op (g k.castSucc) (g k.succ) = op (g k.castSucc) (g k.succ)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ g k.succ = g k.succ

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ g k.castSucc = g k.castSucc

pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ ↑k < ↑j

pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
]

Goal state after:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ ↑k < ↑j

case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ ↑k.castSucc < ↑j

Tactic:
]

Goal state after:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ ↑k.castSucc < ↑j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ g k.succ = g k.succ

pp: case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ ↑j < ↑k

pp: case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc

Tactic:
]

Goal state after:
case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ ↑j < ↑k

case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc
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 b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
]

Goal state after:
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 b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
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 b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
]

Goal state after:
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 b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ s = {a} ∪ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ : Pairwise R l
⊢ Pairwise R l

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ : Pairwise R l
⊢ Pairwise R l
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : 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 : α}, [a, b] <+ l → R a b

Tactic:
]

Goal state after:
α : 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 : α}, [a, b] <+ l → R a b
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.reverse.head ⋯)

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.reverse.head ⋯)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.dropLast

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.dropLast
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ : List α
hab : ¬Lex r (a :: l₁) (a :: l₂)
hba : ¬Lex r (a :: l₂) (a :: l₁)
⊢ a :: l₂ = a :: l₂

Tactic:
]

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

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1)

Tactic:
]

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
]

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))

Tactic:
]

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
]

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : LT α
l l' : List α
⊢ Lex (fun x1 x2 ↦ x1 < x2) l l' ↔ Lex (fun x1 x2 ↦ x1 < x2) l l'

Tactic:
]

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

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u < a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
]

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u < a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b ↦ (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)) l.ranges

Tactic:
]

Goal state after:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b ↦ (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)) l.ranges
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l

Tactic:
]

Goal state after:
α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l
Module: Mathlib.Data.List.Chain

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case cons_cons.a
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ head :: (l₁ ++ a :: b :: l₂) = ?m.103 :: (?m.104 ++ a :: b :: ?cons_cons.l₂)

pp: α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ α

pp: α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

pp: case cons_cons.l₂
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

Tactic:
]

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.toList.prod

Tactic:
]

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

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (map f s).prod = (map f s).prod

Tactic:
]

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 = a * b

Tactic:
]

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

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = a ^ count a s

Tactic:
]

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

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun x1 x2 ↦ x1 * x2) 1 s)

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun x1 x2 ↦ x1 * x2) 1 s)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
inst✝ : Trans R R R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
]

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a b : α
inst✝ : Trans R R R
hl : Pairwise R (a :: l)
hb : b ∈ l
⊢ R a b
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)

Tactic:
]

Goal state after:
case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)