awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ p.gcd q ≤ p - q

Tactic:
have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
this : p.gcd q ≤ p - q
⊢ q ≤ w.length - q

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ q ≤ (drop q w).length

Tactic:
have drop_len : q ≤ (drop q w).length := by
        rw [length_drop]
        have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
        lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
let : ∀ (z : List α) (hz : drop q w ++ z = w), take q (drop q w) = take q w
⊢ take q (drop q w) = take q w

Tactic:
let ⟨z, hz⟩ := per_q.drop_prefix
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
h : take q w = take q (drop q w ++ z)
convert_to : take q (drop q w) = take q (drop q w ++ z)
⊢ take q (drop q w) = take q w

Tactic:
convert_to take q (drop q w) = take q (drop q w ++ z)

Premises used: List.drop, List.take, HAppend.hAppend
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
h h₁ : take q w = take q w
⊢ take q w = take q (drop q w ++ z)

Tactic:
rw [hz]
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q (drop q w ++ z)

Tactic:
(take_append_of_le_length drop_len).symm

Premises used: List.take_append_of_le_length, Eq.symm
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q (drop q w ++ z)

Tactic:
exact (take_append_of_le_length drop_len).symm

Premises used: List.take_append_of_le_length, Eq.symm
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
⊢ take q (drop q w) = take q w

Tactic:
have take_eq : take q (drop q w) = take q w := by
          let ⟨z, hz⟩ := per_q.drop_prefix
          convert_to take q (drop q w) = take q (drop q w ++ z)
          · rw [hz]
          exact (take_append_of_le_length drop_len).symm
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
simp : p - q + q ≤ w.length - q + (p - q).gcd q
⊢ p - q + q - (p - q).gcd q ≤ (drop q w).length

Tactic:
simp
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ p - q + q ≤ w.length - q + (p - q).gcd q

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ (drop q w).HasPeriod ((p - q).gcd q)

Tactic:
have IH : HasPeriod (drop q w) ((p - q).gcd q) :=
        per_diff.gcd per_q' (by simp; lia)
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
h : w = take q (drop q w) ++ drop q w
inr : (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)
⊢ w.HasPeriod (p.gcd q)

Tactic:
convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)

Premises used: Nat.gcd, List.HasPeriod, List.drop, List.take, HAppend.hAppend
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)

Tactic:
exact (gcd_stable ▸ IH).take_append (p.gcd q) q (drop q w)
          (gcd_dvd_right p q) drop_len
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
inr : ∀ (x : Ordering) (hyp : compare p q = x), w.HasPeriod (p.gcd q)
⊢ w.HasPeriod (p.gcd q)

Tactic:
cases hyp : compare p q with
  | lt => -- if `p` is less than `q`, switch the two periods
      have p_lt_q := Nat.compare_eq_lt.mp hyp
      exact (gcd_comm q p ▸ per_q.gcd) per_p (add_comm p q ▸ len)
  | eq => simpa [(Nat.compare_eq_eq).mp hyp]
  | gt =>
      have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp
      have gcd_lt_p : p.gcd q < p := by
        have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
        exact this.lt_of_le (gcd_le_left q p_pos)
      have per_diff : HasPeriod (drop q w) (p - q) := by
        have : p = (p - q) + q := by lia
        exact per_q.drop_of_hasPeriod_add (this ▸ per_p)
      have per_q' : HasPeriod (drop q w) q := by
        apply @HasPeriod.factor _ (take q w) (drop q w) [] q
        all_goals simp_all
      have gcd_stable : (p - q).gcd q = p.gcd q := gcd_sub_self_left (le_of_lt q_lt_p)
      have drop_len : q ≤ (drop q w).length := by
        rw [length_drop]
        have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
        lia
      have take_eq : take q (drop q w) = take q w := by
          let ⟨z, hz⟩ := per_q.drop_prefix
          convert_to take q (drop q w) = take q (drop q w ++ z)
          · rw [hz]
          exact (take_append_of_le_length drop_len).symm
      -- the induction step
      have IH : HasPeriod (drop q w) ((p - q).gcd q) :=
        per_diff.gcd per_q' (by simp; lia)
      convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)
      · rw [take_eq, take_append_drop q w]
      · exact (gcd_stable ▸ IH).take_append (p.gcd q) q (drop q w)
          (gcd_dvd_right p q) drop_len

Premises used: Nat.gcd, List.HasPeriod, List.take_append_drop, Ord.compare, List.drop, List.take, HAppend.hAppend
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
⊢ l ~ l

Tactic:
Perm.refl _

