awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∪ u + s = s + t ∪ (s + u)
rw₁ : t + s ∪ (u + s) = s + t ∪ (s + u)
⊢ s + (t ∪ u) = s + t ∪ (s + u)
have rw₂ : t + s ∪ (u + s) = t + s ∪ (s + u)
Tactic: rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∪ u + s = s + t ∪ (s + u)
rw₁ : t + s ∪ (u + s) = s + t ∪ (s + u)
rw₂ : t + s ∪ (u + s) = t + s ∪ (s + u)
⊢ s + (t ∪ u) = s + t ∪ (s + u)
have rw₃ : t + s ∪ (u + s) = t + s ∪ (u + s)
Tactic: rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)
have by_contra! : ∀ (h : s ∩ t + u ≠ (s + u) ∩ (t + u)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
⊢ False
have obtain : ∀ (a : α) (ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)), False
Tactic: obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
    (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)
⊢ False
have ha₁ : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
Tactic: rw [← cons_add] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s + t ∩ u = (s + t) ∩ (s + u)
have rw : t ∩ u + s = (s + t) ∩ (s + u)
Tactic: rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∩ u + s = (s + t) ∩ (s + u)
⊢ s + t ∩ u = (s + t) ∩ (s + u)
have rw₁ : (t + s) ∩ (u + s) = (s + t) ∩ (s + u)
Tactic: rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∩ u + s = (s + t) ∩ (s + u)
rw₁ : (t + s) ∩ (u + s) = (s + t) ∩ (s + u)
⊢ s + t ∩ u = (s + t) ∩ (s + u)
have rw₂ : (t + s) ∩ (u + s) = (t + s) ∩ (s + u)
Tactic: rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∩ u + s = (s + t) ∩ (s + u)
rw₁ : (t + s) ∩ (u + s) = (s + t) ∩ (s + u)
rw₂ : (t + s) ∩ (u + s) = (t + s) ∩ (s + u)
⊢ s + t ∩ u = (s + t) ∩ (s + u)
have rw₃ : (t + s) ∩ (u + s) = (t + s) ∩ (u + s)
Tactic: rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t
have a : s ∪ t + s ∩ t ≤ s + t
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : s ∪ t + s ∩ t ≤ s + t
⊢ s ∪ t + s ∩ t = s + t
have a₁ : s + t ≤ s ∪ t + s ∩ t
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t
have a : s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
Tactic: rw [union_add_distrib]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
have a : t + s ∩ t ≤ s + t
Tactic: refine union_le (Multiset.add_le_add_left inter_le_right) ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t
have a : s ∩ t + t ≤ s + t
Tactic: rw [Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
have a : t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
Tactic: rw [Multiset.add_comm, add_inter_distrib]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
have a : t + s ≤ s ∪ t + t
Tactic: refine le_inter (Multiset.add_le_add_right le_union_right) ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t
have a : s + t ≤ s ∪ t + t
Tactic: rw [Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s - t + s ∩ t = s
have rw : s - t + t ∩ s = s
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s - t + t ∩ s = s
have revert : ∀ (s : Multiset α), s - t + t ∩ s = s
Tactic: revert s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s
have refine : ∀ (a : α) (t : Multiset α) (IH : ∀ (s : Multiset α), s - t + t ∩ s = s) (s : Multiset α),
  s - a ::ₘ t + (a ::ₘ t) ∩ s = s
Tactic: refine Multiset.induction_on t (by simp) fun a t IH s => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos : ∀ (h : a ∈ s), s - a ::ₘ t + (a ::ₘ t) ∩ s = s
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
pos : ∀ (h : a ∈ s), s - a ::ₘ t + (a ::ₘ t) ∩ s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have neg : ∀ (h : ¬a ∈ s), s - a ::ₘ t + (a ::ₘ t) ∩ s = s
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
Tactic: rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos₁ : s.erase a - t + a ::ₘ t ∩ s.erase a = s
Tactic: rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
pos₁ : s.erase a - t + a ::ₘ t ∩ s.erase a = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos₂ : a ::ₘ (s.erase a - t + t ∩ s.erase a) = s
Tactic: rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
pos₁ : s.erase a - t + a ::ₘ t ∩ s.erase a = s
pos₂ : a ::ₘ (s.erase a - t + t ∩ s.erase a) = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos₃ : a ::ₘ s.erase a = s
Tactic: rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
pos₁ : s.erase a - t + a ::ₘ t ∩ s.erase a = s
pos₂ : a ::ₘ (s.erase a - t + t ∩ s.erase a) = s
pos₃ : a ::ₘ s.erase a = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have pos₄ : s = s
Tactic: rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have neg : s - a ::ₘ t + t ∩ s = s
Tactic: rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
neg : s - a ::ₘ t + t ∩ s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have neg₁ : s.erase a - t + t ∩ s = s
Tactic: rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
neg : s - a ::ₘ t + t ∩ s = s
neg₁ : s.erase a - t + t ∩ s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have neg₂ : s - t + t ∩ s = s
Tactic: rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
neg : s - a ::ₘ t + t ∩ s = s
neg₁ : s.erase a - t + t ∩ s = s
neg₂ : s - t + t ∩ s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
have neg₃ : s = s
Tactic: rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∩ t) = min (count a s) (count a t)
have a₁ : count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
Tactic: apply @Nat.add_left_cancel (count a (s - t))
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
have a₁ : count a (s - t + s ∩ t) = count a (s - t) + min (count a s) (count a t)
Tactic: rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
a₁ : count a (s - t + s ∩ t) = count a (s - t) + min (count a s) (count a t)
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
have a₂ : count a s = count a (s - t) + min (count a s) (count a t)
Tactic: rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
a₁ : count a (s - t + s ∩ t) = count a (s - t) + min (count a s) (count a t)
a₂ : count a s = count a (s - t) + min (count a s) (count a t)
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
have a₃ : count a s = count a s - count a t + min (count a s) (count a t)
Tactic: rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
a₁ : count a (s - t + s ∩ t) = count a (s - t) + min (count a s) (count a t)
a₂ : count a s = count a (s - t) + min (count a s) (count a t)
a₃ : count a s = count a s - count a t + min (count a s) (count a t)
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
have a₄ : count a s = count a s
Tactic: rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
⊢ (↑s : Multiset α) ∩ (↑t : Multiset α) = (↑(s.bagInter t) : Multiset α)
have a : ∀ (a : α), count a ((↑s : Multiset α) ∩ (↑t : Multiset α)) = count a (↑(s.bagInter t) : Multiset α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x
have a : ∀ (y : α), count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
have a : min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Tactic: rw [count_inter, count_replicate, count_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
have pos : ∀ (h : x = y), min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
pos : ∀ (h : x = y), min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
have neg : ∀ (h : ¬x = y), min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ s ∩ replicate n x = replicate (min (count x s) n) x
have rw : replicate n x ∩ s = replicate (min (count x s) n) x
Tactic: rw [inter_comm, replicate_inter, min_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
x : α
rw : replicate n x ∩ s = replicate (min (count x s) n) x
⊢ s ∩ replicate n x = replicate (min (count x s) n) x
have rw₁ : replicate (min n (count x s)) x = replicate (min (count x s) n) x
Tactic: rw [inter_comm, replicate_inter, min_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
x : α
rw : replicate n x ∩ s = replicate (min (count x s) n) x
rw₁ : replicate (min n (count x s)) x = replicate (min (count x s) n) x
⊢ s ∩ replicate n x = replicate (min (count x s) n) x
have rw₂ : replicate (min (count x s) n) x = replicate (min (count x s) n) x
Tactic: rw [inter_comm, replicate_inter, min_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N ∩ Q + (P - M) = N
have a : ∀ (x : α), count x (N ∩ Q + (P - M)) = count x N
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x (N ∩ Q + (P - M)) = count x N
have a : min (count x N) (count x Q) + (count x P - count x M) = count x N
Tactic: rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x M + count x N = count x P + count x Q
have rw : ∀ (h : ∀ (a : α), count a (M + N) = count a (P + Q)) (x : α), count x M + count x N = count x P + count x Q
Tactic: rw [Multiset.ext] at h
Cleared hypotheses: h, x
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ min (count x N) (count x Q) + (count x P - count x M) = count x N
have h0 : count x M + count x N = count x P + count x Q
Tactic: have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.count_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t
have refine_1 : ∀ (h : _root_.Disjoint s t) (a : α) (hs : a ∈ s) (ht : a ∈ t), False
Tactic: refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t : Multiset α
refine_1 : ∀ (h : _root_.Disjoint s t) (a : α) (hs : a ∈ s) (ht : a ∈ t), False
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t
have refine_2 : ∀ (h : ∀ {a : α}, a ∈ s → ¬a ∈ t) (u : Multiset α) (hs : u ≤ s) (ht : u ≤ t), u ≤ ⊥
Tactic: refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥
have refine_2 : ∀ (a : α), ¬a ∈ u
Tactic: rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint l {a} ↔ ¬a ∈ l
have rw : _root_.Disjoint {a} l ↔ ¬a ∈ l
Tactic: rw [_root_.disjoint_comm, singleton_disjoint]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
l : Multiset α
a : α
rw : _root_.Disjoint {a} l ↔ ¬a ∈ l
⊢ _root_.Disjoint l {a} ↔ ¬a ∈ l
have rw₁ : ¬a ∈ l ↔ ¬a ∈ l
Tactic: rw [_root_.disjoint_comm, singleton_disjoint]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint s (t + u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have rw : _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
Tactic: rw [_root_.disjoint_comm, disjoint_add_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mp₁ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mpr₁ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
mpr₁ mpr₂ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mpr₃ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
mpr₁ mpr₂ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mpr₃ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mpr₄ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint u s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
mpr₁ mpr₂ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mpr₃ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s
mpr₄ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint u s
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
have mp₅ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
Tactic: tauto