mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z 0 = cons z p 0

pp: case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
i✝ : Fin n
⊢ update (cons x p) 0 z i✝.succ = cons z p i✝.succ

Tactic:
<;>

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z 0 = cons z p 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
i✝ : Fin n
⊢ update (cons x p) 0 z i✝.succ = cons z p i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

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

pp: case succ
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ cons (q 0) (tail q) i✝.succ = q i✝.succ

Tactic:
<;>

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (q 0) (tail q) 0 = q 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ cons (q 0) (tail q) i✝.succ = q i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
by
  ext j
  cases j using Fin.cases <;> simp [tail]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
rw [predAbove_last_of_ne_last hi]

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

Goal state before:
pp: case zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
⊢ cons x₀ x 0 = cons x₀ x j → 0 = j

pp: case succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x j → i✝.succ = j

Tactic:
<;>

Goal state after:
case zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
⊢ cons x₀ x 0 = cons x₀ x j → 0 = j

case succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x j → i✝.succ = j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case zero.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

pp: case zero.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x 0 = cons x₀ x i✝.succ → 0 = i✝.succ

pp: case succ.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x 0 → i✝.succ = 0

pp: case succ.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝¹ i✝ : Fin n
⊢ cons x₀ x i✝¹.succ = cons x₀ x i✝.succ → i✝¹.succ = i✝.succ

Tactic:
<;>

Goal state after:
case zero.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

case zero.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x 0 = cons x₀ x i✝.succ → 0 = i✝.succ

case succ.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x 0 → i✝.succ = 0

case succ.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝¹ i✝ : Fin n
⊢ cons x₀ x i✝¹.succ = cons x₀ x i✝.succ → i✝¹.succ = i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
<;>

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
<;>

Goal state after:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case left
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin m
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (castAdd n i✝) = v (castAdd n i✝)

pp: case right
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin n
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (natAdd m i✝) = v (natAdd m i✝)

Tactic:
<;>

Goal state after:
case left
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin m
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (castAdd n i✝) = v (castAdd n i✝)

case right
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin n
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (natAdd m i✝) = v (natAdd m i✝)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
i : Fin m
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)

pp: case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
j : Fin n
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
i : Fin m
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inl i) = Sum.elim xs ys (Sum.inl i)

case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
j : Fin n
⊢ (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) (Sum.inr j) = Sum.elim xs ys (Sum.inr j)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin m
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inl y)) = Sum.inl y

pp: case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin n
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inr y)) = Sum.inr y

Tactic:
<;>

Goal state after:
case inl
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin m
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inl y)) = Sum.inl y

case inr
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
y : Fin n
⊢ (fun i ↦ addCases Sum.inl Sum.inr i) (Sum.elim (castAdd n) (natAdd m) (Sum.inr y)) = Sum.inr y
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (castAdd n i)) = castAdd n i

pp: case refine_2
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (natAdd m i)) = natAdd m i

Tactic:
<;>

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (castAdd n i)) = castAdd n i

case refine_2
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) (natAdd m i)) = natAdd m i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.inl
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
j : Fin n
y : α j.castSucc
⊢ snoc (update p j y) x j.castSucc = update (snoc p x) j.castSucc y j.castSucc

pp: case cast.inr
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
hne : j ≠ i
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc

Tactic:
<;>

Goal state after:
case cast.inl
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
j : Fin n
y : α j.castSucc
⊢ snoc (update p j y) x j.castSucc = update (snoc p x) j.castSucc y j.castSucc

case cast.inr
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
hne : j ≠ i
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case last
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ update (snoc p x) (last n) z (last n) = snoc p z (last n)

pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
i✝ : Fin n
⊢ update (snoc p x) (last n) z i✝.castSucc = snoc p z i✝.castSucc

Tactic:
<;>

Goal state after:
case last
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ update (snoc p x) (last n) z (last n) = snoc p z (last n)

case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
i✝ : Fin n
⊢ update (snoc p x) (last n) z i✝.castSucc = snoc p z i✝.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

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

pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ snoc (init q) (q (last n)) i✝.castSucc = q i✝.castSucc

Tactic:
<;>

