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

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

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4

Tactic:
grind

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

Goal state before:
pp: case refl
n : ℕ
h : Fin n = Fin n
⊢ cast h = Fin.cast ⋯

Tactic:
rfl

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

Goal state before:
pp: case inr
α : 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 : ℕ
this : ∀ (i j : ℕ), j ≤ i → (#(g i) - 1 = #(g j) - 1 ↔ g i = g j)
hij : ¬j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j

Tactic:
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
h : #(g i) - 1 = #(g j) - 1
⊢ #(g j) ≤ #(g i)

Tactic:
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:
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:
grind

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
rfl

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯

Tactic:
rfl

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

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : i < n + m
⊢ as ⟨i, ⋯⟩ = as ⟨i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

Tactic:
rfl

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : i < n + m
⊢ bs ⟨i - n, ⋯⟩ = bs ⟨i - n, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

Tactic:
rfl

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
rfl

Goal state after:
case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : ¬i < n + m
⊢ b = b

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding x✝ = e x✝

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ (orderedInsert r a []).length = [].length + 1

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r a tail✝).length = tail✝.length + 1
⊢ (orderedInsert r a (head✝ :: tail✝)).length = (head✝ :: tail✝).length + 1

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
⊢ a ∈ orderedInsert r b [] ↔ a = b ∨ a ∈ []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b head✝ : α
tail✝ : List α
tail_ih✝ : a ∈ orderedInsert r b tail✝ ↔ a = b ∨ a ∈ tail✝
⊢ a ∈ orderedInsert r b (head✝ :: tail✝) ↔ a = b ∨ a ∈ head✝ :: tail✝

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
hl₁ : ∀ (a : α), a ∈ [] → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ [] → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x head✝ : α
tail✝ : List α
tail_ih✝ :
  (∀ (a : α), a ∈ tail✝ → (r a x ↔ s (f a) (f x))) →
    (∀ (a : α), a ∈ tail✝ → (r x a ↔ s (f x) (f a))) →
      map f (orderedInsert r x tail✝) = orderedInsert s (f x) (map f tail✝)
hl₁ : ∀ (a : α), a ∈ head✝ :: tail✝ → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ head✝ :: tail✝ → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x (head✝ :: tail✝)) = orderedInsert s (f x) (map f (head✝ :: tail✝))

Tactic:
grind

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case mpr.refine_2
α : 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)
⊢ ∀ (ix : ℕ),
    l[ix]? = l'[(OrderEmbedding.ofStrictMono (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) ix]?

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
hx : ¬x ∈ []
⊢ (orderedInsert r x []).erase x = []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x head✝ : α
tail✝ : List α
tail_ih✝ : ¬x ∈ tail✝ → (orderedInsert r x tail✝).erase x = tail✝
hx : ¬x ∈ head✝ :: tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
⊢ [] <+ orderedInsert r x []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ <+ orderedInsert r x tail✝
⊢ head✝ :: tail✝ <+ orderedInsert r x (head✝ :: tail✝)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
head✝ : α
tail✝ : List α
tail_ih✝ : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ orderedInsert r a (head✝ :: tail✝)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
orderedInsert_cons,

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : (if r x a then x :: a :: as else a :: orderedInsert r x as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.List.Sort

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

Tactic:
grind

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

Goal state before:
pp: case fst
n : ℕ
α : Fin (n + 1) → Type u_3
x✝ : (i : Fin (n + 1)) → α i
⊢ ((insertNthEquiv α 0).symm x✝).1 = ((consEquiv α).symm x✝).1

Tactic:
rfl

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

Goal state before:
pp: case snd
n : ℕ
α : Fin (n + 1) → Type u_3
x✝¹ : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ ((insertNthEquiv α 0).symm x✝¹).2 x✝ = ((consEquiv α).symm x✝¹).2 x✝

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
hr : Pairwise r c
hc : c <+ []
⊢ c <+ insertionSort r []

Tactic:
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:
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:
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:
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:
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:
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:
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:
grind

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

Goal state before:
pp: case refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
⊢ Fin.find p h = i → p i ∧ ∀ (j : Fin n), j < i → ¬p j

Tactic:
grind

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

Goal state before:
pp: case refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
h : ∃ k, p k
x✝ : p i ∧ ∀ (j : Fin n), j < i → ¬p j
hm : p i
hlt : ∀ (j : Fin n), j < i → ¬p j
this : Fin.find p h ≤ i
⊢ Fin.find p h = i

Tactic:
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:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedGE ↔ Pairwise (fun x1 x2 ↦ x1 ≥ x2) l

Tactic:
by
  simp only [sortedGE_iff_antitone_get, antitone_iff_forall_lt, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLT ↔ Pairwise (fun x1 x2 ↦ x1 < x2) l

Tactic:
simp only [sortedLT_iff_strictMono_get, StrictMono, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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:
grind

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ Nat.find ⋯ = ↑(Fin.find (fun x ↦ p ↑x) ⋯)

Tactic:
val_find

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

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

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ ∀ (n_1 : ℕ), n_1 ≤ h.choose → (p n_1 ↔ ∃ h, p ↑⟨n_1, h⟩)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedLE ↔ l.SortedGE

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedGE ↔ l.SortedLE

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ Fin.find p h < i → ∃ m, m < i ∧ p m

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedLT ↔ l.SortedGT

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedGT ↔ l.SortedLT

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ Fin.find p h ≤ i → ∃ m, m ≤ i ∧ p m

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → True) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ

Tactic:
implies_true,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    True ∧ ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ
Module: Mathlib.Data.List.Flatten

Goal state before:
pp: case slnil
α : Type u_1
l₁ l₂ : List (List α)
⊢ [].flatten <+ [].flatten

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : l₁✝.flatten <+ l₂✝.flatten
⊢ l₁✝.flatten <+ (a✝¹ :: l₂✝).flatten

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : l₁✝.flatten <+ l₂✝.flatten
⊢ (a✝¹ :: l₁✝).flatten <+ (a✝¹ :: l₂✝).flatten

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f g : α → List β
h : ∀ (a : α), a ∈ [] → f a <+ g a
⊢ flatMap f [] <+ flatMap g []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f g : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), a ∈ tail✝ → f a <+ g a) → flatMap f tail✝ <+ flatMap g tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → f a <+ g a
⊢ flatMap f (head✝ :: tail✝) <+ flatMap g (head✝ :: tail✝)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
i : Nat
h : i < [].length
⊢ drop i (take (i + 1) []) = [[][i]]

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i : Nat) (h : i < tail✝.length), drop i (take (i + 1) tail✝) = [tail✝[i]]
i : Nat
h : i < (head✝ :: tail✝).length
⊢ drop i (take (i + 1) (head✝ :: tail✝)) = [(head✝ :: tail✝)[i]]

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
x : List α
⊢ x ++ (map (fun x_1 ↦ x_1 ++ x) []).flatten = (map (fun x_1 ↦ x ++ x_1) []).flatten ++ x

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
x head✝ : List α
tail✝ : List (List α)
tail_ih✝ : x ++ (map (fun x_1 ↦ x_1 ++ x) tail✝).flatten = (map (fun x_1 ↦ x ++ x_1) tail✝).flatten ++ x
⊢ x ++ (map (fun x_1 ↦ x_1 ++ x) (head✝ :: tail✝)).flatten = (map (fun x_1 ↦ x ++ x_1) (head✝ :: tail✝)).flatten ++ x

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
hl : [] ≠ []
hl' : [].head hl ≠ []
⊢ ([].head hl).head hl' = [].flatten.head ⋯

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
hl : head✝ :: tail✝ ≠ []
hl' : (head✝ :: tail✝).head hl ≠ []
⊢ ((head✝ :: tail✝).head hl).head hl' = (head✝ :: tail✝).flatten.head ⋯

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
⊢ l ≠ []

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.head ⋯ ≠ []
⊢ l ≠ []

