mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ↑(map f s) = ⇑f '' ↑s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x ↦ x ∈ s)) s.val.attach = s.val

Tactic:
exact Multiset.attach_map_val _

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

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

Tactic:
← Finset.coe_ssubset,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ ↑s.toFinset ⊂ ↑t ↔ s ⊂ ↑t
Module: Mathlib.Data.Fintype.Sets

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

Tactic:
← Finset.coe_ssubset,

Goal state after:
α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊂ ↑t.toFinset ↔ ↑s ⊂ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (image f s) = image f ({a ∈ s | p (f a)})

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : α
⊢ image f {a} = {f a}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
a : α
s : Finset α
⊢ image f (insert a s) = insert (f a) (image f s)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ (image f s).erase (f a) ⊆ image f (s.erase a)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ image f (s.erase a) = (image f s).erase (f a)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inl
a : Int
ha : 0 ≤ a
b : Int
hc : 0 ≤ 0
⊢ a * (b / 0) ≤ a * b / 0

pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c

Tactic:
· simp

Goal state after:
case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s ⊆ t
⊢ filterMap f s f_inj ⊆ filterMap f t f_inj

Tactic:
by grind

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

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ i.castPred ⋯ = i.rev.rev.castPred ⋯

Tactic:
castPred_inj,

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ i = i.rev.rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #({a} ∩ s) ≤ 1

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ #(insert a s) ≤ #s + 1

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 1 ∨ #{a, b} = 2

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
by grind

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

Goal state before:
pp: case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
| succ n =>

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ #∅ ≤ #t

pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
· simp

Goal state after:
case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ ∀ (a : α) (s_1 : Finset α),
    a ∉ s_1 → #(s ∪ s_1) + #(s ∩ s_1) = #s + #s_1 → #(s ∪ insert a s_1) + #(s ∩ insert a s_1) = #s + #(insert a s_1)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s ∪ t) = #s + #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) = #s + #t - #(s ∩ t)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) = #s + #t - #(s ∪ t)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) ≤ #s + #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) + #s = #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #s = #t - #(s ∩ t) - #(s \ t)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #(s ∩ t) - #(s \ t) = #(t \ (s ∩ t)) - #(s \ t)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(t \ (s ∩ t)) - #(s \ t) = #(t \ s) - #(s \ t)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #s ≤ #(t \ s)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #s ≤ #(s \ t) + #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s \ t) = #s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) ≤ #(t \ s) ↔ #s ≤ #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) < #(t \ s) ↔ #s < #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) = #(t \ s) ↔ #s = #t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ (u \ s).Nonempty

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ s ⊆ u.erase a ∧ u.erase a ⊆ t ∧ #(u.erase a) = k

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ #(t \ s) = 1

Tactic:
by grind

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

Goal state before:
pp: case inl
α : Type u_1
⊢ #∅ ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b

pp: case inr
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
x : α
hx : x ∈ s
h : ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s = {x}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
y : α
h✝ : P y ∧ ∀ x ∈ ∅, r x y
⊢ Nonempty α

Tactic:
exact ⟨y⟩

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
⊢ tail (update q 0 z) = tail q

Tactic:
by
  ext j
  simp [tail]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (Classical.choose ⋯)

Tactic:
apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := ⋯
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ f m ∈ image (fun i ↦ f ↑i) univ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
⊢ g ∘ tail q = tail (g ∘ q)

Tactic:
by
  ext j
  simp [tail]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #(univ \ s) = Fintype.card α - #s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t x x_1 x_2, t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x_1 ≠ x_2 ∧ t = {x, x_1, x_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
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.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t x x_1 x_2 x_3,
      t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x ≠ x_3 ∧ x_1 ≠ x_2 ∧ x_1 ≠ x_3 ∧ x_2 ≠ x_3 ∧ t = {x, x_1, x_2, x_3}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
exists_comm (α := Finset α)

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

Goal state before:
pp: case cons_duplicate
α : Type u_1
l : List α
x y✝ : α
l✝ : List α
a✝ : x ∈+ l✝
hm : x ∈ l✝
⊢ x ∈ y✝ :: l✝