Premises used: List.Perm.refl
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l : List α
⊢ Std.Symm.{u_1 + 1} (α := List α) Perm

Tactic:
⟨fun _ _ ↦ .symm⟩

Premises used: Std.Symm.mk, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ ~ l₂
⊢ l₁ ⊆ l₃ ↔ l₂ ⊆ l₃

Tactic:
⟨h.symm.subset.trans, h.subset.trans⟩

Premises used: List.Perm.subset, Iff.intro, List.Subset.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ ~ l₂
⊢ l₃ ⊆ l₁ ↔ l₃ ⊆ l₂

Tactic:
⟨fun h' => h'.trans h.subset, fun h' => h'.trans h.symm.subset⟩

Premises used: List.Perm.subset, Iff.intro, List.Subset.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
rw : (l.eraseIdx n).insertIdx n a ~ a :: l.eraseIdx n
⊢ l.set n a ~ a :: l.eraseIdx n

Tactic:
rw [← insertIdx_eraseIdx_self (Nat.ne_of_lt h)]

Premises used: List.insertIdx_eraseIdx_self, Nat.ne_of_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
h₁ : n ≤ (l.eraseIdx n).length
⊢ (l.eraseIdx n).insertIdx n a ~ a :: l.eraseIdx n

Tactic:
apply perm_insertIdx

Premises used: List.perm_insertIdx
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
h₁ : n ≤ l.length - 1
⊢ n ≤ (l.eraseIdx n).length

Tactic:
rw [length_eraseIdx_of_lt h]

Premises used: List.length_eraseIdx_of_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1

Tactic:
Nat.le_sub_one_of_lt h

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1

Tactic:
exact Nat.le_sub_one_of_lt h

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h :: l.eraseIdx n ~ l

Tactic:
simpa [h] using (set_perm_cons_eraseIdx h l[n]).symm

Premises used: List.set_perm_cons_eraseIdx, GetElem.getElem, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
rw : a :: l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
rw₁ : a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂
rw₂ rw₃ : l₁ ~ l₂ ↔ l₁ ~ l₂
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]

Premises used: List.perm_insertIdx, rel_congr_left, rel_congr_right, List.perm_cons
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
inr :
  ∀ (this : ∀ {l₁ l₂ : List α} (hle : l₁.length ≤ l₂.length), l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
    (hle : ¬l₁.length ≤ l₂.length), l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
wlog : ∀ {l₁ l₂ : List α} (hle : l₁.length ≤ l₂.length), l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

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

Premises used: List.length
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α} (hle : l₁.length ≤ l₂.length), l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
hle : ¬l₁.length ≤ l₂.length
inr : l₂.insertIdx n a ~ l₁.insertIdx n a ↔ l₁ ~ l₂
inr₁ : l₂ ~ l₁ ↔ l₁ ~ l₂
inr₂ inr₃ : l₁ ~ l₂ ↔ l₁ ~ l₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]

Premises used: List.perm_comm, Nat.le_of_not_ge
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
inl : l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [insertIdx_of_length_lt hn₁]

Premises used: List.insertIdx_of_length_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
inl inl₁ : l₁ ~ l₂ ↔ l₁ ~ l₂
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [insertIdx_of_length_lt hn₂]

Premises used: List.insertIdx_of_length_lt
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
inl : ¬l₁ ~ l₂.insertIdx n a
inl₁ : ¬l₁ ~ l₂
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
apply iff_of_false

Premises used: iff_of_false
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ (l₂.insertIdx n a).length < n

Tactic:
rw [h.length_eq] at hn₁

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
hn₃ : (l₂.insertIdx n a).length < n
⊢ l₂.length ≥ n

Tactic:
rw [h.length_eq] at hn₁

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
hn₃ : (l₂.insertIdx n a).length < n
hn₄ : l₂.length ≥ n
⊢ l₁ ~ l₂.insertIdx n a

Tactic:
rw [h.length_eq] at hn₁

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : (l₂.insertIdx n a).length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False

Tactic:
grind
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Tactic:
grind [Perm.length_eq]

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ l₂.length < n ∨ l₂.length ≥ n

Tactic:
cases Nat.lt_or_ge (length l₂) n with
    | inl hn₂ => rw [insertIdx_of_length_lt hn₂]
    | inr hn₂ =>
      apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]

Premises used: iff_of_false, List.Perm.length_eq, Nat.lt_or_ge, List.length
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length ≥ n
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
perm_insertIdx_iff_of_le hn₁ (Nat.le_trans hn₁ hle) _

