ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ y ↔ z + x = z ∪ x ∧ x = y
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ y ↔ Disjoint z x ∧ x = y
rw [← add_eq_union_iff_disjoint]
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ y → z + x = z ∪ x ∧ x = y

case mpr
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ x ∧ x = y → z + x = z ∪ y
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ y ↔ z + x = z ∪ x ∧ x = y
constructor
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ z + x = z ∪ x ∧ x = y
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ y → z + x = z ∪ x ∧ x = y
intro h0
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ x = y

case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ x = y → z + x = z ∪ x
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ z + x = z ∪ x ∧ x = y
rw [and_iff_right_of_imp]
no goals
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ x = y
exact (le_of_add_le_add_left <| h0.trans_le <| union_le_add z y).antisymm h
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x z : Multiset α
h : x ≤ x
h0 : z + x = z ∪ x
⊢ z + x = z ∪ x
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
h0 : z + x = z ∪ y
⊢ x = y → z + x = z ∪ x
rintro rfl
no goals
case mp
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x z : Multiset α
h : x ≤ x
h0 : z + x = z ∪ x
⊢ z + x = z ∪ x
exact h0
case mpr.intro
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x z : Multiset α
h0 : z + x = z ∪ x
h : x ≤ x
⊢ z + x = z ∪ x
case mpr
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : y ≤ x
⊢ z + x = z ∪ x ∧ x = y → z + x = z ∪ y
rintro ⟨h0, rfl⟩
no goals
case mpr.intro
ι : Type ?u.902858
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x z : Multiset α
h0 : z + x = z ∪ x
h : x ≤ x
⊢ z + x = z ∪ x
exact h0