Goal state after:
case last
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (init q) (q (last n)) (last n) = q (last n)

case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ snoc (init q) (q (last n)) i✝.castSucc = q i✝.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

pp: case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Tactic:
<;>

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
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, ⋯⟩

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

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, ⋯⟩

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

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, ⋯⟩

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

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
lt_add : i < n + m
⊢ as ⟨i, ⋯⟩ = as ⟨i, ⋯⟩

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

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, ⋯⟩

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

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, ⋯⟩

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
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (drop (f 0 + 1) l')[f' ix]?

Tactic:
rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (hd :: tl)[ix + 1]?

α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 + 1 ≤ f (ix + 1)
Module: Mathlib.Data.List.NodupEquivFin

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

pp: case mp.cons_cons.refine_1.zero.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔ 0 ≤ n✝ + 1

pp: case mp.cons_cons.refine_1.succ.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ≤ if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ↔ n✝ + 1 ≤ 0

pp: case mp.cons_cons.refine_1.succ.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝¹ n✝ : ℕ
⊢ ((if n✝¹ + 1 = 0 then 0 else (f (n✝¹ + 1).pred).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔
    n✝¹ + 1 ≤ n✝ + 1

Tactic:
<;>

Goal state after:
case mp.cons_cons.refine_1.zero.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ((if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ≤ if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ↔ 0 ≤ 0

case mp.cons_cons.refine_1.zero.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔ 0 ≤ n✝ + 1

case mp.cons_cons.refine_1.succ.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ ((if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ≤ if 0 = 0 then 0 else (f (Nat.pred 0)).succ) ↔ n✝ + 1 ≤ 0

case mp.cons_cons.refine_1.succ.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝¹ n✝ : ℕ
⊢ ((if n✝¹ + 1 = 0 then 0 else (f (n✝¹ + 1).pred).succ) ≤ if n✝ + 1 = 0 then 0 else (f (n✝ + 1).pred).succ) ↔
    n✝¹ + 1 ≤ n✝ + 1
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ i, P i

pp: case inr
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ i, P i

Tactic:
<;>

Goal state after:
case inl
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ i, P i

case inr
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ i, P i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ i, P i

pp: case inr
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ i, P i

Tactic:
<;>

Goal state after:
case inl
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ i, P i

case inr
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ i, P i
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

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

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

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
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ orderedInsert r a [] = takeWhile (fun b ↦ decide ¬r a b) [] ++ a :: dropWhile (fun b ↦ decide ¬r a b) []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ :
  orderedInsert r a tail✝ = takeWhile (fun b ↦ decide ¬r a b) tail✝ ++ a :: dropWhile (fun b ↦ decide ¬r a b) tail✝
⊢ orderedInsert r a (head✝ :: tail✝) =
    takeWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝) ++ a :: dropWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ orderedInsert r a [] = takeWhile (fun b ↦ decide ¬r a b) [] ++ a :: dropWhile (fun b ↦ decide ¬r a b) []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ :
  orderedInsert r a tail✝ = takeWhile (fun b ↦ decide ¬r a b) tail✝ ++ a :: dropWhile (fun b ↦ decide ¬r a b) tail✝
⊢ orderedInsert r a (head✝ :: tail✝) =
    takeWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝) ++ a :: dropWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝)
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 ∈ []

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

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

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✝
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 [])

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

Goal state after:
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 [])

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✝))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ insertionSort r [] ~ []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : insertionSort r tail✝ ~ tail✝
⊢ insertionSort r (head✝ :: tail✝) ~ head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ insertionSort r [] ~ []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : insertionSort r tail✝ ~ tail✝
⊢ insertionSort r (head✝ :: tail✝) ~ head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ Pairwise r [] → insertionSort r [] = []

pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise r tail✝ → insertionSort r tail✝ = tail✝
⊢ Pairwise r (head✝ :: tail✝) → insertionSort r (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ Pairwise r [] → insertionSort r [] = []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise r tail✝ → insertionSort r tail✝ = tail✝
⊢ Pairwise r (head✝ :: tail✝) → insertionSort r (head✝ :: tail✝) = head✝ :: tail✝