awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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
have rw : q ≤ w.length - q
Tactic: rw [length_drop]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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
have rw : (p - q).gcd q ≤ p - q
Tactic: rw [← gcd_stable]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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 - q).gcd q ≤ p - q
have apply : 0 < p - q
Tactic: apply gcd_le_left q
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
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 ≤ w.length - q
have this : p.gcd q ≤ p - q
Tactic: have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
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
⊢ w.HasPeriod (p.gcd q)
have drop_len : 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
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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
have let : ∀ (z : List α) (hz : drop q w ++ z = w), take q (drop q w) = take q w
Tactic: let ⟨z, hz⟩ := per_q.drop_prefix
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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 w
have h : take q w = take q (drop q w ++ z)
Tactic: convert_to take q (drop q w) = take q (drop q w ++ z)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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)
⊢ take q (drop q w) = take q w
have convert_to : take q (drop q w) = take q (drop q w ++ z)
Tactic: convert_to take q (drop q w) = take q (drop q w ++ z)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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 w = take q (drop q w ++ z)
have h : take q w = take q w
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
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
⊢ w.HasPeriod (p.gcd q)
have take_eq : 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
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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 - (p - q).gcd q ≤ (drop q w).length
have simp : p - q + q ≤ w.length - q + (p - q).gcd q
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
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
⊢ w.HasPeriod (p.gcd q)
have IH : (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)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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)
⊢ w.HasPeriod (p.gcd q)
have h : w = take q (drop q w) ++ drop q w
Tactic: convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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
⊢ w.HasPeriod (p.gcd q)
have inr : (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)
Tactic: convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
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
⊢ w.HasPeriod (p.gcd q)
have inr : ∀ (x : Ordering) (hyp : compare p q = x), 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
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ l.set n a ~ a :: l.eraseIdx n
have rw : (l.eraseIdx n).insertIdx n a ~ a :: l.eraseIdx n
Tactic: rw [← insertIdx_eraseIdx_self (Nat.ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a ~ a :: l.eraseIdx n
have h₁ : n ≤ (l.eraseIdx n).length
Tactic: apply perm_insertIdx
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ (l.eraseIdx n).length
have h₁ : n ≤ l.length - 1
Tactic: rw [length_eraseIdx_of_lt h]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have rw : a :: l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Tactic: rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have rw₁ : a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂
Tactic: rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have rw₂ : l₁ ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have 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₂
Tactic: wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have wlog : ∀ {l₁ l₂ : List α} (hle : l₁.length ≤ l₂.length), l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Tactic: wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inr : l₂.insertIdx n a ~ l₁.insertIdx n a ↔ l₁ ~ l₂
Tactic: rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inr₁ : l₂ ~ l₁ ↔ l₁ ~ l₂
Tactic: rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inr₂ : l₁ ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
have inl : l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Tactic: rw [insertIdx_of_length_lt hn₁]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inl : l₁ ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [insertIdx_of_length_lt hn₂]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inl : ¬l₁ ~ l₂.insertIdx n a
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have inl₁ : ¬l₁ ~ l₂
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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
⊢ False
have hn₃ : (l₂.insertIdx n a).length < n
Tactic: rw [h.length_eq] at hn₁
Cleared hypotheses: hn₁, hn₂, h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have x : 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]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
have x : 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) _
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have 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
Tactic: rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have 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₂
Tactic: rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have inl₁ : l₁ ~ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ m hm :: 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 ..)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have inl₂ : l₁ ~ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n hn :: 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 ..)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have inl₃ : l₁ ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have hn : 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 ..)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have 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
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 ..)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have h₁ : l₂.length ≤ n
Tactic: rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
Cleared hypotheses: h, hm
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have inr : l₁.eraseIdx m ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
inr : l₁.eraseIdx m ~ l₂ ↔ l₁ ~ l₂
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have inr₁ : l₁ ~ l₂ ↔ l₁ ~ l₂
Tactic: rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
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
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
have x : 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]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a c : List α) → Prop) (Perm ∘r Perm) Perm
have h : ∀ (a c : List α), (Perm ∘r Perm) a c = (a ~ c)
Tactic: funext a c
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)
have h : (Perm ∘r Perm) a c ↔ a ~ c
Tactic: apply propext
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c
have h : (Perm ∘r Perm) a c → a ~ c
Tactic: constructor