Tactic:
grind

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

Goal state before:
pp: case inl
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
h✝ : l = []
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
grind

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

Goal state before:
pp: case inr
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
h✝ : ∃ l' b, l = l'.concat b
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.getLast ⋯ ≠ []
⊢ l ≠ []

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLT ↔ l.SortedLT

Tactic:
simp_rw [sortedLT_iff_pairwise]
  exact e.ltEmbedding.pairwise_listMap

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

Goal state before:
pp: case pos
n : ℕ
p : Fin n → Bool
h✝ : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h✝)

Tactic:
grind

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

Goal state before:
pp: case neg
n : ℕ
p : Fin n → Bool
h✝ : ¬∃ i, p i = true
⊢ find? p = none

Tactic:
grind

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
hjk : ↑j ≠ ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
by
  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
    · rwa [Fin.lt_def]
  · exact False.elim (hjk h.symm)
  · rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
R✝ : α✝ → α✝ → Prop
l✝ : List α✝
a : α✝
α : Type u_3
l : List α
R : α → α → Prop
l' : List α
h : 1 < l'.length
⊢ l' ≠ []

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
l : List α
⊢ (l = [] ∨ ∃ a_1 b, R a_1 b ∧ ∃ x, IsChain R (b :: x) ∧ a = a_1 ∧ l = b :: x) ↔
    l = [] ∨ ∃ b, R a b ∧ ∃ x, IsChain R (b :: x) ∧ l = b :: x

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ [] → b ∈ [].tail → R a b → S a b
⊢ IsChain S []

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
R S : α → α → Prop
l : List α
a✝ : α
H : ∀ (a b : α), a ∈ [a✝] → b ∈ [a✝].tail → R a b → S a b
⊢ IsChain S [a✝]

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
R S : α → α → Prop
l : List α
a✝ b✝ : α
l✝ : List α
hr✝ : R a✝ b✝
h✝ : IsChain R (b✝ :: l✝)
h_ih✝ : (∀ (a b : α), a ∈ b✝ :: l✝ → b ∈ (b✝ :: l✝).tail → R a b → S a b) → IsChain S (b✝ :: l✝)
H : ∀ (a b : α), a ∈ a✝ :: b✝ :: l✝ → b ∈ (a✝ :: b✝ :: l✝).tail → R a b → S a b
⊢ IsChain S (a✝ :: b✝ :: l✝)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)

Tactic:
grind

Goal state after: