-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_insertIdx_iff {l₁ l₂ : List α} {n : ℕ} {a : α} :
    insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Proof state:
case inr
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length ≥ n
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
exact perm_insertIdx_iff_of_le hn₁ (le_trans hn₁ hle) _

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂

Result:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Proof state:
case inl.inr
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
apply iff_of_false

Result:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ insertIdx n a l₂

case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Proof state:
case inl.inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
⊢ l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
rw [insertIdx_of_length_lt _ _ _ hn₂]

Result:
no goals

Proof state:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : (insertIdx n a l₂).length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ insertIdx n a l₂
⊢ False

Tactic:
exact (hn₁.trans_le hn₂).not_le (length_le_length_insertIdx ..)

Result:
no goals

Proof state:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
rw [perm_comm, this (le_of_not_le hle), perm_comm]

Result:
no goals

Proof state:
case inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ insertIdx n a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
rw [insertIdx_of_length_lt _ _ _ hn₁]

Result:
case inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Proof state:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ insertIdx n a l₂

Tactic:
intro h

Result:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ insertIdx n a l₂
⊢ False

Proof state:
case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Tactic:
exact fun h ↦ (hn₁.trans_le hn₂).not_le h.length_eq.ge

Result:
no goals

Proof state:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ insertIdx n a l₂
⊢ False

Tactic:
rw [h.length_eq] at hn₁

Result:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : (insertIdx n a l₂).length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ insertIdx n a l₂
⊢ False