Tactic:
exact mem_cons_of_mem _ hm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
hij : j ≤ i
h : #(g i) - 1 = #(g j) - 1
⊢ #(g j) ≤ #(g i)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
hij : j ≤ i
⊢ g i = g j → #(g i) - 1 = #(g j) - 1

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
hG : Antitone fun i ↦ #(g i) - 1
n : ℕ
hn : n ≤ #(g 0) - 1
hn' : ∀ (m : ℕ), n ≤ m → #(g m) - 1 = #(g n) - 1
⊢ n < #s ∧ ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
by grind

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
f : α → α
hs : Set.MapsTo f ↑∅ ↑∅
⊢ ∃ n ≤ #∅, ∀ (m : ℕ), n ≤ m → image f^[m] ∅ = image f^[n] ∅

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
j : Fin n
⊢ init (update q (last n) z) j = init q j

Tactic:
simp [init, Fin.ne_of_lt]

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

Goal state before:
pp: case zero
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
isLt✝ : 0 < n + 1 + m
⊢ (if h : 0 < n + 1 then cases a as ⟨0, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨0, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨0, isLt✝⟩)

pp: case succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
· simp

Goal state after:
case succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:

Tactic:
Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
        _ = #s.toFinset := s.toFinset_card.symm
        _ < Fintype.card α :=
          Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

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

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

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:
· simp

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✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.refine_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (a b : Fin l.length), ⟨f ↑a, ⋯⟩ ≤ ⟨f ↑b, ⋯⟩ ↔ a ≤ b

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
⊢ ∀ (ix : Fin l.length), l.get ix = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ?mp.refine_1) ix)

Tactic:
· simp

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
⊢ ∀ (ix : Fin l.length), l.get ix = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) ix)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
← Finset.coe_ssubset,

Goal state after:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ ↑hs.toFinset ⊂ ↑t ↔ s ⊂ ↑t
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊂ ht.toFinset ↔ ↑s ⊂ t

Tactic:
← Finset.coe_ssubset,

Goal state after:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ ↑s ⊂ ↑ht.toFinset ↔ ↑s ⊂ t
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.zero.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 hj : 0 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.zero.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
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

pp: case mpr.refine_1.succ.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
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.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
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
· simp

Goal state after:
case mpr.refine_1.zero.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
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

case mpr.refine_1.succ.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
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.refine_1.succ.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
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.succ.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
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.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
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
· simp

Goal state after:
case mpr.refine_1.succ.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
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.Fin.Tuple.Basic

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

pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)

Tactic:
· simp

Goal state after:
case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Irrefl r
l₁ l₂ : List α
h₁ : Pairwise r l₁
h₂ : Pairwise r l₂
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₂ ⊆ l₁

Tactic:
by grind

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

Goal state before:
pp: m✝ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j✝ : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m j : ℕ
hm : j < n - m
⊢ j < n

Tactic:
by grind

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

Goal state before:
pp: m✝¹ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m✝ m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
⊢ 0 < m + 1

Tactic:
by grind

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

Goal state before:
pp: m✝¹ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m✝ m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - (m + 1)), ¬p ⟨j, ⋯⟩
hnm : ¬p ⟨n - (m + 1), ⋯⟩
⊢ ∀ (j : ℕ) (hm : j < n - m), ¬p ⟨j, ⋯⟩

Tactic:
by grind

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

Goal state before:
pp: m✝ n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
m : ℕ
hj : ∀ (j : ℕ) (hm : j < n - 0), ¬p ⟨j, ⋯⟩
x✝ : ∃ k, p k
val✝ : ℕ
isLt✝ : val✝ < n
h✝ : p ⟨val✝, isLt✝⟩
⊢ False

Tactic:
by grind

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

Goal state before:
pp: m n✝ : ℕ
p✝ q : Fin n✝ → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n✝
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
⊢ ∀ (j : ℕ) (hm : j < n - n), ¬p ⟨j, ⋯⟩

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
p✝ q : Fin n → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ ∃ n, p n

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
p✝ q : Fin n → Prop
inst✝² : DecidablePred p✝
inst✝¹ : DecidablePred q
i j : Fin n
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ ∃ i h, p ↑⟨i, h⟩

Tactic:
by grind

Goal state after: