awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c = b ∨ c ∈ l
cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r c c
⊢ r b c
have cons₁ : ∀ (hc : c ∈ l), r b c
Tactic: rcases hc with (rfl | hc)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hc : c = a ∨ c ∈ l
hb : b ∈ l
⊢ r b c
have cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r b c
Tactic: rcases hc with (rfl | hc)
Cleared hypotheses: a, hs, hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hc : c = a ∨ c ∈ l
hb : b ∈ l
cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r b c
⊢ r b c
have cons₁ : ∀ (hc : c ∈ l), r b c
Tactic: rcases hc with (rfl | hc)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
a : α
l : List α
h_1 : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil
h : Chain r (↑(a :: l) : Cycle α)
⊢ (↑(a :: l) : Cycle α) = Cycle.nil
have ha : a ∈ a :: l
Tactic: have ha : a ∈ a :: l := mem_cons_self
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
h : Chain r s
⊢ s = Cycle.nil
have nil : ∀ (h : Chain r Cycle.nil), Eq.{u_1 + 1} (α := Cycle α) Cycle.nil Cycle.nil
Tactic: induction s with
  | nil => rfl
  | cons a l h =>
    have ha : a ∈ a :: l := mem_cons_self
    exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
h : Chain r s
nil : ∀ (h : Chain r Cycle.nil), Eq.{u_1 + 1} (α := Cycle α) Cycle.nil Cycle.nil
⊢ s = Cycle.nil
have cons : ∀ (a : α) (l : List α) (h : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil)
  (h : Chain r (↑(a :: l) : Cycle α)), (↑(a :: l) : Cycle α) = Cycle.nil
Tactic: induction s with
  | nil => rfl
  | cons a l h =>
    have ha : a ∈ a :: l := mem_cons_self
    exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
