mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
⊢ ∀ ⦃i j : ℕ⦄ ⦃hi : i < (finRange n).length⦄ ⦃hj : j < (finRange n).length⦄, i < j → (finRange n)[i] < (finRange n)[j]

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
n : ℕ
⊢ ∃ s, #s = n + 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ (f '' u).Finite

Tactic:
by

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
⊢ p h.choose

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ ↑⋯.toFinset ⊆ s

Tactic:
by

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

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

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ InjOn f ↑⋯.toFinset

Tactic:
by

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

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

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

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

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
⊢ ∃ u, ↑u ⊆ s ∧ InjOn f ↑u ∧ image f u = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedLE ↔ l.SortedGE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedGE ↔ l.SortedLE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedLT ↔ l.SortedGT

Tactic:
by

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
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedGT ↔ l.SortedLT

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False
⊢ ∀ ⦃x y z : ↑s⦄, x < y → y < z → False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedLE ↔ l.SortedGE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedGE ↔ l.SortedLE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT

Tactic:
by

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
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.toDual) l).SortedGT ↔ l.SortedLT

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
⊢ Fin.find p h = 0 ↔ p 0

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise rb (map (⇑e) l) ↔ List.Pairwise ra l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise (Function.swap rb) (map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
⊢ l₁.flatten <+ l₂.flatten

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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

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

Tactic:
by

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

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
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
by

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).SortedLE ↔ l.SortedLE

Tactic:
by

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
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
by

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 : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
by

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

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ x ∉ filter p s

Tactic:
by

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

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).SortedGE ↔ l.SortedGE

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
⊢ find? p = if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ x ∉ {i ∈ s | ¬p i}

Tactic:
by

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).SortedGT ↔ l.SortedGT

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLE ↔ l.SortedGE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGE ↔ l.SortedLE

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
by

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
h : ∃ i, p i
⊢ decide (p h.choose) = true

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ (find? fun x ↦ decide (p x)).get ⋯ = Fin.find p h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLT ↔ l.SortedGT

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h ∈ find? fun b ↦ decide (p b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGT ↔ l.SortedLT

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
i : Fin n
⊢ i ∈ find? p ↔ p i = true ∧ ∀ (j : Fin n), j < i → ¬p j = true

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) ⋯)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
    dsimp only at hi
    subst hi
    simpa using h

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c (f a) ∨ r c b ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
← or_assoc,

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ ((r c (f a) ∨ r c b) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
by

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

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

Goal state before:
pp: α : Type u_3
l : List α
R : α → α → Prop
⊢ Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ Pairwise R l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l.tail
⊢ R (l.head ⋯) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hhead : R (l.head ⋯) (l.head ⋯)
⊢ R (l.head ⋯) a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
a✝ : Mem a tail✝
⊢ a ∈ tail✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
h : Pairwise R l
ha : a ∈ l
⊢ R l.head! a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (b :: l)

Tactic:
by

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

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

Tactic:
by

Goal state after: