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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons_cons.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?

Tactic:
simpa using

Goal state after:
case mp.cons_cons.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ l₁✝[n✝]? = l₂✝[f n✝]?
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Injective (natEmbeddingAux α)

Tactic:
by
  rintro m n h
  let := Classical.decEq α
  wlog hmlen : m ≤ n generalizing m n
  · exact (this h.symm <| le_of_not_ge hmlen).symm
  by_contra hmn
  have hmn : m < n := lt_of_le_of_ne hmlen hmn
  refine (Classical.choose_spec (exists_notMem_finset
    ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
      (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_
  refine Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)
  rw [h, natEmbeddingAux]

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ #(map (natEmbedding α) (range n)) = n

Tactic:
rw [card_map, card_range]

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

Goal state before:
pp: case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ some (l.get i) = some (l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) i))

Tactic:
simpa using

Goal state after:
case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ l[↑i] = l'[f ↑i]
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ b :: orderedInsert r a l ~ a :: b :: l
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)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

Tactic:
simpa using

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
⊢ xₚ = yₚ

Tactic:
simpa using

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
⊢ xₚ = yₚ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i < j
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

Tactic:
simpa using

Goal state after:
case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ xs → (r a x ↔ s (f a) (f x))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype ↑{i | i ≤ n}

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype ↑{i | i ≤ n}
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))

Tactic:
simpa using

Goal state after:
case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ xs → (r x a ↔ s (f x) (f a))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
p : Finset α → Prop
h : ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
s : Finset α
⊢ p s

Tactic:
simpa using

Goal state after:
α : Type u
p : Finset α → Prop
h : ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
s : Finset α
⊢ p s
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨0, hi⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

Tactic:
simpa using

Goal state after:
case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ x = l[↑n]
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
simpa using

Goal state after:
case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ x = l[↑m]
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 i.rev = snoc (f ∘ rev) a i

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
simpa using

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

Goal state before:
pp: case cons
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (↑(Finset.cons a s ha)) hs

Tactic:
simpa using

Goal state after:
case cons
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (Insert.insert a ↑s) ⋯
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise r (l.merge l' fun x1 x2 ↦ decide (r x1 x2))

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise r (l.merge l' fun x1 x2 ↦ decide (r x1 x2))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ decide (r a c) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a c
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a ?m.42

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a ?m.42
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r b c

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r b c
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b : α
⊢ (decide (r a b) || decide (r b a)) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b : α
⊢ r a b ∨ r b a
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ r a b) l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l'

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ r a b) l'
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ Pairwise r (l.mergeSort fun x1 x2 ↦ decide (r x1 x2))

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ Pairwise r (l.mergeSort fun x1 x2 ↦ decide (r x1 x2))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ decide (r x✝² x✝¹) = true → decide (r x✝¹ x✝) = true → decide (r x✝² x✝) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ r x✝² x✝¹ → r x✝¹ x✝ → r x✝² x✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), (decide (r a b) || decide (r b a)) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), r a b ∨ r b a
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z = x ∨ z = y
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedLT
hl₂ : l₂.SortedGT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedLT
hl₂ : l₂.SortedGT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedGT
hl₂ : l₂.SortedLT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedGT
hl₂ : l₂.SortedLT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Type u_1
ai : ℕ
a b : Fin ai → α
h : ⟨ai, a⟩.snd = ⟨ai, b⟩.snd ∘ Fin.cast ⋯
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Tactic:
simpa using

Goal state after:
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : ⟨ai, a⟩.snd = ⟨ai, b⟩.snd ∘ Fin.cast ⋯
⊢ 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:
try (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 ∈ l

Tactic:
try (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:
try (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: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h✝ : Pairwise R l
a b : α
h : R a b
⊢ Decidable.decide (R a b) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h✝ : Pairwise R l
a b : α
h : R a b
⊢ R a b
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.prod

Tactic:
conv_rhs => rw [← coe_toList s]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = (↑s.toList).prod
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
simpa using

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ l₂.getLast? → ∀ (y : α), y ∈ l₃.head? → R x y
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x ↦ count x l) l.dedup).sum = l.length

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x ↦ count x l) l.dedup).sum = l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l[↑k] = l[(l.length - n % l.length + ↑k + n) % l.length]
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝ : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
hab : Rel r a✝ b✝
hst : Rel (Rel r) as✝ bs✝
ih : Rel r as✝.join bs✝.join
⊢ Rel r (a✝ ::ₘ as✝).join (b✝ ::ₘ bs✝).join

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝ : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
hab : Rel r a✝ b✝
hst : Rel (Rel r) as✝ bs✝
ih : Rel r as✝.join bs✝.join
⊢ Rel r (a✝ + as✝.join) (b✝ + bs✝.join)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ b ∈ t.disjiUnion (fun a ↦ {x ∈ s | f x = a}) ⋯ ↔ b ∈ {c ∈ s | f c ∈ t}

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ f b ∈ t ∧ b ∈ s ↔ b ∈ s ∧ f b ∈ t
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
x✝ : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
x✝ : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
h : l.reverse ~r l'
⊢ l ~r l'.reverse

Tactic:
simpa using

Goal state after:
case mp
α : Type u
l l' : List α
h : l.reverse ~r l'
⊢ l ~r l'.reverse
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : M
l : List M
a : M
h : a ∈ ⟦l⟧
⊢ a ∣ prod ⟦l⟧

Tactic:
simpa using

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : M
l : List M
a : M
h : a ∈ ⟦l⟧
⊢ a ∣ l.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'

Tactic:
simpa using

Goal state after:
case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ a :: l ~r l ++ [a]

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
a : α
⊢ a :: l ~r l ++ [a]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]

Tactic:
simp only [getLast_append, dropLast_concat]

Goal state after:
case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False