have rw : ∀ (hs : ∀ a ∈ s, ∀ b ∈ s, r a b) {a b : α} (ha : a ∈ s) (hb : b ∈ s), a = b
Tactic: rw [chain_iff_pairwise] at hs
Cleared hypotheses: hs, a, b, ha, hb
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup
have isTrue : a ∈ l.dedup → (a :: l).dedup = l.dedup
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
isTrue : a ∈ l.dedup → (a :: l).dedup = l.dedup
⊢ (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup
have isFalse : ¬a ∈ l.dedup → (a :: l).dedup = a :: l.dedup
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ a ∈ l.dedup ↔ a ∈ l
have refine_2 : ∀ (this : (¬∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b),
  a ∈ l.dedup ↔ a ∈ l
Tactic: have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
refine_2 :
  ∀ (this : (¬∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b),
    a ∈ l.dedup ↔ a ∈ l
⊢ a ∈ l.dedup ↔ a ∈ l
have refine_1 : ∀ {x y z : α}, (fun (x1 x2 : α) ↦ x1 ≠ x2) x z → (fun (x1 x2 : α) ↦ x1 ≠ x2) x y ∨ (fun (x1 x2 : α) ↦ x1 ≠ x2) y z
Tactic: have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
have pos : ∀ (ha : a ∈ l),
  (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
Tactic: by_cases ha : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
pos :
  ∀ (ha : a ∈ l),
    (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
have neg : ∀ (ha : ¬a ∈ l),
  (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
Tactic: by_cases ha : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
have pos : ∀ (ha : a ∈ l),
  (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
Tactic: by_cases ha : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
pos :
  ∀ (ha : a ∈ l),
    (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
have neg : ∀ (ha : ¬a ∈ l),
  (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
Tactic: by_cases ha : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
have refine_1 : ∀ (h : l.dedup = a :: l'), a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
refine_1 : ∀ (h : l.dedup = a :: l'), a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
have refine_2 : ∀ (h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'), l.dedup = a :: l'
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'
have rw : (a :: l').tail = l'
Tactic: rw [h, tail_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
rw : (a :: l').tail = l'
⊢ l.dedup.tail = l'
have rw₁ : l' = l'
Tactic: rw [h, tail_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
have refine_1 : ∀ (ha : a ∈ l'), False
Tactic: refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
⊢ False
have this : 0 < count a l'
Tactic: have := count_pos_iff.2 ha
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this : 0 < count a l'
⊢ False
have this₁ : count a l.dedup ≤ 1
Tactic: have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this_1 : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ False
have this₁ : count a l' + 1 ≤ 1
Tactic: rw [h, count_cons_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'
have this : l.dedup.head! :: l.dedup.tail = l.dedup
Tactic: have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
⊢ l.dedup = a :: l'
have hal : a ∈ l.dedup
Tactic: have hal : a ∈ l.dedup := mem_dedup.2 h.1
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ l.dedup = a :: l'
have hal₁ : ¬a ∈ l.dedup.tail → a = l.dedup.head!
Tactic: rw [← this, mem_cons, or_iff_not_imp_right] at hal
Cleared hypotheses: hal
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []
have pos : ∀ (h : a ∈ l), (a :: l).dedup = [] ↔ a :: l = []
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
pos : ∀ (h : a ∈ l), (a :: l).dedup = [] ↔ a :: l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []
have neg : ∀ (h : ¬a ∈ l), (a :: l).dedup = [] ↔ a :: l = []
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.dedup = [] ↔ l = []
have nil : Eq.{u_1 + 1} (α := List α) (dedup []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
Tactic: induction l with
  | nil => exact Iff.rfl
  | cons a l hl =>
    by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (dedup []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
⊢ l.dedup = [] ↔ l = []
have cons : ∀ (a : α) (l : List α) (hl : l.dedup = [] ↔ l = []), (a :: l).dedup = [] ↔ a :: l = []
Tactic: induction l with
  | nil => exact Iff.rfl
  | cons a l hl =>
    by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
have cons : ∀ (a : α) (l₁ : List α) (IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup), (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
Tactic: induction l₁ with | nil => rfl | cons a l₁ IH => ?_
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
have cons : (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)
Tactic: simp only [cons_union] at *
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)
have cons : (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Tactic: rw [← IH, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have pos : ∀ (h : a ∈ (l₁ ++ l₂).dedup), (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Tactic: by_cases h : a ∈ dedup (l₁ ++ l₂)
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
pos : ∀ (h : a ∈ (l₁ ++ l₂).dedup), (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have neg : ∀ (h : ¬a ∈ (l₁ ++ l₂).dedup), (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Tactic: by_cases h : a ∈ dedup (l₁ ++ l₂)
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have pos : (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
Tactic: rw [dedup_cons_of_mem' h, insert_of_mem h]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
pos : (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have pos₁ : (l₁ ++ l₂).dedup = (l₁ ++ l₂).dedup
Tactic: rw [dedup_cons_of_mem' h, insert_of_mem h]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have neg : a :: (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
Tactic: rw [dedup_cons_of_notMem' h, insert_of_not_mem h]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
neg : a :: (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
have neg₁ : a :: (l₁ ++ l₂).dedup = a :: (l₁ ++ l₂).dedup
Tactic: rw [dedup_cons_of_notMem' h, insert_of_not_mem h]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have pos : ∀ (h : x ∈ xs), (f x :: map f xs).dedup = map f (x :: xs).dedup
Tactic: by_cases h : x ∈ xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
pos : ∀ (h : x ∈ xs), (f x :: map f xs).dedup = map f (x :: xs).dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have neg : ∀ (h : ¬x ∈ xs), (f x :: map f xs).dedup = map f (x :: xs).dedup
Tactic: by_cases h : x ∈ xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have pos : (f x :: map f xs).dedup = map f xs.dedup
Tactic: rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
pos : (f x :: map f xs).dedup = map f xs.dedup
pos₁ : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have pos₂ : map f xs.dedup = map f xs.dedup
Tactic: rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have neg : (f x :: map f xs).dedup = map f (x :: xs.dedup)
Tactic: rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
neg : (f x :: map f xs).dedup = map f (x :: xs.dedup)
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have neg₁ : f x :: (map f xs).dedup = map f (x :: xs.dedup)
Tactic: rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
neg : (f x :: map f xs).dedup = map f (x :: xs.dedup)
neg₁ : f x :: (map f xs).dedup = map f (x :: xs.dedup)
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have neg₂ : f x :: map f xs.dedup = map f (x :: xs.dedup)
Tactic: rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
neg : (f x :: map f xs).dedup = map f (x :: xs.dedup)
neg₁ : f x :: (map f xs).dedup = map f (x :: xs.dedup)
neg₂ : f x :: map f xs.dedup = map f (x :: xs.dedup)
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
have neg₃ : f x :: map f xs.dedup = f x :: map f xs.dedup
Tactic: rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
⊢ (map f xs).dedup = map f xs.dedup
have nil : (map f []).dedup = map f (dedup [])
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
nil : (map f []).dedup = map f (dedup [])
⊢ (map f xs).dedup = map f xs.dedup
have cons : ∀ (x : α) (xs : List α) (ih : (map f xs).dedup = map f xs.dedup), (map f (x :: xs)).dedup = map f (x :: xs).dedup
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup
have rw : xs ∪ ys.dedup = ys.dedup
Tactic: rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
rw : xs ∪ ys.dedup = ys.dedup
⊢ (xs ++ ys).dedup = ys.dedup
have rw₁ : ys.dedup = ys.dedup
Tactic: rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
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
have cons : List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Tactic: rw [cons_union]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have h₁ : ¬x ∈ ys ∧ xs.Disjoint ys
Tactic: rw [disjoint_cons_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have pos : ∀ (hx : x ∈ xs), List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Tactic: by_cases hx : x ∈ xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
pos : ∀ (hx : x ∈ xs), List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have neg : ∀ (hx : ¬x ∈ xs), List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Tactic: by_cases hx : x ∈ xs
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have pos : List.insert x (xs ∪ ys) = xs.dedup ++ ys
Tactic: rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
pos : List.insert x (xs ∪ ys) = xs.dedup ++ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have pos₁ : xs ∪ ys = xs.dedup ++ ys
Tactic: rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
pos : List.insert x (xs ∪ ys) = xs.dedup ++ ys
pos₁ : xs ∪ ys = xs.dedup ++ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have pos₂ : xs.dedup ++ ys = xs.dedup ++ ys
Tactic: rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
have neg : ¬x ∈ xs ∪ ys
Tactic: rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∪ ys
have neg : ¬x ∈ xs ∧ ¬x ∈ ys
Tactic: rw [mem_union_iff, not_or]