Premises used: List.perm_insertIdx_iff_of_le, Nat.le_trans
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length ≥ n
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

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

Premises used: List.perm_insertIdx_iff_of_le, Nat.le_trans
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.length < n ∨ l₁.length ≥ n

Tactic:
cases Nat.lt_or_ge (length l₁) n with
  | inl hn₁ =>
    rw [insertIdx_of_length_lt hn₁]
    cases Nat.lt_or_ge (length l₂) n with
    | inl hn₂ => rw [insertIdx_of_length_lt hn₂]
    | inr hn₂ =>
      apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]
  | inr hn₁ =>
    exact perm_insertIdx_iff_of_le hn₁ (Nat.le_trans hn₁ hle) _

Premises used: iff_of_false, List.Perm.length_eq, Nat.lt_or_ge, List.length
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
n : ℕ
a : α
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a

Tactic:
perm_insertIdx_iff.mpr h

Premises used: Iff.mpr, List.perm_insertIdx_iff
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
hm : m < l₁.length
⊢ ∃ (h : n < l₂.length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n h =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm

Tactic:
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h

Premises used: List.getElem?_eq_some_iff, eq_comm, List.getElem?_eq_getElem
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm
inl :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm :: l₁.eraseIdx m ~
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm :: l₂.eraseIdx n ↔
    l₁ ~ l₂
inl₁ : l₁ ~ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm :: l₂.eraseIdx n ↔ l₁ ~ l₂
inl₂ : l₁ ~ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n hn :: l₂.eraseIdx n ↔ l₁ ~ l₂
inl₃ inl₄ : l₁ ~ l₂ ↔ l₁ ~ l₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Premises used: List.getElem_cons_eraseIdx_perm, rel_congr_left, rel_congr_right, List.perm_cons, GetElem.getElem
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h :
  ∃ (h : n < l₂.length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n h =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm
⊢ n < l₂.length

Tactic:
cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Premises used: List.getElem_cons_eraseIdx_perm, rel_congr_left, rel_congr_right, List.perm_cons, GetElem.getElem
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h :
  ∃ (h : n < l₂.length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n h =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm
hn : n < l₂.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm

Tactic:
cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Premises used: List.getElem_cons_eraseIdx_perm, rel_congr_left, rel_congr_right, List.perm_cons, GetElem.getElem
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
hm : m ≥ l₁.length
⊢ l₂.length ≤ n

Tactic:
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h

Premises used: List.getElem?_eq_none, eq_comm, List.getElem?_eq_none_iff
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
hm : m ≥ l₁.length
h₁ : l₂.length ≤ n
⊢ m ≥ l₁.length

Tactic:
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h

Premises used: List.getElem?_eq_none, eq_comm, List.getElem?_eq_none_iff
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
inr : l₁.eraseIdx m ~ l₂ ↔ l₁ ~ l₂
inr₁ inr₂ : l₁ ~ l₂ ↔ l₁ ~ l₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

Premises used: List.eraseIdx_of_length_le
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
⊢ m < l₁.length ∨ m ≥ l₁.length

Tactic:
cases Nat.lt_or_ge m l₁.length with
  | inl hm =>
    rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
    cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]
  | inr hm =>
    rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
    rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

Premises used: List.getElem_cons_eraseIdx_perm, List.getElem?_eq_some_iff, rel_congr_left, rel_congr_right, eq_comm, List.perm_cons, GetElem.getElem, Nat.lt_or_ge, List.eraseIdx_of_length_le, List.getElem?_eq_none_iff, List.length
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
h : ∀ (a c : List α), (Perm ∘r Perm) a c = (a ~ c)
⊢ Eq.{u_1 + 1} (α := (a c : List α) → Prop) (Perm ∘r Perm) Perm

Tactic:
funext a c
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
h : (Perm ∘r Perm) a c ↔ a ~ c
⊢ (Perm ∘r Perm) a c = (a ~ c)

Tactic:
apply propext

Premises used: propext
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
h : (Perm ∘r Perm) a c → a ~ c
h₁ : a ~ c → (Perm ∘r Perm) a c
⊢ (Perm ∘r Perm) a c ↔ a ~ c

Tactic:
constructor
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

Tactic:
fun ⟨b, hab, hba⟩ => Perm.trans hab hba

Premises used: _private.0.List.perm_comp_perm.match_1, List.Perm, List.Perm.trans
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

Tactic:
exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Tactic:
fun h => ⟨a, Perm.refl a, h⟩

Premises used: List.Perm.refl, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Tactic:
exact fun h => ⟨a, Perm.refl a, h⟩