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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b ↦ decide (p b)) l) = List.filterMap (fun x ↦ if p x then f x else none) l

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b ↦ decide (p b)) l) = List.filterMap (fun x ↦ if p x then f x else none) l
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ p a
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ y = z ∧ _root_.Disjoint x y

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ _root_.Disjoint x y ∧ y = z
Module: Mathlib.Data.Finset.Empty

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ IsEmpty ↥s ↔ s = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Finset α
⊢ IsEmpty ↥s ↔ s = ∅
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t

Tactic:
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take n l₁ <+: List.take n l₂

Tactic:
simpa using

Goal state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take n l₁ <+: l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.cons
α : Type u_1
tail✝¹ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝¹ → tail✝¹ = l₁ ++ drop l₁.length tail✝¹
head✝ : α
tail✝ : List α
h' : tail✝ <+: tail✝¹
h : head✝ :: tail✝ <+: head✝ :: tail✝¹
⊢ head✝ :: tail✝¹ = head✝ :: tail✝ ++ drop (head✝ :: tail✝).length (head✝ :: tail✝¹)

Tactic:
simpa using

Goal state after:
case cons.cons
α : Type u_1
tail✝¹ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝¹ → tail✝¹ = l₁ ++ drop l₁.length tail✝¹
head✝ : α
tail✝ : List α
h' : tail✝ <+: tail✝¹
h : head✝ :: tail✝ <+: head✝ :: tail✝¹
⊢ tail✝¹ = tail✝ ++ drop tail✝.length tail✝¹
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons
α : Type u_1
x : α
l : List α
IH : l.tails.length = l.length + 1
⊢ (x :: l).tails.length = (x :: l).length + 1

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
x : α
l : List α
IH : l.tails.length = l.length + 1
⊢ l.tails.length = l.length + 1
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
apply ext_getElem

Goal state after:
case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : f.symm x ∈ s
⊢ x ∈ t

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : f.symm x ∈ s
⊢ x ∈ t
Module: Mathlib.Data.Fintype.OfMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ s
Module: Mathlib.Data.Fintype.OfMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ l.toFinset

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ l
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ f a ∉ map f s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ a ∉ s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ Disjoint s.toFinset t.toFinset ↔ Disjoint s t

Tactic:
by simp only [← disjoint_coe, coe_toFinset]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Prop), x ∈ { val := {True, False}, nodup := fintype._proof_1 }

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Prop), x ∨ ¬x
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
ha : a ∉ s
x : α
hx : x ∈ cons a s ha
⊢ ⟨x, hx⟩ ∈ (cons a s ha).attach ↔ ⟨x, hx⟩ ∈ cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯

Tactic:
simpa using

Goal state after:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
x : α
hx : x ∈ cons a s ha
⊢ x = a ∨ x ∈ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ ⟨x, hx⟩ ∈ (insert a s).attach ↔ ⟨x, hx⟩ ∈ insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ x = a ∨ x ∈ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.18
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p ↑x

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.18
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p ↑x
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ a ∈ s, p a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
simpa [subtype_map] using h

Goal state after:
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h : (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) i = (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) j
⊢ i = j

Tactic:
simpa using

Goal state after:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h : (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) i = (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) j
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
simpa using

Goal state after:
k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ ↑a = ↑b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ Injective fun a ↦ i ↑a ⋯

Tactic:
intro ⟨_, _⟩

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
val✝ : α
property✝ : val✝ ∈ s
⊢ ∀ ⦃a₂ : ↥s⦄, (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩ = (fun a ↦ i ↑a ⋯) a₂ → ⟨val✝, property✝⟩ = a₂
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
val✝¹ : α
property✝¹ : val✝¹ ∈ s
val✝ : α
property✝ : val✝ ∈ s
h : (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
simpa using

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
val✝¹ : α
property✝¹ : val✝¹ ∈ s
val✝ : α
property✝ : val✝ ∈ s
h : (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩
⊢ val✝¹ = val✝
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.MapsTo f ↑(range n) ↑s

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ ∀ ⦃x : ℕ⦄, x < n → f x ∈ s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
simpa using

Goal state after:
n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ (↑i + 1) % n = ↑i + 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
x : β
hx : x ∈ ↑t
⊢ x ∈ f' '' ↑s.attach

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
x : β
hx : x ∈ ↑t
⊢ ∃ a, ∃ (h : a ∈ s), f a ⋯ = x
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f =
    ((ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i.castSucc * n + ↑j, ⋯⟩).concat
        (ofFn fun j ↦ f ⟨↑(Fin.last m) * n + ↑j, ⋯⟩)).flatten

Tactic:
succ_mul

Goal state after:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun i ↦ f (Fin.cast ⋯ i)) =
    ((ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i.castSucc * n + ↑j, ⋯⟩).concat
        (ofFn fun j ↦ f ⟨↑(Fin.last m) * n + ↑j, ⋯⟩)).flatten
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ b.castLT ⋯ ≤ a.castLT ha

Tactic:
simpa using

Goal state after:
n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑b ≤ ↑a
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simpa using

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ x.castSucc
h' : y.succAbove x ≠ 0
⊢ (y.succAbove x).pred h' = x

Tactic:
simp only [succAbove_of_le_castSucc _ _ h, pred_succ]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
⊢ succAbove 1 1 = 2

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ succAbove 1 1 = 2
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = ↑i

Tactic:
simpa using

Goal state after:
k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = ↑i
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f

Tactic:
refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f

Goal state after:
case refine_1
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn Fin.elim0).Nodup → Function.Injective Fin.elim0

case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
this : #(t \ image f s) = 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
this : #(t \ image f s) = 1
⊢ ∃! x, x ∈ t ∧ ∀ x_1 ∈ s, ¬f x_1 = x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ ∃! x, x ∉ image f univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ ∃! x, ∀ (x_1 : α), ¬f x_1 = x
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a ↦ ⟨f a, ⋯⟩) a = ⟨val✝, ⋯⟩

Tactic:
simpa using

Goal state after:
α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ f a = val✝
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
s : Finset α
hsn : #s ≤ n
hnα : n ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ
s : Finset α
hsn : #s ≤ n
hnα : n ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ #t = n
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
obtain hm | hm := h

Goal state after:
case refine_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l

Tactic:
simpa using

Goal state after:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
by
  rw [strongDownwardInduction]

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

Goal state before:
pp: α : Type u_1
l✝ : List α
x✝ : α
inst✝ : DecidableEq α
x y : α
l : List α
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hx : ¬(y = x ∧ x ∈ l)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using

Goal state after:
α : Type u_1
l✝ : List α
x✝ : α
inst✝ : DecidableEq α
x y : α
l : List α
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hx : ¬(y = x ∧ x ∈ l)
⊢ y = x → ¬x ∈ l
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n

Tactic:
simpa using

Goal state after:
n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
i : Fin n
⊢ x i = y i

Tactic:
simpa using

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
i : Fin n
⊢ x i = y i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
⊢ xₙ = yₙ

Tactic:
simpa using

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
⊢ xₙ = yₙ
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
⊢ some hd = l'[f 0]?

Tactic:
simpa using

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
⊢ some hd = l'[f 0]?
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j.castSucc
⊢ i.castSucc = j.castSucc

Tactic:
simpa using

Goal state after:
case cast.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j.castSucc
⊢ x i = x j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ Injective x

Tactic:
simpa using

Goal state after:
case refine_1
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ Injective x
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x ↦ x + 1) ⋯)) ix]?

Tactic:
simpa using

Goal state after:
case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?