awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
have suffices : 1 + List.count a l < List.count a l * List.count a l
Tactic: suffices 1 + l.count a < l.count a * l.count a by simpa
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l
have rw : 2 * List.count a l ≤ List.count a l * List.count a l
Tactic: rw [← Nat.two_mul]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l * List.count a l
have a₁ : 1 + List.count a l < List.count a l + List.count a l
Tactic: calc
    1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
a₁ : 1 + List.count a l < List.count a l + List.count a l
⊢ 1 + List.count a l < List.count a l * List.count a l
have a₂ : List.count a l + List.count a l ≤ List.count a l * List.count a l
Tactic: calc
    1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
x : α × α
⊢ x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd
have rcases : ∀ (x y : α), (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd
have simp_rw : (∃ (i : ℕ),
    ∃ (h : i < l.length),
      ∃ (j : ℕ),
        ∃ (h_1 : j < l.length),
          ¬i = j ∧
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry = x ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j sorry = y) ↔
  (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
Tactic: simp_rw [mem_offDiag_iff_getElem, mem_iff_getElem, Ne]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) ↔
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
have mp : (∃ (i : ℕ),
    ∃ (h : i < l.length),
      ∃ (j : ℕ),
        ∃ (h_1 : j < l.length),
          ¬i = j ∧
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry = x ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j sorry = y) →
  (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
x y : α
mp :
  (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) →
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
⊢ (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) ↔
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
have mpr : (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y →
  ∃ (i : ℕ),
    ∃ (h : i < l.length),
      ∃ (j : ℕ),
        ∃ (h_1 : j < l.length),
          ¬i = j ∧
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry = x ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j sorry = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
have H : Symmetric fun (x y : α) ↦ x ≠ y → R x y
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
H : Symmetric fun (x y : α) ↦ x ≠ y → R x y
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
have H₁ : ∀ (x : α), x ∈ l → x ≠ x → R x x
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
H : Symmetric fun (x y : α) ↦ x ≠ y → R x y
H₁ : ∀ (x : α), x ∈ l → x ≠ x → R x x
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
have H₂ : Pairwise (fun (x y : α) ↦ x ≠ y → R x y) l
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : 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
have rw : ∀ {a b : α}, [a, b] <+ l → R a b
Tactic: rw [pairwise_iff_forall_sublist]
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b
have refl : ∀ (hab : [a, a] <+ l), R a a
Tactic: cases heq
Cleared hypotheses: b, hab, heq
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ R a b
have a₁ : a ∈ l
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ : a ∈ l
⊢ R a b
have a₂ : b ∈ l
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ : a ∈ l
a₂ : b ∈ l
⊢ R a b
have a₃ : a ≠ b
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l
have a₁ : a ∈ [a, b]
Tactic: apply hab.subset
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l
have a₁ : a ∈ [a, b]
Tactic: try (apply hab.subset; simp)
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l
have a₁ : b ∈ [a, b]
Tactic: apply hab.subset
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l
have a₁ : b ∈ [a, b]
Tactic: try (apply hab.subset; simp)
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b
have if : ∀ (heq : a = b), R a b
Tactic: if heq : a = b then
    cases heq; apply refl
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
if : ∀ (heq : a = b), R a b
⊢ R a b
have if₁ : ∀ (heq : ¬a = b), R a b
Tactic: if heq : a = b then
    cases heq; apply refl
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise R l
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)
have rw : ∀ (h : Pairwise (fun (b a : α) ↦ R a b) l.reverse) (ha : a ∈ l.dropLast), R a (l.getLast sorry)
Tactic: rw [← pairwise_reverse] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun (b a : α) ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)
have rw : R a (l.reverse.head sorry)
Tactic: rw [getLast_eq_head_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : 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
have rwa : a ∈ l.dropLast.reverse
Tactic: rwa [tail_reverse, mem_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (hypothesis)
Goal:
α : 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 ⋯)
have ha₁ : a ∈ l.dropLast ∨ a = l.getLast sorry
Tactic: rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha
Cleared hypotheses: hlast
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
inst : Inhabited α
inst_1 : Std.Refl R
h : Pairwise R l
ha : a ∈ l
⊢ R l.head! a
have nil : ∀ (h : Pairwise R []) (ha : Membership.mem (γ := List α) [] a), R (head! []) a
Tactic: cases l
Cleared hypotheses: l, h, ha
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
inst : Inhabited α
inst_1 : Std.Refl R
h : Pairwise R l
ha : a ∈ l
nil : ∀ (h : Pairwise R []) (ha : Membership.mem (γ := List α) [] a), R (head! []) a
⊢ R l.head! a
have cons : ∀ (head : α) (tail : List α) (h : Pairwise R (head :: tail)) (ha : a ∈ head :: tail), R (head :: tail).head! a
Tactic: cases l
Cleared hypotheses: l, h, ha
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
head : α
tail : List α
h : Pairwise R (head :: tail)
ha : a ∈ head :: tail
⊢ R (head :: tail).head! a
have cons : ∀ (h : Pairwise R (a :: tail)), R (a :: tail).head! a
Tactic: cases ha with
    | head => exact refl_of ..
    | tail => exact rel_of_pairwise_cons h (by assumption)
Cleared hypotheses: head, h, ha
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
head : α
tail : List α
h : Pairwise R (head :: tail)
ha : a ∈ head :: tail
cons : ∀ (h : Pairwise R (a :: tail)), R (a :: tail).head! a
⊢ R (head :: tail).head! a
have cons₁ : Mem a tail → R (head :: tail).head! a
Tactic: cases ha with
    | head => exact refl_of ..
    | tail => exact rel_of_pairwise_cons h (by assumption)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
⊢ Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (b :: l)
have simp_rw : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)
Tactic: simp_rw [← isChain_iff_pairwise, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)
have simp_rw : R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)
Tactic: simp_rw [pairwise_cons_cons_iff_of_trans]
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
⊢ R (l.get a) (l.get b)
have inl : ∀ (hab : a ≤ a), R (l.get a) (l.get a)
Tactic: obtain rfl | hlt := Fin.eq_or_lt_of_le hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.List.Pairwise (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
inl : ∀ (hab : a ≤ a), R (l.get a) (l.get a)
⊢ R (l.get a) (l.get b)
have inr : ∀ (hlt : a < b), R (l.get a) (l.get b)
Tactic: obtain rfl | hlt := Fin.eq_or_lt_of_le hab
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l
have nil : Eq.{u_1 + 1} (α := List α) (reverse []) []
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
p : l.Palindrome
nil : Eq.{u_1 + 1} (α := List α) (reverse []) []
⊢ l.reverse = l
have singleton : ∀ (x : α), [x].reverse = [x]
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
p : l.Palindrome
nil : Eq.{u_1 + 1} (α := List α) (reverse []) []
singleton : ∀ (x : α), [x].reverse = [x]
⊢ l.reverse = l
have cons_concat : ∀ (x : α) {l : List α}, l.Palindrome → l.reverse = l → (x :: (l ++ [x])).reverse = x :: (l ++ [x])
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
⊢ l.reverse = l → l.Palindrome
have refine : ∀ (a : α) (l : List α) (b : α),
  (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome
Tactic: refine bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (hypothesis)
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
have hr₁ : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
Tactic: rw [reverse_cons, reverse_append] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
have rw : (x :: (l ++ [x])).Palindrome
Tactic: rw [head_eq_of_cons_eq hr]
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (hypothesis)
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [x])).Palindrome
have this : l.Palindrome
Tactic: have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
⊢ (l ++ l.reverse).Palindrome
have a : (l ++ l.reverse).reverse = l ++ l.reverse
Tactic: apply of_reverse_eq
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
⊢ (l ++ l.reverse).reverse = l ++ l.reverse
have a : l.reverse.reverse ++ l.reverse = l ++ l.reverse
Tactic: rw [reverse_append, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
l : List α
a : l.reverse.reverse ++ l.reverse = l ++ l.reverse
⊢ (l ++ l.reverse).reverse = l ++ l.reverse
have a₁ : l ++ l.reverse = l ++ l.reverse
Tactic: rw [reverse_append, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ (map f l).reverse = map f l
have rw : map f l.reverse = map f l
Tactic: rw [← map_reverse, p.reverse_eq]
-- Lean 4 proof step from Mathlib.Data.List.Palindrome (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
rw : map f l.reverse = map f l
⊢ (map f l).reverse = map f l
have rw₁ : map f l = map f l
Tactic: rw [← map_reverse, p.reverse_eq]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔
    ∀ i < w.length - p,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
have mp : w.HasPeriod p →
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mp :
  w.HasPeriod p →
    ∀ i < w.length - p,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
⊢ w.HasPeriod p ↔
    ∀ i < w.length - p,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
have mpr : (∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)) →
  w.HasPeriod p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j + p)
have i1 : j < w.length
Tactic: have i1 : j < w.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j + p)
have i2 : j + p < w.length
Tactic: have i2 : j + p < w.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j + p)
have min : p < w.length
Tactic: have min : p < w.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
min : p < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j + p)
have this : j + p - (take p w).length = j
Tactic: have : j + p - (List.take p w).length = j := by
      simp_all [min_eq_left_of_lt]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
⊢ drop p w <+: w
have simp : ∀ (i : ℕ) (h : i < w.length - p),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (p + i) sorry)
Tactic: simp only [prefix_iff_getElem?, length_drop, getElem_drop]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
i : ℕ
leni : i < w.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (p + i) ⋯)
have len : i + p < w.length
Tactic: have len : i + p < w.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
⊢ w <+: take p w ++ w
have drop : drop p w <+: w
Tactic: have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
drop : List.drop p w <+: w
⊢ w <+: take p w ++ w
have drop₁ : take p w ++ List.drop p w <+: take p w ++ w
Tactic: rw [← prefix_append_right_inj (w.take p)] at drop
Cleared hypotheses: drop
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have pos : ∀ (p_zero : p = 0),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
pos :
  ∀ (p_zero : p = 0),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have neg : ∀ (p_zero : ¬p = 0),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % 0) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: rw [p_zero, mod_zero]