awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys = xs.dedup ++ ys
have nil : ∀ (h : Disjoint [] ys), [] ∪ ys = dedup [] ++ ys
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union]
    rw [disjoint_cons_left] at h
    by_cases hx : x ∈ xs
    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
    · rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
nil : ∀ (h : Disjoint [] ys), [] ∪ ys = dedup [] ++ ys
⊢ xs ∪ ys = xs.dedup ++ ys
have cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys) (h : (x :: xs).Disjoint ys),
  x :: xs ∪ ys = (x :: xs).dedup ++ ys
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union]
    rw [disjoint_cons_left] at h
    by_cases hx : x ∈ xs
    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
    · rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup
have rw : xs.Disjoint ys.dedup
Tactic: rw [List.dedup_append, Disjoint.union_eq]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
n : ℕ
h : n + 2 ≠ 0
⊢ (replicate (n + 2) x).dedup = [x]
have rw : (x :: replicate (n + 1) x).dedup = [x]
Tactic: rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
n : ℕ
h : n + 2 ≠ 0
rw : (x :: replicate (n + 1) x).dedup = [x]
⊢ (replicate (n + 2) x).dedup = [x]
have rw₁ : (replicate n.succ x).dedup = [x]
Tactic: rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
n : ℕ
h : n + 2 ≠ 0
rw : (x :: replicate (n + 1) x).dedup = [x]
rw₁ : (replicate n.succ x).dedup = [x]
⊢ (replicate (n + 2) x).dedup = [x]
have rw₂ : [x] = [x]
Tactic: rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0
have simp_rw : Eq (α := ℕ) (if a ∈ l.dedup then 1 else 0) (if a ∈ l then 1 else 0)
Tactic: simp_rw [List.Nodup.count <| nodup_dedup l, mem_dedup]
-- Lean 4 proof step from Mathlib.Data.List.Defs (goal)
Goal:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (is.length + length.{u_1} (α := α) [], is.length)
    ((t :: ts).length + is.length, (t :: ts).length)
have simp_wf : Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (is.length, is.length)
  (ts.length + 1 + is.length, ts.length + 1)
