awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
hnm : n < m
⊢ filter (fun (x : ℕ) ↦ decide (x ≤ n)) (Ico n m) = [n]
have rw : filter (fun (x : ℕ) ↦ decide (x ≤ n)) (Ico n m) = filter (fun (x : ℕ) ↦ decide (x < n + 1)) (Ico n m)
Tactic: rw [← filter_lt_of_succ_bot hnm]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ (iterate f a n).length = n
have zero : ∀ (a : α), (iterate f a 0).length = 0
Tactic: induction n generalizing a
Cleared hypotheses: a, n
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
zero : ∀ (a : α), (iterate f a 0).length = 0
⊢ (iterate f a n).length = n
have succ : ∀ (n : ℕ), (∀ (a : α), (iterate f a n).length = n) → ∀ (a : α), (iterate f a (n + 1)).length = n + 1
Tactic: induction n generalizing a
Cleared hypotheses: a, n
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ iterate f a n = [] ↔ n = 0
have rw : (iterate f a n).length = 0 ↔ n = 0
Tactic: rw [← length_eq_zero_iff, length_iterate]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
rw : (iterate f a n).length = 0 ↔ n = 0
⊢ iterate f a n = [] ↔ n = 0
have rw₁ : n = 0 ↔ n = 0
Tactic: rw [← length_eq_zero_iff, length_iterate]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < (iterate f a n).length
⊢ i < n
have rwa : ∀ (h : i < n), i < n
Tactic: rwa [length_iterate] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ map (fun (x : ℕ) ↦ f^[x] a) (range n) = iterate f a n
have hl : length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = (iterate f a n).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
n : ℕ
f : α → α
a : α
hl : length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = (iterate f a n).length
⊢ map (fun (x : ℕ) ↦ f^[x] a) (range n) = iterate f a n
have h : ∀ (i : ℕ) (h₁ : i < length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n))) (h₂ : i < (iterate f a n).length),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (iterate f a n) i h₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ₂ : a :: iterate f (f a) (n + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₂ : a :: iterate f (f a) (n + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ₃ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₂ : a :: iterate f (f a) (n + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₃ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ₄ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₂ : a :: iterate f (f a) (n + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₃ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₄ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1
have succ₅ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1)
Tactic: rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n
have zero : ∀ (a : α), iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n
Tactic: induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
Cleared hypotheses: a, m
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
zero : ∀ (a : α), iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n
have succ : ∀ (n_1 : ℕ) (ih : ∀ (a : α), iterate f a (n_1 + n) = iterate f a n_1 ++ iterate f (f^[n_1] a) n) (a : α),
  iterate f a (n_1 + 1 + n) = iterate f a (n_1 + 1) ++ iterate f (f^[n_1 + 1] a) n
Tactic: induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]
Cleared hypotheses: a, m
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ take m (iterate f a n) = iterate f a (min m n)
have rw : take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = iterate f a (min m n)
Tactic: rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
rw : take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = iterate f a (min m n)
⊢ take m (iterate f a n) = iterate f a (min m n)
have rw₁ : Eq.{u_1 + 1} (α := List α) (take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)))
  (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
Tactic: rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
rw : take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = iterate f a (min m n)
rw₁ :
  Eq.{u_1 + 1} (α := List α) (take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
⊢ take m (iterate f a n) = iterate f a (min m n)
have rw₂ : Eq.{u_1 + 1} (α := List α) (map (fun (x : ℕ) ↦ f^[x] a) (take m (range n)))
  (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
Tactic: rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]
-- Lean 4 proof step from Mathlib.Data.List.Iterate (goal)
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
rw : take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = iterate f a (min m n)
rw₁ :
  Eq.{u_1 + 1} (α := List α) (take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
rw₂ :
  Eq.{u_1 + 1} (α := List α) (map (fun (x : ℕ) ↦ f^[x] a) (take m (range n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
⊢ take m (iterate f a n) = iterate f a (min m n)
have rw₃ : Eq.{u_1 + 1} (α := List α) (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
  (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
Tactic: rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ x :: xs ∪ ys = ys
have cons : List.insert x (xs ∪ ys) = ys
Tactic: rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys
h : x :: xs ⊆ ys
cons : List.insert x (xs ∪ ys) = ys
⊢ x :: xs ∪ ys = ys
have cons₁ : xs ∪ ys = ys
Tactic: rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys
h : x :: xs ⊆ ys
cons : List.insert x (xs ∪ ys) = ys
cons₁ : xs ∪ ys = ys
⊢ x :: xs ∪ ys = ys
have cons₂ : ys = ys
Tactic: rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys = ys
have nil : ∀ (h : [] ⊆ ys), [] ∪ ys = ys
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
nil : ∀ (h : [] ⊆ ys), [] ∪ ys = ys
⊢ xs ∪ ys = ys
have cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys) (h : x :: xs ⊆ ys), x :: xs ∪ ys = ys
Tactic: induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
⊢ (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂
have pos : a ∈ l₂ → (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
pos : a ∈ l₂ → (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
⊢ (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂
have neg : ¬a ∈ l₂ → (a :: l₁) ∩ l₂ = l₁ ∩ l₂
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l ∩ [] = []
have nil : Eq.{u_1 + 1} (α := List α) ([] ∩ []) []
Tactic: induction l with grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) ([] ∩ []) []
⊢ l ∩ [] = []
have cons : ∀ (head : α) (tail : List α), tail ∩ [] = [] → (head :: tail) ∩ [] = []
Tactic: induction l with grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂
have simp : (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂
Tactic: simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ List.bagInter [] l = []
have nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
⊢ List.bagInter [] l = []
have cons : ∀ (head : α) (tail : List α), List.bagInter [] (head :: tail) = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.bagInter [] = []
have nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
⊢ l.bagInter [] = []
have cons : ∀ (head : α) (tail : List α), (head :: tail).bagInter [] = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
have nil : ∀ (h : Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = a :: l₁.bagInter (List.erase [] a)
Tactic: cases l₂ with grind [List.bagInter]
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
nil : ∀ (h : Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = a :: l₁.bagInter (List.erase [] a)
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
have cons : ∀ (head : α) (tail : List α) (h : a ∈ head :: tail),
  (a :: l₁).bagInter (head :: tail) = a :: l₁.bagInter ((head :: tail).erase a)
Tactic: cases l₂ with grind [List.bagInter]
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂
have nil : ∀ (h : ¬Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = l₁.bagInter []
Tactic: cases l₂ with grind [List.bagInter]
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
nil : ∀ (h : ¬Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = l₁.bagInter []
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂
have cons : ∀ (head : α) (tail : List α) (h : ¬a ∈ head :: tail), (a :: l₁).bagInter (head :: tail) = l₁.bagInter (head :: tail)
Tactic: cases l₂ with grind [List.bagInter]
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
⊢ (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂
have pos : a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
pos : a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
⊢ (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂
have neg : ¬a ∈ l₂ → (a :: l₁).bagInter l₂ = l₁.bagInter l₂
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂
have nil : ∀ (l₂ : List α) (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (a :: l₂) = List.bagInter [] l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
nil : ∀ (l₂ : List α) (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (a :: l₂) = List.bagInter [] l₂
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂
have cons : ∀ (head : α) (tail : List α),
  (∀ (l₂ : List α) (h : ¬a ∈ tail), tail.bagInter (a :: l₂) = tail.bagInter l₂) →
    ∀ (l₂ : List α) (h : ¬a ∈ head :: tail), (head :: tail).bagInter (a :: l₂) = (head :: tail).bagInter l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
have case1 : ∀ (x : List α), Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
have case2 : ∀ (t : List α), (t = [] → False) → (Membership.mem (γ := List α) [] a ↔ a ∈ t ∧ Membership.mem (γ := List α) [] a)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x
case2 :
  ∀ (t : List α), (t = [] → False) → (Membership.mem (γ := List α) [] a ↔ a ∈ t ∧ Membership.mem (γ := List α) [] a)
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
have case3 : ∀ (a_1 : α) (l₁ l₂ : List α),
  (l₂ = [] → False) →
    elem a_1 l₂ = true →
      (a ∈ l₁.bagInter (l₂.erase a_1) ↔ a ∈ l₁ ∧ a ∈ l₂.erase a_1) →
        (a ∈ a_1 :: l₁.bagInter (l₂.erase a_1) ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x
case2 :
  ∀ (t : List α), (t = [] → False) → (Membership.mem (γ := List α) [] a ↔ a ∈ t ∧ Membership.mem (γ := List α) [] a)
case3 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      elem a_1 l₂ = true →
        (a ∈ l₁.bagInter (l₂.erase a_1) ↔ a ∈ l₁ ∧ a ∈ l₂.erase a_1) →
          (a ∈ a_1 :: l₁.bagInter (l₂.erase a_1) ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂)
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
have case4 : ∀ (a_1 : α) (l₁ l₂ : List α),
  (l₂ = [] → False) →
    ¬elem a_1 l₂ = true → (a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂) → (a ∈ l₁.bagInter l₂ ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
have case1 : ∀ (x : List α), count a [] = min (count a []) (count a x)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), count a [] = min (count a []) (count a x)
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
have case2 : ∀ (t : List α), (t = [] → False) → count a [] = min (count a t) (count a [])
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), count a [] = min (count a []) (count a x)
case2 : ∀ (t : List α), (t = [] → False) → count a [] = min (count a t) (count a [])
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
have case3 : ∀ (a_1 : α) (l₁ l₂ : List α),
  (l₂ = [] → False) →
    elem a_1 l₂ = true →
      count a (l₁.bagInter (l₂.erase a_1)) = min (count a l₁) (count a (l₂.erase a_1)) →
        count a (a_1 :: l₁.bagInter (l₂.erase a_1)) = min (count a (a_1 :: l₁)) (count a l₂)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), count a [] = min (count a []) (count a x)
case2 : ∀ (t : List α), (t = [] → False) → count a [] = min (count a t) (count a [])
case3 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      elem a_1 l₂ = true →
        count a (l₁.bagInter (l₂.erase a_1)) = min (count a l₁) (count a (l₂.erase a_1)) →
          count a (a_1 :: l₁.bagInter (l₂.erase a_1)) = min (count a (a_1 :: l₁)) (count a l₂)
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
have case4 : ∀ (a_1 : α) (l₁ l₂ : List α),
  (l₂ = [] → False) →
    ¬elem a_1 l₂ = true →
      count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂) →
        count a (l₁.bagInter l₂) = min (count a (a_1 :: l₁)) (count a l₂)
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ l₁.bagInter l₂ <+ l₁
have case1 : ∀ (x : List α), Sublist.{u_1} (α := α) [] []
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
case1 : ∀ (x : List α), Sublist.{u_1} (α := α) [] []
⊢ l₁.bagInter l₂ <+ l₁
have case2 : ∀ (t : List α), (t = [] → False) → [] <+ t
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
case1 : ∀ (x : List α), Sublist.{u_1} (α := α) [] []
case2 : ∀ (t : List α), (t = [] → False) → [] <+ t
⊢ l₁.bagInter l₂ <+ l₁
have case3 : ∀ (a : α) (l₁ l₂ : List α),
  (l₂ = [] → False) → elem a l₂ = true → l₁.bagInter (l₂.erase a) <+ l₁ → a :: l₁.bagInter (l₂.erase a) <+ a :: l₁
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
case1 : ∀ (x : List α), Sublist.{u_1} (α := α) [] []
case2 : ∀ (t : List α), (t = [] → False) → [] <+ t
case3 :
  ∀ (a : α) (l₁ l₂ : List α),
    (l₂ = [] → False) → elem a l₂ = true → l₁.bagInter (l₂.erase a) <+ l₁ → a :: l₁.bagInter (l₂.erase a) <+ a :: l₁
⊢ l₁.bagInter l₂ <+ l₁
have case4 : ∀ (a : α) (l₁ l₂ : List α), (l₂ = [] → False) → ¬elem a l₂ = true → l₁.bagInter l₂ <+ l₁ → l₁.bagInter l₂ <+ a :: l₁
Tactic: fun_induction List.bagInter with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a : α
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []
have nil : List.bagInter [] [a] = if Membership.mem (γ := List α) [] a then [a] else []
Tactic: induction l₁