awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
s t : Multiset α
x : α
inst_2 : DecidablePred (r x)
h : Rel r s t
empty : ∀ {t : Multiset α} (h : Rel r 0 t), countP (r x) 0 = countP (r x) t
⊢ countP (r x) s = countP (r x) t
have cons : ∀ (y : α) (s : Multiset α) (ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t) {t : Multiset α}
  (h : Rel r (y ::ₘ s) t), countP (r x) (y ::ₘ s) = countP (r x) t
Tactic: induction s using Multiset.induction_on generalizing t with
  | empty => rw [rel_zero_left.mp h]
  | cons y s ih =>
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
    rw [countP_cons, countP_cons, ih hb2]
    simp only [Nat.add_right_inj]
    exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    ∀ (a : α), count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ≤ 1
have simp : _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1
Tactic: simp only [quot_mk_to_coe'', coe_nodup, coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0
have pos : ∀ (h : a ∈ s), count a s = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
pos : ∀ (h : a ∈ s), count a s = 1
⊢ count a s = if a ∈ s then 1 else 0
have neg : ∀ (h : ¬a ∈ s), count a s = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : α
x : List α
⊢ count a (dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) x)) =
    if Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) x) a then 1 else 0
have simp : List.count a x.dedup = if a ∈ x then 1 else 0
Tactic: simp only [quot_mk_to_coe'', coe_dedup, mem_coe, coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s ≤ s.dedup ↔ s.Nodup
have rw : s ≤ s ∧ s.Nodup ↔ s.Nodup
Tactic: rw [le_dedup, and_iff_right le_rfl]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
rw : s ≤ s ∧ s.Nodup ↔ s.Nodup
⊢ s ≤ s.dedup ↔ s.Nodup
have rw₁ : s.Nodup ↔ s.Nodup
Tactic: rw [le_dedup, and_iff_right le_rfl]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ (s + t).dedup = t.dedup
have h₁ : ∀ (a b : List α)
  (h :
    Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
  (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
Tactic: induction s, t using Quot.induction_on₂
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ⊆ s
⊢ (s + t).dedup = s.dedup
have rw : (t + s).dedup = s.dedup
Tactic: rw [s.add_comm, Subset.dedup_add_right h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ⊆ s
rw : (t + s).dedup = s.dedup
⊢ (s + t).dedup = s.dedup
have rw₁ : s.dedup = s.dedup
Tactic: rw [s.add_comm, Subset.dedup_add_right h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ (s + t).dedup = s.dedup + t.dedup
have h₁ : ∀ (a b : List α)
  (h :
    _root_.Disjoint (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
  (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) +
      dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
Tactic: induction s, t using Quot.induction_on₂
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (s ++ t).dedup ~ s.dedup
have rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
Tactic: rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
⊢ (s ++ t).dedup ~ s.dedup
have rw₁ : (↑(s ++ t) : Multiset α).dedup = (↑s.dedup : Multiset α)
Tactic: rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
rw₁ : (↑(s ++ t) : Multiset α).dedup = (↑s.dedup : Multiset α)
⊢ (s ++ t).dedup ~ s.dedup
have rw₂ : ((↑s : Multiset α) + (↑t : Multiset α)).dedup = (↑s.dedup : Multiset α)
Tactic: rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
rw₁ : (↑(s ++ t) : Multiset α).dedup = (↑s.dedup : Multiset α)
rw₂ : ((↑s : Multiset α) + (↑t : Multiset α)).dedup = (↑s.dedup : Multiset α)
⊢ (s ++ t).dedup ~ s.dedup
have rw₃ : (↑s : Multiset α).dedup = (↑s.dedup : Multiset α)
Tactic: rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
rw₁ : (↑(s ++ t) : Multiset α).dedup = (↑s.dedup : Multiset α)
rw₂ : ((↑s : Multiset α) + (↑t : Multiset α)).dedup = (↑s.dedup : Multiset α)
rw₃ : (↑s : Multiset α).dedup = (↑s.dedup : Multiset α)
⊢ (s ++ t).dedup ~ s.dedup
have rw₄ : (↑s.dedup : Multiset α) = (↑s.dedup : Multiset α)
Tactic: rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Defs (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : (↑l₁ : Multiset α) = s₂
H : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
      (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) e H =
    (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)
have subst : ∀ {H : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a},
  Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
      (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) sorry H =
    (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)
Tactic: subst e
Cleared hypotheses: s₂, e, H
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
have hXZXY₁ : Z₁ + X₁ = Y₂ + X₂
Tactic: rw [add_comm X₁, add_comm X₂] at hXZXY
Cleared hypotheses: hXZXY, hYZ₂
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
have refine_1 : Z₂ + (Z₁ - Y₂) ≠ ∅
Tactic: refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_1 : Z₂ + (Z₁ - Y₂) ≠ ∅
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
have refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
Tactic: refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_1 : Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
have refine_3 : X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
Tactic: refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_1 : Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
refine_3 : X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
have refine_4 : ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
Tactic: refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
have refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + Y₁ + (Y₂ - Z₁)
Tactic: rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + Y₁ + (Y₂ - Z₁)
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
have refine_2₁ : X₁ + Y₁ = X₁ ∩ X₂ + (Y₂ - Z₁) + Y₁
Tactic: rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + Y₁ + (Y₂ - Z₁)
refine_2₁ : X₁ + Y₁ = X₁ ∩ X₂ + (Y₂ - Z₁) + Y₁
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
have refine_2₂ : X₁ + Y₁ = X₁ + Y₁
Tactic: rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
have refine_3 : Y₂ + X₂ = Z₁ + X₁
Tactic: rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
have refine_4 : (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
  ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z
Tactic: simp only [mem_add, or_imp, forall_and]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
⊢ (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z
have refine_4 : ∀ (y : α) (hy : y ∈ Y₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
refine_4 : ∀ (y : α) (hy : y ∈ Y₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z
have refine_4₁ : ∀ (y : α) (hy : y ∈ Y₂ - Z₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
have refine_4 : ∀ (z : α) (hz : z ∈ Z₁) (hyz : y < z), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
have pos : ∀ (z_in : z ∈ Y₂), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: by_cases z_in : z ∈ Y₂
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
pos : ∀ (z_in : z ∈ Y₂), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
have neg : ∀ (z_in : ¬z ∈ Y₂), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: by_cases z_in : z ∈ Y₂
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
have pos : ∀ (w : α) (hw : w ∈ Z₂) (hzw : z < w), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ z ∈ Z₁ - Y₂
have rwa : count z Y₂ < count z Z₁
Tactic: rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
rwa : count z Y₂ < count z Z₁
⊢ z ∈ Z₁ - Y₂
have rwa₁ : 0 < count z Z₁
Tactic: rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
have refine_4 : ∀ (z : α) (hz : z ∈ Z₂) (hyz : y < z), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Tactic: obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have rintro : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
  (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have rintro₁ : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
  (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
rintro₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have refine_1 : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z), Z₂ + (Z₁ - Y₂) ≠ ∅
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
rintro₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
refine_1 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    Z₂ + (Z₁ - Y₂) ≠ ∅
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have refine_2 : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
  X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P