Tactic: simp_wf
-- Lean 4 proof step from Mathlib.Data.List.Defs (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n
have zero : ∀ (a : α) (l : List α), iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0
Tactic: induction n generalizing a l
Cleared hypotheses: a, n, l
-- Lean 4 proof step from Mathlib.Data.List.Defs (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
zero : ∀ (a : α) (l : List α), iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n
have succ : ∀ (n : ℕ),
  (∀ (a : α) (l : List α), iterateTR.loop f a n l = l.reverse ++ iterate f a n) →
    ∀ (a : α) (l : List α), iterateTR.loop f a (n + 1) l = l.reverse ++ iterate f a (n + 1)
Tactic: induction n generalizing a l
Cleared hypotheses: a, n, l
-- Lean 4 proof step from Mathlib.Data.List.Defs (goal)
Goal:
⊢ @iterate = @iterateTR
have h : ∀ (α : Type u_7) (f : α → α) (a : α) (n : ℕ), iterate f a n = iterateTR f a n
Tactic: funext α f a n
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l
have rw : (if R b a then b :: destutter' R a l else destutter' R b l) = b :: destutter' R a l
Tactic: rw [destutter', if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : R b a
rw : (if R b a then b :: destutter' R a l else destutter' R b l) = b :: destutter' R a l
⊢ destutter' R b (a :: l) = b :: destutter' R a l
have rw₁ : b :: destutter' R a l = b :: destutter' R a l
Tactic: rw [destutter', if_pos h]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b (a :: l) = destutter' R b l
have rw : (if R b a then b :: destutter' R a l else destutter' R b l) = destutter' R b l
Tactic: rw [destutter', if_neg h]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : ¬R b a
rw : (if R b a then b :: destutter' R a l else destutter' R b l) = destutter' R b l
⊢ destutter' R b (a :: l) = destutter' R b l
have rw₁ : destutter' R b l = destutter' R b l
Tactic: rw [destutter', if_neg h]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]
have pos : ∀ (h : R a b), destutter' R a [b] = [a, b]
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
pos : ∀ (h : R a b), destutter' R a [b] = [a, b]
⊢ destutter' R a [b] = if R a b then [a, b] else [a]
have neg : ∀ (h : ¬R a b), destutter' R a [b] = [a]
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
have pos : R a b → a :: destutter' R b l <+ a :: b :: l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
pos : R a b → a :: destutter' R b l <+ a :: b :: l
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
have neg : ¬R a b → destutter' R a l <+ a :: b :: l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter' R a l <+ a :: l
have nil : ∀ (a : α), destutter' R a [] <+ [a]
Tactic: induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons_cons a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
nil : ∀ (a : α), destutter' R a [] <+ [a]
⊢ destutter' R a l <+ a :: l
have cons : ∀ (b : α) (l : List α) (hl : ∀ (a : α), destutter' R a l <+ a :: l) (a : α), destutter' R a (b :: l) <+ a :: b :: l
Tactic: induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons_cons a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l
have pos : R a b → a ∈ a :: destutter' R b l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
pos : R a b → a ∈ a :: destutter' R b l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l
have neg : ¬R a b → a ∈ destutter' R a l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ a ∈ destutter' R a l
have nil : a ∈ destutter' R a []
Tactic: induction l with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · simp
    · assumption
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
nil : a ∈ destutter' R a []
⊢ a ∈ destutter' R a l
have cons : ∀ (b : α) (l : List α) (hl : a ∈ destutter' R a l), a ∈ destutter' R a (b :: l)
Tactic: induction l with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · simp
    · assumption
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
IH2 : ∀ (y a : α), IsChain R (destutter' R a (y :: l))
a : α
⊢ IsChain R (destutter' R a (b :: c :: l))
have IH2₁ : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
Tactic: simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
Cleared hypotheses: IH2
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ IsChain R (destutter' R a (b :: c :: l))
have cons_cons : (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
    (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
  (¬R a b → R a c → IsChain R (a :: destutter' R c l))
Tactic: simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
a : α
⊢ IsChain R (destutter' R a l)
have nil : ∀ (a : α), IsChain R (destutter' R a [])
Tactic: induction l using twoStepInduction generalizing a with
  | nil => simp
  | singleton => simp [apply_ite]
  | cons_cons b c l IH IH2 =>
    simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
    simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
    exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩
Cleared hypotheses: l, a
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
a : α
nil : ∀ (a : α), IsChain R (destutter' R a [])
⊢ IsChain R (destutter' R a l)
have singleton : ∀ (x a : α), IsChain R (destutter' R a [x])
Tactic: induction l using twoStepInduction generalizing a with
  | nil => simp
  | singleton => simp [apply_ite]
  | cons_cons b c l IH IH2 =>
    simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
    simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
    exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩
Cleared hypotheses: l, a
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
a : α
nil : ∀ (a : α), IsChain R (destutter' R a [])
singleton : ∀ (x a : α), IsChain R (destutter' R a [x])
⊢ IsChain R (destutter' R a l)
have cons_cons : ∀ (b c : α) (l : List α) (IH : ∀ (a : α), IsChain R (destutter' R a l))
  (IH2 : ∀ (y a : α), IsChain R (destutter' R a (y :: l))) (a : α), IsChain R (destutter' R a (b :: c :: l))
Tactic: induction l using twoStepInduction generalizing a with
  | nil => simp
  | singleton => simp [apply_ite]
  | cons_cons b c l IH IH2 =>
    simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
    simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
    exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩
Cleared hypotheses: l, a
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
have h₁ : R a b
Tactic: obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
h₁ : R a b
⊢ destutter' R a (b :: l) = a :: b :: l
have hc : IsChain R (b :: l)
Tactic: obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h_1 : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
have cons : a :: destutter' R b l = a :: b :: l
Tactic: rw [l.destutter'_cons_pos h, hb hc]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h_1 : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
cons : a :: destutter' R b l = a :: b :: l
⊢ destutter' R a (b :: l) = a :: b :: l
have cons₁ : a :: b :: l = a :: b :: l
Tactic: rw [l.destutter'_cons_pos h, hb hc]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : IsChain R (a :: l)
⊢ destutter' R a l = a :: l
have nil : ∀ {a : α} (h : IsChain R [a]), destutter' R a [] = [a]
Tactic: induction l generalizing a with
  | nil => simp
  | cons b l hb =>
    obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
    rw [l.destutter'_cons_pos h, hb hc]
Cleared hypotheses: l, a, h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : IsChain R (a :: l)
nil : ∀ {a : α} (h : IsChain R [a]), destutter' R a [] = [a]
⊢ destutter' R a l = a :: l
have cons : ∀ (b : α) (l : List α) (hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l) {a : α}
  (h : IsChain R (a :: b :: l)), destutter' R a (b :: l) = a :: b :: l
Tactic: induction l generalizing a with
  | nil => simp
  | cons b l hb =>
    obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
    rw [l.destutter'_cons_pos h, hb hc]
Cleared hypotheses: l, a, h
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (a :: l)
have rw : IsChain R (destutter' R a l)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))
have this : R a b ↔ R₂ (f a) (f b)
Tactic: have := hl a (by simp) b (by simp)
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))
have simp_rw : map f (if R a b then a :: destutter' R b l else destutter' R a l) =
  if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Tactic: simp_rw [map_cons, destutter_cons_cons, ← this]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
have pos : ∀ (hr : R a b),
  map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Tactic: by_cases hr : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
pos :
  ∀ (hr : R a b),
    map f (if R a b then a :: destutter' R b l else destutter' R a l) =
      if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
have neg : ∀ (hr : ¬R a b),
  map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Tactic: by_cases hr : R a b
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have by_cases : ∀ (hbc : R b c), (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
Tactic: by_cases hbc : R b c
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
by_cases : ∀ (hbc : R b c), (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have by_cases₁ : ∀ (hbc : ¬R b c), (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
Tactic: by_cases hbc : R b c
-- Lean 4 proof step from Mathlib.Data.List.Destutter (hypothesis)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have hac : ¬Rᶜ a c
Tactic: have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have simp_rw : (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
  (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
simp_rw :
  (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
    (if R a c then a :: destutter' R c l else destutter' R a l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have simp_rw₁ : (if R b c then b :: destutter' R c l else destutter' R b l).length ≤ (a :: destutter' R c l).length
Tactic: simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
simp_rw :
  (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
    (if R a c then a :: destutter' R c l else destutter' R a l).length
simp_rw₁ : (if R b c then b :: destutter' R c l else destutter' R b l).length ≤ (a :: destutter' R c l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have simp_rw₂ : (b :: destutter' R c l).length ≤ (a :: destutter' R c l).length
Tactic: simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
simp_rw :
  (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
    (if R a c then a :: destutter' R c l else destutter' R a l).length
simp_rw₁ : (if R b c then b :: destutter' R c l else destutter' R b l).length ≤ (a :: destutter' R c l).length
simp_rw₂ : (b :: destutter' R c l).length ≤ (a :: destutter' R c l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have simp_rw₃ : (destutter' R c l).length + 1 ≤ (destutter' R c l).length + 1
Tactic: simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
have simp : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: simp only [destutter', if_neg hbc]
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
have by_cases : ∀ (hac : R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: by_cases hac : R a c
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
by_cases :
  ∀ (hac : R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
have by_cases₁ : ∀ (hac : ¬R a c), (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
Tactic: by_cases hac : R a c
-- Lean 4 proof step from Mathlib.Data.List.Destutter (goal)
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
have simp : (destutter' R b l).length ≤ (destutter' R c l).length + 1
Tactic: simp only [if_pos hac, length_cons]