awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mp₅ mp₆ mp₇ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
⊢ _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 ≤ u → x ≤ ⊥
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
mp₅ mp₆ mp₇ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₈ mp₉ mp₁₀ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
⊢ _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 → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
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
mp₅ mp₆ mp₇ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₈ mp₉ mp₁₀ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
mpr₅ mpr₆ mpr₇ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
⊢ _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 → ∀ ⦃x : Multiset α⦄, x ≤ u → x ≤ s → x ≤ ⊥
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint {a} t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
have rw : ¬a ∈ t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
Tactic: rw [singleton_disjoint]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have rw : ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: rw [_root_.disjoint_comm, disjoint_cons_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₁ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₁ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mp₅ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
mp₅ mp₆ mp₇ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
have mpr₅ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t
have rw : s ∩ t ⊆ 0 ↔ _root_.Disjoint s t
Tactic: rw [← subset_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₃ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₃ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₄ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₃ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₄ :
  (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₅ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₃ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₄ :
  (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0
simp_rw₅ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
have simp_rw₆ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a s = 0 ∨ count a t = 0
Tactic: simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t
have rw : u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
Tactic: rw [← add_eq_union_iff_disjoint]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
have refine_1 : ∀ (h0 : u + s = u ∪ t), u + s = u ∪ s ∧ s = t
Tactic: refine ⟨fun h0 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
refine_1 : ∀ (h0 : u + s = u ∪ t), u + s = u ∪ s ∧ s = t
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
have refine_2 : u + s = u ∪ s ∧ s = t → u + s = u ∪ t
Tactic: refine ⟨fun h0 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t
have refine_1 : s = t
Tactic: rw [and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
refine_1 : s = t
⊢ u + s = u ∪ s ∧ s = t
have refine_1₁ : s = t → u + s = u ∪ s
Tactic: rw [and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a : α | a ∈ m} fun (a₁ a₂ : α) ↦ r (f a₁) (f a₂)
b₁ : β
h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} b₁
b₂ : β
h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} b₂
hn : b₁ ≠ b₂
⊢ r b₁ b₂
have obtain : ∀ (a₁ : α) (H₁ : a₁ ∈ m) (h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₁)) (a₂ : α) (H₂ : a₂ ∈ m)
  (h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₂)) (hn : f a₁ ≠ f a₂), r (f a₁) (f a₂)
Tactic: obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
Cleared hypotheses: b₁, h₁, b₂, h₂, hn
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a (s ∪ t) ≤ 1
have rw : max (count a s) (count a t) ≤ 1
Tactic: rw [count_union]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
have mk : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) [])
Tactic: induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
l : List α
mk : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) [])
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
have mk₁ : ∀ (head : α) (tail : List α) (ih : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) tail)),
  p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (head :: tail))
Tactic: induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x x_1 : List α
h : x ≈ x_1
a : α
l l' : List α
b : C ⟦l⟧
b' : C ⟦l'⟧
hl : l ~ l'
h_1 : b ≍ b'
⊢ C_cons a ⟦l⟧ b ≍ C_cons a ⟦l'⟧ b'
have e_2 : ⟦l⟧ = ⟦l'⟧
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x
⊢ Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) 0
have rw : Eq.{u_1 + 1} (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) []) 0
Tactic: rw [eq_nil_iff_forall_not_mem.mpr H]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have haveI : ∀ (this : DecidableEq α),
  a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: haveI : DecidableEq α := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have mp : a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
mp : a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have mpr : (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have pos : ∀ (h : a = b), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
pos : ∀ (h : a = b), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have neg : ∀ (h : ¬a = b), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have pos : ∀ (eq : a ::ₘ as = a ::ₘ bs), a = a ∧ as = bs ∨ a ≠ a ∧ ∃ (cs : Multiset α), as = a ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: subst h
Cleared hypotheses: b, eq, h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (hypothesis)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have this₁ : a ∈ b ::ₘ bs
Tactic: have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (hypothesis)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have this₁ : a ∈ bs
Tactic: have : a ∈ bs := by simpa [h]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have neg : ∀ (cs : Multiset α) (hcs : bs = a ::ₘ cs), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
Tactic: rcases exists_cons_of_mem this with ⟨cs, hcs⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
have neg : as = b ::ₘ cs
Tactic: simp only [h, hcs, false_and, ne_eq, not_false_eq_true, cons_inj_right, exists_eq_right',
        true_and, false_or]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (hypothesis)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ as = b ::ₘ cs
have this₁ : a ::ₘ as = b ::ₘ a ::ₘ cs
Tactic: have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (hypothesis)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this_3 : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ as = b ::ₘ cs
have this₁ : a ::ₘ as = a ::ₘ b ::ₘ cs
Tactic: have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
have mpr : ∀ (eq₁ : a = b) (eq₂ : as = bs), a ::ₘ as = b ::ₘ bs
Tactic: rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
mpr : ∀ (eq₁ : a = b) (eq₂ : as = bs), a ::ₘ as = b ::ₘ bs
⊢ a ::ₘ as = b ::ₘ bs
have mpr₁ : a ≠ b → ∀ (cs : Multiset α) (eq₁ : as = b ::ₘ cs) (eq₂ : bs = a ::ₘ cs), a ::ₘ as = b ::ₘ bs
Tactic: rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
Cleared hypotheses: h